Skip to content

Instantly share code, notes, and snippets.

@johnchandlerburnham
Created April 15, 2020 06:59
Show Gist options
  • Save johnchandlerburnham/0e37c0cb265aa67355892e32cb9579f8 to your computer and use it in GitHub Desktop.
Save johnchandlerburnham/0e37c0cb265aa67355892e32cb9579f8 to your computer and use it in GitHub Desktop.
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|
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment