MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "FunctionExtensionality.ma" ---
--- scope checking ---
--- type checking ---
type  Id : ^(A : Set) -> ^(a : A) -> ^ A -> Set
term  Id.refl : .[A : Set] -> .[a : A] -> < Id.refl : Id A a a >
term  subst : .[A : Set] -> .[a : A] -> .[b : A] -> .[q : Id A a b] -> .[P : A -> Set] -> P a -> P b
{ subst [A] [a] [.a] [Id.refl] [P] h = h
}
term  J : .[A : Set] -> .[P : (a : A) -> (b : A) -> Id A a b -> Set] -> (h : (a : A) -> P a a Id.refl) -> (a : A) -> (b : A) -> .[q : Id A a b] -> P a b q
{ J [A] [P] h a .a [Id.refl] = h a
}
term  subst : .[A : Set] -> (a : A) -> (b : A) -> (q : Id A a b) -> .[P : A -> Set] -> P a -> P b
term  subst = [\ A ->] \ a -> \ b -> \ q -> [\ P ->] J [A] [\ x -> \ y -> \ p -> P x -> P y] (\ y -> \ p -> p) a b [q]
term  ext : .[A : Set] -> .[B : A -> Set] -> .[f : (x : A) -> B x] -> .[g : (x : A) -> B x] -> (h : .[x : A] -> Id (B x) (f x) (g x)) -> Id ((x : A) -> B x) f g
{}
error during typechecking:
extReducesNot
/// new A : Set
/// new a : v0
/// new f : (v0::Tm -> {A {a = v1, A = v0}})
/// new p : (.[x : v0::Tm] -> Id A x (f x){f = (v2 Up (v0::Tm -> {A {a = v1, A = v0}})), a = v1, A = v0})
/// checkExpr 4 |- refl : Id A a (subst [A -> A] (\ x -> x) (f ) (ext [A] [\ x -> A] [\ x -> x] [f ] (p x)) [\ x -> A] a)
/// checkForced fromList [(A,0),(a,1),(f,2),(p,3)] |- refl : Id A a (subst [A -> A] (\ x -> x) (f ) (ext [A] [\ x -> A] [\ x -> x] [f ] (p x)) [\ x -> A] a)
/// leqVal' (subtyping)  < Id.refl : Id A a a >  <=+  Id A a (subst [A -> A] (\ x -> x) (f ) (ext [A] [\ x -> A] [\ x -> x] [f ] (p x)) [\ x -> A] a)
/// leqVal' (subtyping)  Id A a a  <=+  Id A a (subst [A -> A] (\ x -> x) (f ) (ext [A] [\ x -> A] [\ x -> x] [f ] (p x)) [\ x -> A] a)
/// leqVal'  a  <=^  J (A -> A) (\ x -> \ y -> \ p -> A x -> A y) (\ y -> \ p -> p) (\ x -> x) (f ) (ext [A] [\ x -> A] [\ x -> x] [f ] (p x)) a : A
/// leqApp: head mismatch a != J