Stuck.v

Require Import Coq.Program.Basics.
Open Scope program_scope.

(* transportᵖ(p, -) : P(x) → P(y) *)
Definition transport {A : Type} {x y : A} (P : A -> Type) (p : x = y) : P x -> P y :=
  fun (px : P x) => eq_rect x P px y p.

(* (f ~ g) := Π(x:A) f(x) = g(x) *)
Definition homotopy {A : Type} {P : A -> Type} (f g : forall (x : A), P x) : Type :=
  forall (x : A), f x = g x.
Notation "f ~ g" := (homotopy f g) (at level 70, no associativity).

(* isEquiv(f) := (Σ(g:B→A)(f∘g ~ id)) × (Σ(h:B→A)(h∘f ~ id)) *)
Definition isEquiv {A B : Type} f : Type :=
  { g : B -> A & (f ∘ g) ~ id } * { h : B -> A & (h ∘ f) ~ id }.

(* (A ≃ B) := Σ(f:A→B) isEquiv(f) *)
Definition hequiv (A B : Type) : Type := { f : A -> B & isEquiv f }.
Notation "A ≃ B" := (hequiv A B) (at level 70, no associativity).

(* (A ≃ B) → (A = B) *)
(* Note: this isn't the exact univalence axiom, but is a consequence of it *)
Axiom univalence : forall {A B : Type}, A ≃ B -> A = B.

(* negb is an equivalence relation on bool which swaps true and false *)
Definition negb_equiv : bool ≃ bool :=
  let h : (negb ∘ negb) ~ id :=
    fun (x : bool) => match x with | true => eq_refl | false => eq_refl end
  in (existT _ negb (existT _ negb h, existT _ negb h)).

Definition negb_equality : bool = bool :> Type := univalence negb_equiv.
Definition refl_equality : bool = bool :> Type := eq_refl.

(* This expression can be computed to 'true' *)
Definition refl_transport : bool := transport (fun _ => bool) refl_equality true.
Compute refl_transport. (* = true : bool *)

(* Univalence has no computation rule: the expression does not reduce *)
Definition negb_transport : bool := transport (fun _ => bool) negb_equality true.
Compute negb_transport. (* = match univalence ... with | eq_refl => true end : bool *)

(* Note that in the above example, if univalence reduced to eq_refl, then
   negb_transport would result in true. While it makes sense since "true = true",
   that result would not respect the definition of the homotopy equivalence *)

(* HoTT has terms which cannot be reduced to canonical form (this is one example).
   Cubical Type Theory is a type theory which given computation rules to the univalence axiom,
   and as a result has canonical forms for some HoTT examples which do not.
   I think it's still an open problem if CTT has non-canonicalizable expressions. *)