(** * Varieties of univalence *)

Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Idempotents.
Require Import Metatheory.Core.
Local Open Scope path_scope.

(** A weaker form that only asserts that we can make equivalences into paths with a computation rule (no uniqueness rule). *)
Definition WeakUnivalence :=
  { etop : forall A B, (A <~> B) -> (A = B) &
    forall A B (f : A <~> B), equiv_path A B (etop A B f) = f }.

(** The same thing, stated with an incoherent notion of equivalence but a pointwise equality for the computation rule.  *)
Definition IncoherentWeakUnivalence :=
  { etop : forall A B (f : A -> B) (g : B -> A),
      (f o g == idmap) -> (g o f == idmap) -> (A = B) &
    forall A B f g H K, equiv_path A B (etop A B f g H K) == f }.

(** Finally, it even suffices to consider only just a few special cases. This is due to Ian Orton and Andrew Pitts. *)
Record VeryWeakUnivalence :=
  { unit : forall A, A = { a : A & Unit };
    flip : forall A B (C : A -> B -> Type),
        { a : A & { b : B & C a b }} = { b : B & { a : A & C a b }};
    contract : forall A, Contr A -> A = Unit;
    unit_comp : forall A a, transport idmap (unit A) a = (a;tt);
    flip_comp : forall A B C (a:A) (b:B) (c : C a b),
        transport idmap (flip A B C) (a ; (b ; c)) = (b ; (a ; c))
  }.

Theorem WeakUnivalence_implies_Univalence :
  WeakUnivalence -> Univalence_type.
WeakUnivalence -> Univalence_type
Proof.
WeakUnivalence -> Univalence_type
  intros [etop H] A.
etop: forall A B : Type, A <~> B -> A = B
H: forall (A B : Type) (f : A <~> B),
equiv_path A B (etop A B f) = f
A: Type
forall B : Type, IsEquiv (equiv_path A B)
  apply isequiv_from_functor_sigma.
etop: forall A B : Type, A <~> B -> A = B
H: forall (A B : Type) (f : A <~> B),
equiv_path A B (etop A B f) = f
A: Type
IsEquiv (functor_sigma idmap (equiv_path A))
  srapply isequiv_contr_contr.
etop: forall A B : Type, A <~> B -> A = B
H: forall (A B : Type) (f : A <~> B),
equiv_path A B (etop A B f) = f
A: Type
Contr {x : _ & A <~> x}
  srapply (contr_retracttype
            (Build_RetractOf _ _
                             (fun Be => (Be.1 ; equiv_path A Be.1 Be.2))
                             (fun Bf => (Bf.1 ; etop A Bf.1 Bf.2))
                             _)).
etop: forall A B : Type, A <~> B -> A = B
H: forall (A B : Type) (f : A <~> B),
equiv_path A B (etop A B f) = f
A: Type
(fun Be : {x : _ & A = x} =>
 (Be.1; equiv_path A Be.1 Be.2))
o (fun Bf : {x : _ & A <~> x} =>
   (Bf.1; etop A Bf.1 Bf.2)) == idmap
  intros [B f].
etop: forall A B : Type, A <~> B -> A = B
H: forall (A B : Type) (f : A <~> B),
equiv_path A B (etop A B f) = f
A, B: Type
f: A <~> B
(((B; f).1; etop A (B; f).1 (B; f).2).1;
equiv_path A ((B; f).1; etop A (B; f).1 (B; f).2).1
  ((B; f).1; etop A (B; f).1 (B; f).2).2) = 
