MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "InjDataLoop2.ma" ---
--- scope checking ---
--- type checking ---
type  Empty : Set
type  Eq : .[i : Size] -> ^(A : Set i) -> ^(a : A) -> ^ A -> Set
term  Eq.refl : .[i : Size] -> .[A : Set i] -> .[a : A] -> < Eq.refl : Eq [i] A a a >
type  I : ^(F : Set -> Set) -> Set
ty-u  InvI : ^(A : Set) -> Set 1
term  InvI.inv : .[A : Set] -> ^(Inverse : Set -> Set) -> ^(isInverse : Eq [1] Set (I Inverse) A) -> < InvI.inv Inverse isInverse : InvI A >
type  Inverse : .[A : Set] -> (inv : InvI A) -> Set -> Set
{ Inverse [A] (InvI.inv #Inverse #isInverse) = #Inverse
}
term  isInverse : .[A : Set] -> (inv : InvI A) -> Eq [1] Set (I (Inverse [A] inv)) A
{ isInverse [A] (InvI.inv #Inverse #isInverse) = #isInverse
}
tmty  invertible : (A : Set) -> InvI A
{}
type  cantor : Set -> Set
type  cantor = \ A -> Inverse (invertible A) A -> Empty
type  cIc : Set
type  cIc = cantor (I cantor)
error during typechecking:
delta
/// checkExpr 0 |- case invertible (I cantor) : InvI (I cantor)
               { inv .cantor refl -> \ f -> f f
               } : invertible (I cantor) .Inverse (I cantor) -> Empty
/// case 1
/// dot pattern Just cantor
/// not instantiated