HIT.fmc

HIT.fmc

Equal: (A: Type) -> A -> A -> Type
  (A) (a) (b)
  equal_value<P: (b: A) -> Equal(A)(a)(b) -> Type> ->
  (equal: P(a)(equal<A><a>)) ->
  P(b)(equal_value)

equal: <A: Type> -> <a: A> -> Equal(A)(a)(a)
  <A> <a>
  <P> (equal)
  equal

Interval0 : Type
  interval0_value<P: Interval0 -> Type> ->
  P(zero0) ->
  P(one0) ->
  P(interval0_value)

zero0 : Interval0
  <P> (z) (o) z

one0 : Interval0
  <P> (z) (o) z

loop0 : Equal(Interval0)(zero0)(one0)
  equal<Interval0><zero0>

Interval1 : Type
  interval_value<P: Interval1 -> Type> ->
  P(zero1) ->
  P(one1) ->
  P(interval_value)

zero1 : Interval1
  <P> (z) (o) o

one1 : Interval1
  <P> (z) (o) o

loop1 : Equal(Interval1)(zero1)(one1)
  equal<Interval1><one1>

RewriteType : Type
  <A : Type> ->
  <a : A> ->
  <b : A> ->
  (e : Equal(A)(a)(b)) ->
  <P : A -> Type> ->
  (x : P(a)) ->
  P(b)

rewrite : RewriteType
  <A> <a> <b> (e) <P> (x)
  e<(b) (a) P(b)>(x)

MirrorType : Type
  <A : Type> ->
  <a : A> ->
  <b : A> ->
  (e : Equal(A)(a)(b)) ->
  Equal(A)(b)(a)

mirror : MirrorType
  <A> <a> <b> (e)
  e<(b) () Equal(A)(b)(a)>
  | equal<A><a>;

ApplyType : Type
  <A : Type> ->
  <B : A -> Type> -> 
  (a : A) ->
  (b : A) ->
  (f : (x : A) -> B(x)) ->
  (e : Equal(A)(a)(b)) ->
  Equal(B(a))(f(a))(rewrite<A><b><a>(mirror<A><a><b>(e))<B>(f(b)))

apply : ApplyType
  <A> <B> (a) (b) (f) (e)
  e<(eb) (e) Equal(B(a))(f(a))(rewrite<A><eb><a>(mirror<A><a><eb>(e))<B>(f(eb)))>
  | equal<B(a)><f(a)>;

Funext : Type
  <A : Type> ->
  <B : A -> Type> -> 
  (f : (x : A) -> B(x)) ->
  (g : (x : A) -> B(x)) ->
  (H : (x : A) -> Equal(B(x))(f(x))(g(x))) ->
  (x : A) ->
  Equal((x : A) -> B(x))(f)(g)

FunextHelper : Type
  <A : Type> ->
  <B : A -> Type> -> 
  (f : (x : A) -> B(x)) ->
  (g : (x : A) -> B(x)) ->
  (H : (x : A) -> Equal(B(x))(f(x))(g(x))) ->
  (i : Interval0) ->
  (x : A) ->
  B(x)

funext_helper : FunextHelper
  <A> <B> (f) (g) (H) (i) (x)
  i<() B(x)>(f(x))(g(x))

//funext_helperF :
//  <A : Type> ->
//  <B : A -> Type> -> 
//  (f : (x : A) -> B(x)) ->
//  (g : (x : A) -> B(x)) ->
//  Equal((x : A) -> B(x))(funext_helper<A><B>(f)(g)(zero0))(f)
//
//  <A> <B> (f) (g)
//  equal<(x : A) -> B(x)><funext_helper<A><B>(f)(g)(zero0)>
//
//funext_helperG :
//  <A : Type> ->
//  <B : A -> Type> -> 
//  (f : (x : A) -> B(x)) ->
//  (g : (x : A) -> B(x)) ->
//  Equal((x : A) -> B(x))(funext_helper<A><B>(f)(g)(one0))(g)
//
//  <A> <B> (f) (g)
//  equal<(x : A) -> B(x)><funext_helper<A><B>(f)(g)(one0)>

funext : Funext
  <A> <B> (f) (g) (H) (x)
   apply<Interval0><() ((x : A) -> B(x))
     >(zero0)(one0)(funext_helper<A><B>(f)(g))(loop0)

// Found 1 type error(s):
// 
// Inside funext:
// Found type... Equal((x: A) -> B(x))(funext_helper(f)(g)(zero0))(rewrite(mirror(loop0))(funext_helper(f)(g)(one0)))
// Instead of... Equal((x: A) -> B(x))(f)(g)
// With context:
// - A : Type
// - B : A -> Type
// - f : (x: A) -> B(x)
// - g : (x: A) -> B(x)
// - H : (x: A) -> Equal(B(x))(f(x))(g(x))
// - x : A
// On line 139:
//    140| 
//    141| funext : Funext
//    142|   <A> <B> (f) (g) (H) (x)
//    143|    apply<Interval0><() ((x : A) -> B(x))
//    144|      >(zero0)(one0)(funext_helper<A><B>(f)(g))(loop0)
//    145| 
//    146| 
//    147| 
//    148|