(B; f)
  refine (path_sigma' (fun B => A <~> B) 1 (H A B f)).
Defined.

(** For this one and the next one, we need to assume funext to start with (so that these forms of univalence, unlike the usual one, probably don't suffice to prove funext from). *)
Theorem IncoherentWeakUnivalence_implies_Univalence `{Funext} :
  IncoherentWeakUnivalence -> Univalence_type.
H: Funext
IncoherentWeakUnivalence -> Univalence_type
Proof.
H: Funext
IncoherentWeakUnivalence -> Univalence_type
  intros [etop K].
H: Funext
etop: forall (A B : Type) (f : A -> B) 
(g : B -> A),
(fun x : B => f (g x)) == idmap ->
(fun x : A => g (f x)) == idmap -> A = B
K: forall (A B : Type) (f : A -> B) 
(g : B -> A) (H : (fun x : B => f (g x)) == idmap)
(K : (fun x : A => g (f x)) == idmap),
equiv_path A B (etop A B f g H K) == f
Univalence_type
  apply WeakUnivalence_implies_Univalence.
H: Funext
etop: forall (A B : Type) (f : A -> B) 
(g : B -> A),
(fun x : B => f (g x)) == idmap ->
(fun x : A => g (f x)) == idmap -> A = B
K: forall (A B : Type) (f : A -> B) 
(g : B -> A) (H : (fun x : B => f (g x)) == idmap)
(K : (fun x : A => g (f x)) == idmap),
equiv_path A B (etop A B f g H K) == f
WeakUnivalence
  transparent assert (etop' : (forall A B, (A <~> B) -> (A = B))).
H: Funext
etop: forall (A B : Type) (f : A -> B) 
(g : B -> A),
(fun x : B => f (g x)) == idmap ->
(fun x : A => g (f x)) == idmap -> A = B
K: forall (A B : Type) (f : A -> B) 
(g : B -> A) (H : (fun x : B => f (g x)) == idmap)
(K : (fun x : A => g (f x)) == idmap),
equiv_path A B (etop A B f g H K) == f
forall A B : Type, A <~> B -> A = B
H: Funext
etop: forall (A B : Type) (f : A -> B) 
(g : B -> A),
(fun x : B => f (g x)) == idmap ->
(fun x : A => g (f x)) == idmap -> A = B
K: forall (A B : Type) (f : A -> B) 
(g : B -> A) (H : (fun x : B => f (g x)) == idmap)
(K : (fun x : A => g (f x)) == idmap),
equiv_path A B (etop A B f g H K) == f
etop':= ?Goal: forall A B : Type, A <~> B -> A = B
WeakUnivalence
  {
H: Funext
etop: forall (A B : Type) (f : A -> B) 
(g : B -> A),
(fun x : B => f (g x)) == idmap ->
(fun x : A => g (f x)) == idmap -> A = B
K: forall (A B : Type) (f : A -> B) 
(g : B -> A) (H : (fun x : B => f (g x)) == idmap)
(K : (fun x : A => g (f x)) == idmap),
equiv_path A B (etop A B f g H K) == f
forall A B : Type, A <~> B -> A = B intros A B f.
H: Funext
etop: forall (A B : Type) (f : A -> B) 
(g : B -> A),
(fun x : B => f (g x)) == idmap ->
(fun x : A => g (f x)) == idmap -> A = B
K: forall (A B : Type) (f : A -> B) 
(g : B -> A) (H : (fun x : B => f (g x)) == idmap)
(K : (fun x : A => g (f x)) == idmap),
equiv_path A B (etop A B f g H K) == f
A, B: Type
f: A <~> B
A = B
    refine (etop A B f f^-1 _ _).
H: Funext
etop: forall (A B : Type) (f : A -> B) 
(g : B -> A),
(fun x : B => f (g x)) == idmap ->
(fun x : A => g (f x)) == idmap -> A = B
K: forall (A B : Type) (f : A -> B) 
(g : B -> A) (H : (fun x : B => f (g x)) == idmap)
(K : (fun x : A => g (f x)) == idmap),
equiv_path A B (etop A B f g H K) == f
A, B: Type
f: A <~> B
(fun x : B => f (f^-1 x)) == idmap
H: Funext
etop: forall (A B : Type) (f : A -> B) 
(g : B -> A),
(fun x : B => f (g x)) == idmap ->
(fun x : A => g (f x)) == idmap -> A = B
K: forall (A B : Type) (f : A -> B) 
(g : B -> A) (H : (fun x : B => f (g x)) == idmap)
(K : (fun x : A => g (f x)) == idmap),
equiv_path A B (etop A B f g H K) == f
A, B: Type
f: A <~> B
(fun x : A => f^-1 (f x)) == idmap
    -
H: Funext
etop: forall (A B : Type) (f : A -> B) 
(g : B -> A),
(fun x : B => f (g x)) == idmap ->
(fun x : A => g (f x)) == idmap -> A = B
K: forall (A B : Type) (f : A -> B) 
(g : B -> A) (H : (fun x : B => f (g x)) == idmap)
(K : (fun x : A => g (f x)) == idmap),
equiv_path A B (etop A B f g H K) == f
A, B: Type
f: A <~> B
(fun x : B => f (f^-1 x)) == idmap intros x; apply eisretr.
    -
H: Funext
etop: forall (A B : Type) (f : A -> B) 
(g : B -> A),
(fun x : B => f (g x)) == idmap ->
(fun x : A => g (f x)) == idmap -> A = B
K: forall (A B : Type) (f : A -> B) 
(g : B -> A) (H : (fun x : B => f (g x)) == idmap)
(K : (fun x : A => g (f x)) == idmap),
equiv_path A B (etop A B f g H K) == f
A, B: Type
f: A <~> B
(fun x : A => f^-1 (f x)) == idmap intros x; apply eissect. }
H: Funext
etop: forall (A B : Type) (f : A -> B) 
(g : B -> A),
(fun x : B => f (g x)) == idmap ->
(fun x : A => g (f x)) == idmap -> A = B
K: forall (A B : Type) (f : A -> B) 
(g : B -> A) (H : (fun x : B => f (g x)) == idmap)
(K : (fun x : A => g (f x)) == idmap),
equiv_path A B (etop A B f g H K) == f
etop':= fun (A B : Type) (f : A <~> B) =>
etop A B f f^-1
  ((fun x : B => eisretr f x)
   :
   (fun x : B => f (f^-1 x)) == idmap)
  ((fun x : A => eissect f x)
   :
   (fun x : A => f^-1 (f x)) == idmap): forall A B : Type, A <~> B -> A = B
WeakUnivalence
  exists etop'.
H: Funext
etop: forall (A B : Type) (f : A -> B) 
(g : B -> A),
(fun x : B => f (g x)) == idmap ->
(fun x : A => g (f x)) == idmap -> A = B
K: forall (A B : Type) (f : A -> B) 
(g : B -> A) (H : (fun x : B => f (g x)) == idmap)
(K : (fun x : A => g (f x)) == idmap),
equiv_path A B (etop A B f g H K) == f
etop':= fun (A B : Type) (f : A <~> B) =>
etop A B f f^-1
  ((fun x : B => eisretr f x)
   :
   (fun x : B => f (f^-1 x)) == idmap)
  ((fun x : A => eissect f x)
   :
   (fun x : A => f^-1 (f x)) == idmap): forall A B : Type, A <~> B -> A = B
forall (A B : Type) (f : A <~> B),
equiv_path A B (etop' A B f) = f
  intros A B f.
H: Funext
etop: forall (A B : Type) (f : A -> B) 
(g : B -> A),
(fun x : B => f (g x)) == idmap ->
(fun x : A => g (f x)) == idmap -> A = B
K: forall (A B : Type) (f : A -> B) 
(g : B -> A) (H : (fun x : B => f (g x)) == idmap)
(K : (fun x : A => g (f x)) == idmap),
equiv_path A B (etop A B f g H K) == f
etop':= fun (A B : Type) (f : A <~> B) =>
etop A B f f^-1
  ((fun x : B => eisretr f x)
   :
   (fun x : B => f (f^-1 x)) == idmap)
  ((fun x : A => eissect f x)
   :
   (fun x : A => f^-1 (f x)) == idmap): forall A B : Type, A <~> B -> A = B
A, B: Type
f: A <~> B
equiv_path A B (etop' A B f) = f
  apply path_equiv, path_arrow, K.
Defined.

Theorem VeryWeakUnivalence_implies_Univalence `{Funext} :
  VeryWeakUnivalence -> Univalence_type.
H: Funext
VeryWeakUnivalence -> Univalence_type
Proof.
H: Funext
VeryWeakUnivalence -> Univalence_type
  intros vwu.
H: Funext
vwu: VeryWeakUnivalence
Univalence_type apply WeakUnivalence_implies_Univalence.
H: Funext
vwu: VeryWeakUnivalence
WeakUnivalence
  simple refine (_;_).
H: Funext
vwu: VeryWeakUnivalence
forall A B : Type, A <~> B -> A = B
H: Funext
vwu: VeryWeakUnivalence
(fun etop : forall A B : Type, A <~> B -> A = B =>
 forall (A B : Type) (f : A <~> B),
 equiv_path A B (etop A B f) = f) ?proj1
  {
H: Funext
vwu: VeryWeakUnivalence
forall A B : Type, A <~> B -> A = B intros A B f.
H: Funext
vwu: VeryWeakUnivalence
A, B: Type
f: A <~> B
A = B
    refine (unit vwu A @ _ @ (unit vwu B)^).
H: Funext
vwu: VeryWeakUnivalence
A, B: Type
f: A <~> B
{_ : A & Unit} = {_ : B & Unit}
    refine (_ @ flip vwu A B (fun a b => f a = b) @ _).
H: Funext
vwu: VeryWeakUnivalence
A, B: Type
f: A <~> B
{_ : A & Unit} = {a : A & {b : B & f a = b}}
H: Funext
vwu: VeryWeakUnivalence
A, B: Type
f: A <~> B
{b : B & {a : A & f a = b}} = {_ : B & Unit}
    -
H: Funext
vwu: VeryWeakUnivalence
A, B: Type
f: A <~> B
{_ : A & Unit} = {a : A & {b : B & f a = b}} apply ap, path_arrow; intros a.
H: Funext
vwu: VeryWeakUnivalence
A, B: Type
f: A <~> B
a: A
Unit = {b : B & f a = b}
      symmetry; rapply (contract vwu).
    -
H: Funext
vwu: VeryWeakUnivalence
A, B: Type
f: A <~> B
{b : B & {a : A & f a = b}} = {_ : B & Unit} apply ap, path_arrow; intros b.
H: Funext
vwu: VeryWeakUnivalence
A, B: Type
f: A <~> B
b: B
{a : A & f a = b} = Unit
      apply (contract vwu); exact _. }
H: Funext
vwu: VeryWeakUnivalence
(fun etop : forall A B : Type, A <~> B -> A = B =>
 forall (A B : Type) (f : A <~> B),
 equiv_path A B (etop A B f) = f)
  (fun (A B : Type) (f : A <~> B) =>
   (unit vwu A @
    ((ap sig
        (path_arrow (fun _ : A => Unit)
           (fun a : A => {b : B & f a = b})
           ((fun a : A =>
             (contract vwu {b : B & f a = b}
                (contr_basedpaths (f a)))^)
            :
            (fun _ : A => Unit) ==
            (fun a : A => {b : B & f a = b}))) @
      flip vwu A B (fun (a : A) (b : B) => f a = b)) @
     ap sig
       (path_arrow (fun b : B => {a : A & f a = b})
          (fun _ : B => Unit)
          ((fun b : B =>
            contract vwu {a : A & f a = b}
              (istruncmap_fiber b))
           :
           (fun b : B => {a : A & f a = b}) ==
           (fun _ : B => Unit))))) @ (unit vwu B)^)
  {
H: Funext
vwu: VeryWeakUnivalence
(fun etop : forall A B : Type, A <~> B -> A = B =>
 forall (A B : Type) (f : A <~> B),
 equiv_path A B (etop A B f) = f)
  (fun (A B : Type) (f : A <~> B) =>
   (unit vwu A @
    ((ap sig
        (path_arrow (fun _ : A => Unit)
           (fun a : A => {b : B & f a = b})
           ((fun a : A =>
             (contract vwu {b : B & f a = b}
                (contr_basedpaths (f a)))^)
            :
            (fun _ : A => Unit) ==
            (fun a : A => {b : B & f a = b}))) @
      flip vwu A B (fun (a : A) (b : B) => f a = b)) @
     ap sig
       (path_arrow (fun b : B => {a : A & f a = b})
          (fun _ : B => Unit)
          ((fun b : B =>
            contract vwu {a : A & f a = b}
              (istruncmap_fiber b))
           :
           (fun b : B => {a : A & f a = b}) ==
           (fun _ : B => Unit))))) @ (unit vwu B)^) intros A B f.
H: Funext
vwu: VeryWeakUnivalence
A, B: Type
f: A <~> B
equiv_path A B
  ((unit vwu A @
    ((ap sig
        (path_arrow (fun _ : A => Unit)
           (fun a : A => {b : B & f a = b})
           (fun a : A =>
            (contract vwu {b : B & f a = b}
               (contr_basedpaths (f a)))^)) @
      flip vwu A B (fun (a : A) (b : B) => f a = b)) @
     ap sig
       (path_arrow (fun b : B => {a : A & f a = b})
          (fun _ : B => Unit)
          (fun b : B =>
           contract vwu {a : A & f a = b}
             (istruncmap_fiber b))))) @ (unit vwu B)^) =
f
    apply path_equiv, path_arrow; intros a; cbn.
H: Funext
vwu: VeryWeakUnivalence
A, B: Type
f: A <~> B
a: A
transport idmap
  ((unit vwu A @
    ((ap sig
        (path_arrow (fun _ : A => Unit)
           (fun a : A => {b : B & f a = b})
           (fun a : A =>
            (contract vwu {b : B & f a = b}
               (contr_basedpaths (f a)))^)) @
      flip vwu A B (fun (a : A) (b : B) => f a = b)) @
     ap sig
       (path_arrow (fun b : B => {a : A & f a = b})
          (fun _ : B => Unit)
          (fun b : B =>
           contract vwu {a : A & f a = b}
             (istruncmap_fiber b))))) @ (unit vwu B)^)
  a = f a
    rewrite !transport_pp.
H: Funext
vwu: VeryWeakUnivalence
A, B: Type
f: A <~> B
a: A
transport idmap (unit vwu B)^
  (transport idmap
     (ap sig
        (path_arrow (fun b : B => {a : A & f a = b})
           (fun _ : B => Unit)
           (fun b : B =>
            contract vwu {a : A & f a = b}
              (istruncmap_fiber b))))
     (transport idmap
        (flip vwu A B (fun (a : A) (b : B) => f a = b))
        (transport idmap
           (ap sig
              (path_arrow (fun _ : A => Unit)
                 (fun a : A => {b : B & f a = b})
                 (fun a : A =>
                  (contract vwu {b : B & f a = b}
                     (contr_basedpaths (f a)))^)))
           (transport idmap (unit vwu A) a)))) = f a
    refine (moveR_transport_V idmap (unit vwu B) _ (f a) _).
H: Funext
vwu: VeryWeakUnivalence
A, B: Type
f: A <~> B
a: A
transport idmap
  (ap sig
     (path_arrow (fun b : B => {a : A & f a = b})
        (fun _ : B => Unit)
        (fun b : B =>
         contract vwu {a : A & f a = b}
           (istruncmap_fiber b))))
  (transport idmap
     (flip vwu A B (fun (a : A) (b : B) => f a = b))
     (transport idmap
        (ap sig
           (path_arrow (fun _ : A => Unit)
              (fun a : A => {b : B & f a = b})
              (fun a : A =>
               (contract vwu {b : B & f a = b}
                  (contr_basedpaths (f a)))^)))
        (transport idmap (unit vwu A) a))) =
transport idmap (unit vwu B) (f a)
    rewrite !(unit_comp vwu).
H: Funext
vwu: VeryWeakUnivalence
A, B: Type
f: A <~> B
a: A
transport idmap
  (ap sig
     (path_arrow (fun b : B => {a : A & f a = b})
        (fun _ : B => Unit)
        (fun b : B =>
         contract vwu {a : A & f a = b}
           (istruncmap_fiber b))))
  (transport idmap
     (flip vwu A B (fun (a : A) (b : B) => f a = b))
     (transport idmap
        (ap sig
           (path_arrow (fun _ : A => Unit)
              (fun a : A => {b : B & f a = b})
              (fun a : A =>
               (contract vwu {b : B & f a = b}
                  (contr_basedpaths (f a)))^)))
        (a; tt))) = (f a; tt)
    rewrite <- !(transport_compose idmap sig).
H: Funext
vwu: VeryWeakUnivalence
A, B: Type
f: A <~> B
a: A
transport (fun x : B -> Type => {x0 : _ & x x0})
  (path_arrow (fun b : B => {a : A & f a = b})
     (fun _ : B => Unit)
     (fun b : B =>
      contract vwu {a : A & f a = b}
        (istruncmap_fiber b)))
  (transport idmap
     (flip vwu A B (fun (a : A) (b : B) => f a = b))
     (transport (fun x : A -> Type => {x0 : _ & x x0})
        (path_arrow (fun _ : A => Unit)
           (fun a : A => {b : B & f a = b})
           (fun a : A =>
            (contract vwu {b : B & f a = b}
               (contr_basedpaths (f a)))^)) (a; tt))) =
(f a; tt)
    rewrite (transport_sigma' (C := fun P (a0:A) => P a0)); cbn.
H: Funext
vwu: VeryWeakUnivalence
A, B: Type
f: A <~> B
a: A
transport (fun x : B -> Type => {x0 : _ & x x0})
  (path_arrow (fun b : B => {a : A & f a = b})
     (fun _ : B => Unit)
     (fun b : B =>
      contract vwu {a : A & f a = b}
        (istruncmap_fiber b)))
  (transport idmap
     (flip vwu A B (fun (a : A) (b : B) => f a = b))
     (a;
     transport (fun x : A -> Type => x a)
       (path_arrow (fun _ : A => Unit)
          (fun a : A => {b : B & f a = b})
          (fun a : A =>
           (contract vwu {b : B & f a = b}
              (contr_basedpaths (f a)))^)) tt)) =
(f a; tt)
    refine (ap _ _ @ _).
H: Funext
vwu: VeryWeakUnivalence
A, B: Type
f: A <~> B
a: A
transport idmap
  (flip vwu A B (fun (a : A) (b : B) => f a = b))
  (a;
  transport (fun x : A -> Type => x a)
    (path_arrow (fun _ : A => Unit)
       (fun a : A => {b : B & f a = b})
       (fun a : A =>
        (contract vwu {b : B & f a = b}
           (contr_basedpaths (f a)))^)) tt) = ?Goal
H: Funext
vwu: VeryWeakUnivalence
A, B: Type
f: A <~> B
a: A
transport (fun x : B -> Type => {x0 : _ & x x0})
  (path_arrow (fun b : B => {a : A & f a = b})
     (fun _ : B => Unit)
     (fun b : B =>
      contract vwu {a : A & f a = b}
        (istruncmap_fiber b))) ?Goal = (f a; tt)
    1:{
H: Funext
vwu: VeryWeakUnivalence
A, B: Type
f: A <~> B
a: A
transport idmap
  (flip vwu A B (fun (a : A) (b : B) => f a = b))
  (a;
  transport (fun x : A -> Type => x a)
    (path_arrow (fun _ : A => Unit)
       (fun a : A => {b : B & f a = b})
       (fun a : A =>
        (contract vwu {b : B & f a = b}
           (contr_basedpaths (f a)))^)) tt) = ?Goal apply ap, ap.
H: Funext
vwu: VeryWeakUnivalence
A, B: Type
f: A <~> B
a: A
transport (fun x : A -> Type => x a)
  (path_arrow (fun _ : A => Unit)
     (fun a : A => {b : B & f a = b})
     (fun a : A =>
      (contract vwu {b : B & f a = b}
         (contr_basedpaths (f a)))^)) tt = ?y
        exact (path_contr _ (f a ; 1)). }
H: Funext
vwu: VeryWeakUnivalence
A, B: Type
f: A <~> B
a: A
transport (fun x : B -> Type => {x0 : _ & x x0})
  (path_arrow (fun b : B => {a : A & f a = b})
     (fun _ : B => Unit)
     (fun b : B =>
      contract vwu {a : A & f a = b}
        (istruncmap_fiber b)))
  (transport idmap
     (flip vwu A B (fun (a : A) (b : B) => f a = b))
     (a; f a; 1)) = (f a; tt)
    rewrite (flip_comp vwu).
H: Funext
vwu: VeryWeakUnivalence
A, B: Type
f: A <~> B
a: A
transport (fun x : B -> Type => {x0 : _ & x x0})
  (path_arrow (fun b : B => {a : A & f a = b})
     (fun _ : B => Unit)
     (fun b : B =>
      contract vwu {a : A & f a = b}
        (istruncmap_fiber b))) (f a; a; 1) = (f a; tt)
    rewrite transport_sigma'; cbn.
H: Funext
vwu: VeryWeakUnivalence
A, B: Type
f: A <~> B
a: A
(f a;
transport (fun x : B -> Type => x (f a))
  (path_arrow (fun b : B => {a : A & f a = b})
     (fun _ : B => Unit)
     (fun b : B =>
      contract vwu {a : A & f a = b}
        (istruncmap_fiber b))) (a; 1)) = (f a; tt)
    apply ap, path_contr. }
Defined.