(** * Varieties of univalence *)

Require Import HoTT.Basics HoTT.Types.
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 A0 B : Type, A0 <~> B -> A0 = B
H: forall (A0 B : Type) (f : A0 <~> B), equiv_path A0 B (etop A0 B f) = f
A: Type
forall B : Type, IsEquiv (equiv_path A B)
  apply isequiv_from_functor_sigma.
etop: forall A0 B : Type, A0 <~> B -> A0 = B
H: forall (A0 B : Type) (f : A0 <~> B), equiv_path A0 B (etop A0 B f) = f
A: Type
IsEquiv (functor_sigma idmap (equiv_path A))
  srapply isequiv_contr_contr.
etop: forall A0 B : Type, A0 <~> B -> A0 = B
H: forall (A0 B : Type) (f : A0 <~> B), equiv_path A0 B (etop A0 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 A0 B : Type, A0 <~> B -> A0 = B
H: forall (A0 B : Type) (f : A0 <~> B), equiv_path A0 B (etop A0 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 A0 B0 : Type, A0 <~> B0 -> A0 = B0
H: forall (A0 B0 : Type) (f0 : A0 <~> B0), equiv_path A0 B0 (etop A0 B0 f0) = f0
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)
(H0 : (fun x : B => f (g x)) == idmap)
(K0 : (fun x : A => g (f x)) == idmap),
equiv_path A B (etop A B f g H0 K0) == 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)
(H0 : (fun x : B => f (g x)) == idmap)
(K0 : (fun x : A => g (f x)) == idmap),
equiv_path A B (etop A B f g H0 K0) == 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)
(H0 : (fun x : B => f (g x)) == idmap)
(K0 : (fun x : A => g (f x)) == idmap),
equiv_path A B (etop A B f g H0 K0) == 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)
(H0 : (fun x : B => f (g x)) == idmap)
(K0 : (fun x : A => g (f x)) == idmap),
equiv_path A B (etop A B f g H0 K0) == 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)
(H0 : (fun x : B => f (g x)) == idmap)
(K0 : (fun x : A => g (f x)) == idmap),
equiv_path A B (etop A B f g H0 K0) == f
forall A B : Type, A <~> B -> A = B intros A B f.
H: Funext
etop: forall (A0 B0 : Type) (f0 : A0 -> B0) (g : B0 -> A0),
(fun x : B0 => f0 (g x)) == idmap ->
(fun x : A0 => g (f0 x)) == idmap -> A0 = B0
K: forall (A0 B0 : Type) (f0 : A0 -> B0) (g : B0 -> A0)
(H0 : (fun x : B0 => f0 (g x)) == idmap)
(K0 : (fun x : A0 => g (f0 x)) == idmap),
equiv_path A0 B0 (etop A0 B0 f0 g H0 K0) == f0
A, B: Type
f: A <~> B
A = B
    refine (etop A B f f^-1 _ _).
H: Funext
etop: forall (A0 B0 : Type) (f0 : A0 -> B0) (g : B0 -> A0),
(fun x : B0 => f0 (g x)) == idmap ->
(fun x : A0 => g (f0 x)) == idmap -> A0 = B0
K: forall (A0 B0 : Type) (f0 : A0 -> B0) (g : B0 -> A0)
(H0 : (fun x : B0 => f0 (g x)) == idmap)
(K0 : (fun x : A0 => g (f0 x)) == idmap),
equiv_path A0 B0 (etop A0 B0 f0 g H0 K0) == f0
A, B: Type
f: A <~> B
(fun x : B => f (f^-1 x)) == idmap
H: Funext
etop: forall (A0 B0 : Type) (f0 : A0 -> B0) (g : B0 -> A0),
(fun x : B0 => f0 (g x)) == idmap ->
(fun x : A0 => g (f0 x)) == idmap -> A0 = B0
K: forall (A0 B0 : Type) (f0 : A0 -> B0) (g : B0 -> A0)
(H0 : (fun x : B0 => f0 (g x)) == idmap)
(K0 : (fun x : A0 => g (f0 x)) == idmap),
equiv_path A0 B0 (etop A0 B0 f0 g H0 K0) == f0
A, B: Type
f: A <~> B
(fun x : A => f^-1 (f x)) == idmap
    -
