Functional extionality in Formality (almost)

Funext.fmc

// To type-check, install npm:
// $ curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.35.3/install.sh | bash
// $ nvm install 13.10.1
// 
// Then install Formality-Core:
// $ npm i -g formality-core
//
// Then download this file:
// $ curl https://gist.githubusercontent.com/MaiaVictor/28e3332c19fbd80747a0dceb33896b6b/raw/ae8d798225d2e6cc600e158f27d1b83ff384c262/intervals_with_self_types.fmc.c >> main.fmc
//
// Then just run `fmc` in the same dir:
// $ fmc

// Bool
// ====
// Bools can be defined as their dependent eliminations, using a self var `b`.

Bool: Type
  b<P: Bool -> Type> ->
  (True: P(true)) ->
  (False: P(false)) ->
  P(b)

true: Bool
  <P> (t) (f) t

false: Bool
  <P> (t) (f) f

// Nat
// ===
// Nats can be defined as their dependent eliminations, using a self var `n`.

Nat: Type
  n<P: Nat -> Type> ->
  (Zero: P(zero)) ->
  (Succ: (pred: Nat) -> P(succ(pred))) ->
  P(n)

zero: Nat
  <P> (z) (s) z

succ: Nat -> Nat
  (n) <P> (z) (s) s(n)

// Equality
// ========
// Equality can be defined as its dependent elimination, i.e., the J-axiom.

Id: (A: Type) -> A -> A -> Type
  (A) (a) (b)
  e<P: (b: A) -> Id(A)(a)(b) -> Type> ->
  (Refl: P(a)(refl<A><a>)) ->
  P(b)(e)

// A proof that a value is equal to itself.
refl: <A: Type> -> <a: A> -> Id(A)(a)(a)
  <A> <a>
  <P> (refl) refl

// If `a == b`, then `P(a)` implies `P(b)`.
rewrite: <A: Type> -> <a: A> -> <b: A> -> <P: A -> Type> -> <e: Id(A)(a)(b)> -> P(a) -> P(b)
  <A> <a> <b> <P> <e> (x)
  e<(b) (a) P(b)>(x)

// Ints
// ====
// Integers can be defined as a pair of nats quotiented by `(x,y) == (x+1,y+1)`.
// With self-types, we can do it with a smart constructor that normalizes both
// numbers to canonical form, i.e., (4,2) becomes (2,0), (3,5) becomes (0,2)...

Int: Type
  i<P: Int -> Type> ->
  (New: (x: Nat) -> (y: Nat) -> P(int(x)(y))) ->
  P(i)

int: Nat -> Nat -> Int
  (x) (y)
  <P> (new)
  x<(x) P(int(x)(y))>
  | new(zero)(y);
  | (x.pred) y<(y) P(int(succ(x.pred))(y))>
    | new(succ(x.pred))(zero);
    | (y.pred) int(x.pred)(y.pred)<P>(new);;

// Proof that `int(x)(y) == int(succ(x))(succ(y))`.
theorem: (x: Nat) -> (y: Nat) -> Id(Int)(int(x)(y))(int(succ(x))(succ(y)))
  (x) (y) refl<Int><int(x)(y)>

// Intervals
// =========
// Intervals can be defined with an extra constructor for `i0 == i1`, as in:
// data I : Set where
//   i0 : I
//   i1 : I
//   ie : i0 == i1

I: Type
  i<P: I -> Type> ->
  (I0: P(i0)) ->
  (I1: P(i1)) ->
  (Ie: Id(P(i0))(I0)(rewrite<I><i1><i0><P><ie>(I1))) ->
  P(i)

i0: I
  <P> (a) (b) (e)
  a

i1: I
  <P> (a) (b) (e)
  b

// But this is left as an axiom. Can we actually construct it?
ie: Id(I)(i1)(i0)
  ie

// Tests
// =====

// We can convert `i` to `true`.
i_to_true: (i: I) -> Bool
  (i)
  i<() Bool>
  | true;
  | true;
  | refl<Bool><true>;

// We can convert `i` to `false`.
i_to_false: (i: I) -> Bool
  (i)
  i<() Bool>
  | false;
  | false;
  | refl<Bool><false>;

// But we can't convert `i` to `true` or `false` depending on its value.
// distinguish_i: (i: I) -> Bool
//  (i)
//  i<() Bool>
//  | true;
//  | false;
//  | Type; // impossible: demands a proof that `true == false`

// Problem: can we define `ie`?

mirror :
  <A : Type> ->
  <a : A> ->
  <b : A> ->
  (e : Id(A)(a)(b)) ->
  Id(A)(b)(a)
  <A> <a> <b> (e)
  e<(b) () Id(A)(b)(a)>
  | refl<A><a>;

apply:
  <A : Type> ->
  <B : A -> Type> -> 
  (a : A) ->
  (b : A) ->
  (f : (x : A) -> B(x)) ->
  (e : Id(A)(a)(b)) ->
  Id(B(a))(f(a))(rewrite<A><b><a><B><mirror<A><a><b>(e)>(f(b)))
  <A> <B> (a) (b) (f) (e)
  e<(eb) (e) Id(B(a))(f(a))(rewrite<A><eb><a><B><mirror<A><a><eb>(e)>(f(eb)))>
  | refl<B(a)><f(a)>;


funext_helper:
  <A : Type> ->
  <B : A -> Type> ->
  (f : (x : A) -> B(x)) ->
  (g : (x : A) -> B(x)) ->
  (H : (x : A) -> Id(B(x))(f(x))(g(x))) ->
  (i : I) ->
  (x : A) ->
  B(x)
  <A> <B> (f) (g) (H) (i) (x)
  i<() B(x)>(f(x))(g(x))(H(x))

ie2 : Id(I)(i0)(i1)
  mirror<I><i1><i0>(ie)

// non-eta-reduced extentionaly, proving that `∀x:A. f(x) == g(x) -> λx.f(x) == λx.g(x)`
funext:
  <A : Type> ->
  <B : A -> Type> -> 
  (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))((x) f(x))((x) g(x))
  <A> <B> (f) (g) (H)
  apply<I><() ((x : A) -> B(x))>(i0)(i1)((x) funext_helper<A><B>(f)(g)(H)(x))(ie2)