test.xtt

let id = (λ A x → x) : Π (A : Set) (x : A) → A;

let refl = (λ A x i → x) : Π (A : Set) (x : A) → pathp i.A x x;

let funext = (λ A B f g pf i x → pf x i)
  : Π (A : Set) (B : Π(x: A) → Set) (f g : Π(x: A) → B x)
      (pf : ∀ (x : A) → pathp i.(B x) (f x) (g x))
  → pathp i.(Π(x : A) → B x) f g;

let sym = (λ A x y p i → com<i> 1 0 j.A j.y j.(p j) y)
  : Π (A : Set) (x y : A) (p : pathp i.A x y) → pathp i.A y x;

let trans = (λ A x y z p q i → com<i> 0 1 j.A j.x j.(q j) (p i))
  : Π (A : Set) (x y z : A) (p : pathp i.A x y) (q : pathp i.A y z)
  → pathp i.A x z;

let J = (λ A x y P base p →
  coe 0 1 i.(P (p i) (λ j → com<j> 0 i i.A i.x i.(p i) x)) base)
  : Π (A : Set) (x y : A) (P : Π (y : A) (_ : pathp _.A x y) → Set)
      (base : P x (refl A x)) (p : pathp _.A x y)
  → P y p;

let J-computes-definitionally = (λ A x P base i → base)
  : Π (A : Set) (x : A) (P : Π (y : A) (_ : pathp _.A x y) → Set)
      (base : P x (refl A x))
  → pathp i.(P x (refl A x)) (J A x x P base (refl A x)) base;

let pathp-to-coe-path
  = (λ A B P x y p i →
    com<i> 0 1 j.(P j) j.(coe 0 j i.(P i) x) j.(p j) x)
  : Π (A B : Set) (P : pathp i.Set A B) (x : A) (y : B) (p : pathp i.(P i) x y)
  → pathp i.B (coe 0 1 i.(P i) x) y;

let coe-path-to-pathp
  = (λ A B P x y p i →
    com<i> 0 1 j.(P i) j.x j.(p j) (coe 0 i i.(P i) x))
  : Π (A B : Set) (P : pathp i.Set A B) (x : A) (y : B) 
      (p : pathp i.B (coe 0 1 i.(P i) x) y)
  → pathp i.(P i) x y;

-- Definitional UIP!
let UIP_type = Π (A B : Set) (Ty : pathp i.Set A B) (x : A) (y : B)
  (p q : pathp i.(Ty i) x y) → pathp i.(pathp i.(Ty i) x y) p q;

let uip = (λ A B Ty x y p q i → p) : UIP_type;

let second-proj = (λ A x y pf i → snd (pf i))
  : Π (A : Set) (x y : A) (pf : pathp i.(Σ(B : Set) * B) (pair A x) (pair A y))
  → pathp i.A x y;

-- Eta!
let eta-test = (λ A B f i → f)
  : Π (A B : Set) (f : Π(_ : A) → B)
  → pathp i.(Π(_ : A) → B) f (λ x → f x);

let pair-eta-test = (λ A B p i → p)
  : Π (A B : Set) (p : Σ(_ : A) × B)
  → pathp i.(Σ(_ : A) × B) p (pair (fst p) (snd p));

-- It computes!
let regularity-test = (λ A p → refl A)
  : Π (A : Set) (p : pathp i.Set A A) (x : A)
  → pathp i.A x (coe 0 1 i.(p i) x);

-- It makes use of Internal Injectivity during evaluation!
let coe-pi-test = (λ A A' B B' p f → coe 0 1 i.(p i) f)
  : Π (A A' B B' : Set) (p : pathp i.Set (Π(_: A) → B) (Π(_: A') → B'))
      (f : Π(_ : A) → B)
  → Π(_ : A') → B';

let app-to-zero = (λ A x y p → p 0)
  : Π (A : Set) (x y : A) (p : pathp i.A x y) → A;

let app-to-one = (λ A x y p → p 1)
  : Π (A : Set) (x y : A) (p : pathp i.A x y) → A;

let fun-with-pairs
  = (λ A P w w' pf →
    pair (λ i → fst (pf i))
         (λ i → com<i> 0 1 j.(P (fst (pf j)))
                  j.(coe 0 j i.(P (fst (pf i))) (snd w))
                  j.(snd (pf j)) (snd w)))
  : ∀ (A : Set) (P : Π(x : A) → Set)
      (w w' : Σ(x : A) * P x) (pf : pathp i.(Σ(x : A) * P x) w w')
  → Σ (p : pathp i.A (fst w) (fst w'))
    * pathp i.(P (fst w')) (coe 0 1 i.(P (p i)) (snd w)) (snd w');

pathp-to-coe-path