H: Funext
etop: forall (A0 B0 : Type) (f0 : A0 -> B0) (g : B0 -> A0),
(fun x : B0 => f0 (g x)) == idmap ->
(fun x : A0 => g (f0 x)) == idmap -> A0 = B0
K: forall (A0 B0 : Type) (f0 : A0 -> B0) (g : B0 -> A0)
(H0 : (fun x : B0 => f0 (g x)) == idmap)
(K0 : (fun x : A0 => g (f0 x)) == idmap),
equiv_path A0 B0 (etop A0 B0 f0 g H0 K0) == f0
A, B: Type
f: A <~> B
(fun x : B => f (f^-1 x)) == idmap intros x; apply eisretr.
    -
H: Funext
etop: forall (A0 B0 : Type) (f0 : A0 -> B0) (g : B0 -> A0),
(fun x : B0 => f0 (g x)) == idmap ->
(fun x : A0 => g (f0 x)) == idmap -> A0 = B0
K: forall (A0 B0 : Type) (f0 : A0 -> B0) (g : B0 -> A0)
(H0 : (fun x : B0 => f0 (g x)) == idmap)
(K0 : (fun x : A0 => g (f0 x)) == idmap),
equiv_path A0 B0 (etop A0 B0 f0 g H0 K0) == f0
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)
(H0 : (fun x : B => f (g x)) == idmap)
(K0 : (fun x : A => g (f x)) == idmap),
equiv_path A B (etop A B f g H0 K0) == 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)
(H0 : (fun x : B => f (g x)) == idmap)
(K0 : (fun x : A => g (f x)) == idmap),
equiv_path A B (etop A B f g H0 K0) == 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 (A0 B0 : Type) (f0 : A0 -> B0) (g : B0 -> A0),
(fun x : B0 => f0 (g x)) == idmap ->
(fun x : A0 => g (f0 x)) == idmap -> A0 = B0
K: forall (A0 B0 : Type) (f0 : A0 -> B0) (g : B0 -> A0)
(H0 : (fun x : B0 => f0 (g x)) == idmap)
(K0 : (fun x : A0 => g (f0 x)) == idmap),
equiv_path A0 B0 (etop A0 B0 f0 g H0 K0) == f0
etop':= fun (A0 B0 : Type) (f0 : A0 <~> B0) =>
etop A0 B0 f0 f0^-1
  ((fun x : B0 => eisretr f0 x) : (fun x : B0 => f0 (f0^-1 x)) == idmap)
  ((fun x : A0 => eissect f0 x) : (fun x : A0 => f0^-1 (f0 x)) == idmap): forall A0 B0 : Type, A0 <~> B0 -> A0 = B0
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 a0 : A => {b : B & f a0 = b})
           (fun a0 : A =>
            (contract vwu {b : B & f a0 = b} (contr_basedpaths (f a0)))^)) @
      flip vwu A B (fun (a0 : A) (b : B) => f a0 = b)) @
     ap sig
       (path_arrow (fun b : B => {a0 : A & f a0 = b}) 
          (fun _ : B => Unit)
          (fun b : B => contract vwu {a0 : A & f a0 = 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 => {a0 : A & f a0 = b}) 
           (fun _ : B => Unit)
           (fun b : B =>
            contract vwu {a0 : A & f a0 = b} (istruncmap_fiber b))))
     (transport idmap (flip vwu A B (fun (a0 : A) (b : B) => f a0 = b))
        (transport idmap
           (ap sig
              (path_arrow (fun _ : A => Unit)
                 (fun a0 : A => {b : B & f a0 = b})
                 (fun a0 : A =>
                  (contract vwu {b : B & f a0 = b} (contr_basedpaths (f a0)))^)))
           (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 => {a0 : A & f a0 = b}) 
        (fun _ : B => Unit)
        (fun b : B => contract vwu {a0 : A & f a0 = b} (istruncmap_fiber b))))
  (transport idmap (flip vwu A B (fun (a0 : A) (b : B) => f a0 = b))
     (transport idmap
        (ap sig
           (path_arrow (fun _ : A => Unit) (fun a0 : A => {b : B & f a0 = b})
              (fun a0 : A =>
               (contract vwu {b : B & f a0 = b} (contr_basedpaths (f a0)))^)))
        (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 => {a0 : A & f a0 = b}) 
        (fun _ : B => Unit)
        (fun b : B => contract vwu {a0 : A & f a0 = b} (istruncmap_fiber b))))
  (transport idmap (flip vwu A B (fun (a0 : A) (b : B) => f a0 = b))
     (transport idmap
        (ap sig
           (path_arrow (fun _ : A => Unit) (fun a0 : A => {b : B & f a0 = b})
              (fun a0 : A =>
               (contract vwu {b : B & f a0 = b} (contr_basedpaths (f a0)))^)))
        (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 => {a0 : A & f a0 = b}) (fun _ : B => Unit)
     (fun b : B => contract vwu {a0 : A & f a0 = b} (istruncmap_fiber b)))
  (transport idmap (flip vwu A B (fun (a0 : A) (b : B) => f a0 = b))
     (transport (fun x : A -> Type => {x0 : _ & x x0})
        (path_arrow (fun _ : A => Unit) (fun a0 : A => {b : B & f a0 = b})
           (fun a0 : A =>
            (contract vwu {b : B & f a0 = b} (contr_basedpaths (f a0)))^))
        (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 => {a0 : A & f a0 = b}) (fun _ : B => Unit)
     (fun b : B => contract vwu {a0 : A & f a0 = b} (istruncmap_fiber b)))
  (transport idmap (flip vwu A B (fun (a0 : A) (b : B) => f a0 = b))
     (a;
     transport (fun x : A -> Type => x a)
       (path_arrow (fun _ : A => Unit) (fun a0 : A => {b : B & f a0 = b})
          (fun a0 : A =>
           (contract vwu {b : B & f a0 = b} (contr_basedpaths (f a0)))^))
       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 (a0 : A) (b : B) => f a0 = b))
  (a;
  transport (fun x : A -> Type => x a)
    (path_arrow (fun _ : A => Unit) (fun a0 : A => {b : B & f a0 = b})
       (fun a0 : A =>
        (contract vwu {b : B & f a0 = b} (contr_basedpaths (f a0)))^))
    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 => {a0 : A & f a0 = b}) (fun _ : B => Unit)
     (fun b : B => contract vwu {a0 : A & f a0 = 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 (a0 : A) (b : B) => f a0 = b))
  (a;
  transport (fun x : A -> Type => x a)
    (path_arrow (fun _ : A => Unit) (fun a0 : A => {b : B & f a0 = b})
       (fun a0 : A =>
        (contract vwu {b : B & f a0 = b} (contr_basedpaths (f a0)))^))
    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 a0 : A => {b : B & f a0 = b})
     (fun a0 : A =>
      (contract vwu {b : B & f a0 = b} (contr_basedpaths (f a0)))^))
  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 => {a0 : A & f a0 = b}) (fun _ : B => Unit)
     (fun b : B => contract vwu {a0 : A & f a0 = b} (istruncmap_fiber b)))
  (transport idmap (flip vwu A B (fun (a0 : A) (b : B) => f a0 = 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 => {a0 : A & f a0 = b}) (fun _ : B => Unit)
     (fun b : B => contract vwu {a0 : A & f a0 = 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 => {a0 : A & f a0 = b}) (fun _ : B => Unit)
     (fun b : B => contract vwu {a0 : A & f a0 = b} (istruncmap_fiber b)))
  (a; 1)) =
(f a; tt)
    apply ap, path_contr. }
Defined.