-- Equality with an explicit domain
let
  Eq : (A : Type) (x y : A) -> Type;
  Eq A x y = x == y;

-- Identity function with an explicit domain
-- (works as a type annotation)
let
  the : (A : Type) -> A -> A;
  the A x = x;

-- Singleton types
-- The subtype of A generated by "being equal to x : A"
let
  singl : (A : Type) (x : A) -> Type;
  singl A x = (y : A) * x == y;

-- Singletons are contractible
let
  singlC : {A : Type} {a b : A} (p : a == b) -> Eq (singl A a) (a, refl) (b, p);
  singlC p = (p, ());

-- Substitution follows from transport + congruence
-- (just transport by the congruence under P)
let
  subst : {A : Type} (P : A -> Type) {x y : A} (p : x == y) -> P x -> P y;
  subst P path px = coe (cong P path) px;

let
  coe2 : {A B : Type} (p : A == B) → A → B;
  coe2 p = subst (λ x → x) p;

-- Based path induction follows from contractibility of singletons +
-- substitution
let
  J : {A : Type} (a : A) (P : (b : A) -> a == b -> Type)
           (d : P a refl) (b : A) (p : a == b) -> P b p;
  J {A} a P d b p =
    subst {singl A a} (λ y → P y.1 y.2) (singlC p) d;

let
  JComp : {A : Type} (a : A) (P : (b : A) -> a == b -> Type)
               (d : P a refl)
             → J {A} a P d a refl == d;
  JComp {A} a P d = refl;

-- Symmetry follows from axiom J
let
  symm : {A : Type} {x y : A} (p : x == y) -> y == x;
  symm {A} {x} {y} p = J x (λ y p -> y == x) refl y p;

let
  symIsRefl : {A : Type} {a : A} → symm (refl {A} {a}) == refl {A} {a};
  symIsRefl = refl;

let
  isContr : Type -> Type;
  isContr A = (x : A) * (y : A) -> y == x;

let
  comp : {A : Type} {a b c : A} → a == b → b == c → a == c;
  comp {A} {a} p q = subst (λ x → a == x) q (subst (λ x → a == x) p (refl {A} {a}));

let
  trans : {A : Type} {a b c : A} → b == c → a == b → a == c;
  trans {A} {a} p q = comp q p;

let
  transSym : {A : Type} {a : A} → (p : a == a) → comp p (symm p) == refl;
  transSym p = refl;

let
  existsOne : (A : Type) (B : A -> Type) -> ((x : A) × B x) -> isContr A -> (x : A) -> B x;
  existsOne A B prf contr it =
    subst B (comp (contr.2 prf.1) (sym (contr.2 it))) prf.2;

let
  indOne : (P : ⊤ -> Type) -> P () -> (x : ⊤) -> P x;
  indOne P p x = subst P () p;

let
  false : Type;
  false = (A : Type) → A;

let
  exFalso : (P : Type) -> false -> P;
  exFalso P f = f P;

let
  funExt : {A : Type} {B : A -> Type} {f g : (x : A) -> B x}
        -> ((x : A) -> f x == g x) -> f == g;
  funExt p = p;

let
  hfunext : {A : Type} {B : A -> Type} {f g : (x : A) -> B x}
        -> ((x : A) -> f x == g x) == (f == g);
  hfunext = refl;

let
  allAbsurd : {A : Type} (f g : false -> A) -> f == g;
  allAbsurd f g x = exFalso (f x == g x) x;

let
  coerceR1 : {A : Type}
           → Eq (A == A → A → A)
                (λ p x → coe {A} {A} p x)
                (λ x y → y);
  coerceR1 = refl;

let
  K : {A : Type} {x : A} (P : x == x → Type)
    → P refl → (p : x == x) → P p;
  K P p path = subst P (the (refl == path) ()) p;

let
  foo : {A : Type} {B : A -> Type} {f : (x : A) -> B x}
         -> Eq (f == f) refl (λ x → refl);
  foo = K (λ e → (refl {_} {f}) == e) refl (λ x → refl);

let
  coh : {A : Type} (p : A == A) (x : A) → coe p == (λ x → x);
  coh path elem x = refl;

let
  coh2 : {A : Type} (p : A == A) (x : A) → coe p x == x;
  coh2 path elem = K (λ path → coe {A} {A} path elem == elem) refl path;

-- let
--   cohsAgree : {A : Type} (p : A == A) (x : A) → coh {A} p x == coh2 {A} p x;
--   cohsAgree path elem = refl;

let
  congComp : {A B : Type} (f : A -> B) {x : A}
          -> cong f (refl {A} {x}) == refl {B} {f x};
  congComp f = refl;

coe