Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import HFiber.
Require Import Truncations.
Require Import Universes.BAut.

Local Open Scope trunc_scope.
Local Open Scope path_scope.

(** * Rigid types *)

Class IsRigid (A : Type) := 
  path_aut_rigid : forall f g : A <~> A, f == g.

(** Assuming funext, rigidity is equivalent to contractibility of [A <~> A]. *)

Instance contr_aut_rigid `{Funext} (A : Type) `{IsRigid A}
  : Contr (A <~> A).
H: Funext
A: Type
H0: IsRigid A
Contr (A <~> A)
Proof.
H: Funext
A: Type
H0: IsRigid A
Contr (A <~> A)
  apply (Build_Contr _ equiv_idmap).
H: Funext
A: Type
H0: IsRigid A
forall y : A <~> A, 1%equiv = y
  intros f; apply path_equiv, path_arrow, path_aut_rigid.
Defined.

(** Assuming univalence, rigidity is equivalent to contractibility of [BAut A]. *)

Instance contr_baut_rigid `{Univalence} {A : Type} `{IsRigid A}
  : Contr (BAut A).
H: Univalence
A: Type
H0: IsRigid A
Contr (BAut A)
Proof.
H: Univalence
A: Type
H0: IsRigid A
Contr (BAut A)
  refine (contr_change_center (point (BAut A))).
H: Univalence
A: Type
H0: IsRigid A
Contr (BAut A)
  refine (contr_trunc_conn (Tr 0)).
H: Univalence
A: Type
H0: IsRigid A
In (Tr 0) (BAut A)
  apply istrunc_S.
H: Univalence
A: Type
H0: IsRigid A
is_mere_relation (BAut A) paths
  intros Z W; baut_reduce.
H: Univalence
A: Type
H0: IsRigid A
IsHProp (point (BAut A) = point (BAut A))
  exact (istrunc_equiv_istrunc (n := -1) (A <~> A)
                      (path_baut (point (BAut A)) (point (BAut A)))).
Defined.

Definition rigid_contr_Baut `{Univalence} {A : Type} `{Contr (BAut A)}
  : IsRigid A.
H: Univalence
A: Type
Contr0: Contr (BAut A)
IsRigid A
Proof.
H: Univalence
A: Type
Contr0: Contr (BAut A)
IsRigid A
  unfold IsRigid.
H: Univalence
A: Type
Contr0: Contr (BAut A)
forall f g : A <~> A, f == g
  equiv_intro ((path_baut (point (BAut A)) (point (BAut A)))^-1) f.
H: Univalence
A: Type
Contr0: Contr (BAut A)
f: point (BAut A) = point (BAut A)
forall g : A <~> A,
(path_baut (point (BAut A)) (point (BAut A)))^-1 f ==
g
  equiv_intro ((path_baut (point (BAut A)) (point (BAut A)))^-1) g.
H: Univalence
A: Type
Contr0: Contr (BAut A)
f, g: point (BAut A) = point (BAut A)
(path_baut (point (BAut A)) (point (BAut A)))^-1 f ==
(path_baut (point (BAut A)) (point (BAut A)))^-1 g
  apply ap10, ap, ap, path_contr.
Defined.

(** ** HProps are rigid *)

Instance rigid_ishprop
       (A : Type) `{IsHProp A} : IsRigid A.
A: Type
IsHProp0: IsHProp A
IsRigid A
Proof.
A: Type
IsHProp0: IsHProp A
IsRigid A
  intros f g x; apply path_ishprop.
Defined.

(** ** Equivalences of BAut *)

(** Under a truncatedness/connectedness assumption, multiplying by a rigid type doesn't change the automorphism oo-group. *)

(** A lemma: a "monoid homomorphism up to homotopy" between endomorphism monoids restricts to automorphism groups. *)
Definition aut_homomorphism_end `{Funext} {X Y : Type}
           (M : (X -> X) -> (Y -> Y))
           (Mid : M idmap == idmap)
           (MC : forall f g, M (g o f) == M g o M f)
  : (X <~> X) -> (Y <~> Y).
H: Funext
X, Y: Type
M: (X -> X) -> Y -> Y
Mid: M idmap == idmap
MC: forall f g : X -> X, M (g o f) == M g o M f
X <~> X -> Y <~> Y
Proof.
H: Funext
X, Y: Type
M: (X -> X) -> Y -> Y
Mid: M idmap == idmap
MC: forall f g : X -> X, M (g o f) == M g o M f
X <~> X -> Y <~> Y
  assert (MS : forall f g, g o f == idmap -> (M g) o (M f) == idmap).
H: Funext
X, Y: Type
M: (X -> X) -> Y -> Y
Mid: M idmap == idmap
MC: forall f g : X -> X, M (g o f) == M g o M f
forall f g : X -> X,
(fun x : X => g (f x)) == idmap ->
(fun x : Y => M g (M f x)) == idmap
H: Funext
X, Y: Type
M: (X -> X) -> Y -> Y
Mid: M idmap == idmap
MC: forall f g : X -> X, M (g o f) == M g o M f
MS: forall f g : X -> X,
g o f == idmap -> M g o M f == idmap
X <~> X -> Y <~> Y
  {
H: Funext
X, Y: Type
M: (X -> X) -> Y -> Y
Mid: M idmap == idmap
MC: forall f g : X -> X, M (g o f) == M g o M f
forall f g : X -> X,
(fun x : X => g (f x)) == idmap ->
(fun x : Y => M g (M f x)) == idmap intros g f s x.
H: Funext
X, Y: Type
M: (X -> X) -> Y -> Y
Mid: M idmap == idmap
MC: forall f g : X -> X, M (g o f) == M g o M f
g, f: X -> X
s: (fun x : X => f (g x)) == idmap
x: Y
M f (M g x) = x
    transitivity (M (f o g) x).
H: Funext
X, Y: Type
M: (X -> X) -> Y -> Y
Mid: M idmap == idmap
MC: forall f g : X -> X, M (g o f) == M g o M f
g, f: X -> X
s: (fun x : X => f (g x)) == idmap
x: Y
M f (M g x) = M (f o g) x
H: Funext
X, Y: Type
M: (X -> X) -> Y -> Y
Mid: M idmap == idmap
MC: forall f g : X -> X, M (g o f) == M g o M f
g, f: X -> X
s: (fun x : X => f (g x)) == idmap
x: Y
M (f o g) x = x
    +
H: Funext
X, Y: Type
M: (X -> X) -> Y -> Y
Mid: M idmap == idmap
MC: forall f g : X -> X, M (g o f) == M g o M f
g, f: X -> X
s: (fun x : X => f (g x)) == idmap
x: Y
M f (M g x) = M (f o g) x symmetry.
H: Funext
X, Y: Type
M: (X -> X) -> Y -> Y
Mid: M idmap == idmap
MC: forall f g : X -> X, M (g o f) == M g o M f
g, f: X -> X
s: (fun x : X => f (g x)) == idmap
x: Y
M (f o g) x = M f (M g x) exact (MC g f x).
    +
H: Funext
X, Y: Type
M: (X -> X) -> Y -> Y
Mid: M idmap == idmap
MC: forall f g : X -> X, M (g o f) == M g o M f
g, f: X -> X
s: (fun x : X => f (g x)) == idmap
x: Y
M (f o g) x = x transitivity (M idmap x).
H: Funext
X, Y: Type
M: (X -> X) -> Y -> Y
Mid: M idmap == idmap
MC: forall f g : X -> X, M (g o f) == M g o M f
g, f: X -> X
s: (fun x : X => f (g x)) == idmap
x: Y
M (f o g) x = M idmap x
H: Funext
X, Y: Type
M: (X -> X) -> Y -> Y
Mid: M idmap == idmap
MC: forall f g : X -> X, M (g o f) == M g o M f
g, f: X -> X
s: (fun x : X => f (g x)) == idmap
x: Y
M idmap x = x
      *
H: Funext
X, Y: Type
M: (X -> X) -> Y -> Y
Mid: M idmap == idmap
MC: forall f g : X -> X, M (g o f) == M g o M f
g, f: X -> X
s: (fun x : X => f (g x)) == idmap
x: Y
M (f o g) x = M idmap x apply ap10, ap, path_arrow.
H: Funext
X, Y: Type
M: (X -> X) -> Y -> Y
Mid: M idmap == idmap
MC: forall f g : X -> X, M (g o f) == M g o M f
g, f: X -> X
s: (fun x : X => f (g x)) == idmap
x: Y
(fun x : X => f (g x)) == idmap
        intros y; apply s.
      *
H: Funext
X, Y: Type
M: (X -> X) -> Y -> Y
Mid: M idmap == idmap
MC: forall f g : X -> X, M (g o f) == M g o M f
g, f: X -> X
s: (fun x : X => f (g x)) == idmap
x: Y
M idmap x = x apply Mid. }
H: Funext
X, Y: Type
M: (X -> X) -> Y -> Y
Mid: M idmap == idmap
MC: forall f g : X -> X, M (g o f) == M g o M f
MS: forall f g : X -> X,
g o f == idmap -> M g o M f == idmap
X <~> X -> Y <~> Y
  assert (ME : (forall f, IsEquiv f -> IsEquiv (M f))).
H: Funext
X, Y: Type
M: (X -> X) -> Y -> Y
Mid: M idmap == idmap
MC: forall f g : X -> X, M (g o f) == M g o M f
MS: forall f g : X -> X,
g o f == idmap -> M g o M f == idmap
forall f : X -> X, IsEquiv f -> IsEquiv (M f)
H: Funext
X, Y: Type
M: (X -> X) -> Y -> Y
Mid: M idmap == idmap
MC: forall f g : X -> X, M (g o f) == M g o M f
MS: forall f g : X -> X,
g o f == idmap -> M g o M f == idmap
ME: forall f : X -> X, IsEquiv f -> IsEquiv (M f)
X <~> X -> Y <~> Y
  {
H: Funext
X, Y: Type
M: (X -> X) -> Y -> Y
Mid: M idmap == idmap
MC: forall f g : X -> X, M (g o f) == M g o M f
MS: forall f g : X -> X,
g o f == idmap -> M g o M f == idmap
forall f : X -> X, IsEquiv f -> IsEquiv (M f) intros f ?.
H: Funext
X, Y: Type
M: (X -> X) -> Y -> Y
Mid: M idmap == idmap
MC: forall f g : X -> X, M (g o f) == M g o M f
MS: forall f g : X -> X,
g o f == idmap -> M g o M f == idmap
f: X -> X
X0: IsEquiv f
IsEquiv (M f)
    refine (isequiv_adjointify (M f) (M f^-1) _ _);
      apply MS; [ apply eisretr | apply eissect ]. }
H: Funext
X, Y: Type
M: (X -> X) -> Y -> Y
Mid: M idmap == idmap
MC: forall f g : X -> X, M (g o f) == M g o M f
MS: forall f g : X -> X,
g o f == idmap -> M g o M f == idmap
ME: forall f : X -> X, IsEquiv f -> IsEquiv (M f)
X <~> X -> Y <~> Y
  exact (fun f => (Build_Equiv _ _ (M f) (ME f _))).
Defined.

Definition baut_prod_rigid_equiv `{Univalence}
           (X A : Type) (n : trunc_index)
           `{IsTrunc n.+1 X} `{IsRigid A} `{IsConnected n.+1 A}
  : BAut X <~> BAut (X * A).
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
BAut X <~> BAut (X * A)
Proof.
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
BAut X <~> BAut (X * A)
  refine (Build_Equiv _ _ (baut_prod_r X A) _).
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
IsEquiv (baut_prod_r X A)
  apply isequiv_surj_emb.
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
IsConnMap (Tr (-1)) (baut_prod_r X A)
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
IsEmbedding (baut_prod_r X A)
  {
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
IsConnMap (Tr (-1)) (baut_prod_r X A) apply BuildIsSurjection; intros Z.
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
Z: BAut (X * A)
merely (hfiber (baut_prod_r X A) Z)
    baut_reduce.
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
merely
  (hfiber (baut_prod_r X A) (point (BAut (X * A))))
    refine (tr (point _ ; _)).
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
baut_prod_r X A (point (BAut X)) =
point (BAut (X * A))
    apply path_sigma_hprop; reflexivity. }
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
IsEmbedding (baut_prod_r X A)
  {
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
IsEmbedding (baut_prod_r X A) apply isembedding_isequiv_ap.
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
forall x y : BAut X, IsEquiv (ap (baut_prod_r X A))
    intros Z W.
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
Z, W: BAut X
IsEquiv (ap (baut_prod_r X A))
    pose (L := fun e : Z <~> W => equiv_functor_prod_r (B := A) e).
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
Z, W: BAut X
L:= fun e : Z <~> W => equiv_functor_prod_r e: Z <~> W -> Z * A <~> W * A
IsEquiv (ap (baut_prod_r X A))
    refine (isequiv_commsq
             L (ap (baut_prod_r X A))
             (path_baut Z W)
             (path_baut (baut_prod_r X A Z) (baut_prod_r X A W))
             (fun e => (ap_baut_prod_r X A e)^)).
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
Z, W: BAut X
L:= fun e : Z <~> W => equiv_functor_prod_r e: Z <~> W -> Z * A <~> W * A
IsEquiv L
    refine ((isconnected_elim (Tr (-1)) (A := A) _ _).1).
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
Z, W: BAut X
L:= fun e : Z <~> W => equiv_functor_prod_r e: Z <~> W -> Z * A <~> W * A
IsConnected (Tr (-1)) A
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
Z, W: BAut X
L:= fun e : Z <~> W => equiv_functor_prod_r e: Z <~> W -> Z * A <~> W * A
A -> IsEquiv L
    {
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
Z, W: BAut X
L:= fun e : Z <~> W => equiv_functor_prod_r e: Z <~> W -> Z * A <~> W * A
IsConnected (Tr (-1)) A rapply contr_inhabited_hprop.
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
Z, W: BAut X
L:= fun e : Z <~> W => equiv_functor_prod_r e: Z <~> W -> Z * A <~> W * A
Tr (-1) A
      exact (merely_isconnected n A). }
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
Z, W: BAut X
L:= fun e : Z <~> W => equiv_functor_prod_r e: Z <~> W -> Z * A <~> W * A
A -> IsEquiv L
    intros a0.
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
Z, W: BAut X
L:= fun e : Z <~> W => equiv_functor_prod_r e: Z <~> W -> Z * A <~> W * A
a0: A
IsEquiv L
    baut_reduce.
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
IsEquiv L
    pose (M := fun f:X*A -> X*A => fun x => fst (f (x,a0))).
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
IsEquiv L
    assert (MH : forall (a:A) (f:X*A -> X*A) (x:X),
               fst (f (x,a)) = fst (f (x,a0))).
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
IsEquiv L
    {
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0)) refine (conn_map_elim (Tr n) (unit_name a0) _ _).
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
Unit ->
forall (f : X * A -> X * A) 
(x : X), fst (f (x, a0)) = fst (f (x, a0))
      intros; reflexivity. }
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
IsEquiv L
    assert (MC : forall (f g :X*A -> X*A), M (g o f) == M g o M f).
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
forall f g : X * A -> X * A,
M (fun x : X * A => g (f x)) ==
(fun x : X => M g (M f x))
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
IsEquiv L
    {
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
forall f g : X * A -> X * A,
M (fun x : X * A => g (f x)) ==
(fun x : X => M g (M f x)) intros f g x; unfold M.
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
f, g: X * A -> X * A
x: X
fst (g (f (x, a0))) = fst (g (fst (f (x, a0)), a0))
      transitivity (fst (g (fst (f (x,a0)), snd (f (x,a0))))).
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
f, g: X * A -> X * A
x: X
fst (g (f (x, a0))) =
fst (g (fst (f (x, a0)), snd (f (x, a0))))
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
f, g: X * A -> X * A
x: X
fst (g (fst (f (x, a0)), snd (f (x, a0)))) =
fst (g (fst (f (x, a0)), a0))
      -
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
f, g: X * A -> X * A
x: X
fst (g (f (x, a0))) =
fst (g (fst (f (x, a0)), snd (f (x, a0)))) reflexivity.
      -
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
f, g: X * A -> X * A
x: X
fst (g (fst (f (x, a0)), snd (f (x, a0)))) =
fst (g (fst (f (x, a0)), a0)) apply MH. }
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
IsEquiv L
    pose (M' := aut_homomorphism_end M (fun x => 1) MC).
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
IsEquiv L
    assert (Mker : forall f, M' f == 1%equiv -> f == 1%equiv).
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
forall f : X * A <~> X * A,
M' f == 1%equiv -> f == 1%equiv
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
Mker: forall f : X * A <~> X * A,
M' f == 1%equiv -> f == 1%equiv
IsEquiv L
    {
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
forall f : X * A <~> X * A,
M' f == 1%equiv -> f == 1%equiv unfold M', M; cbn.
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
forall f : X * A <~> X * A,
(fun x : X => fst (f (x, a0))) == idmap -> f == idmap intros f p.
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
f: X * A <~> X * A
p: (fun x : X => fst (f (x, a0))) == idmap
f == idmap
      pose (fh := fun x a => (MH a f x) @ p x).
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
f: X * A <~> X * A
p: (fun x : X => fst (f (x, a0))) == idmap
fh:= fun (x : X) (a : A) => MH a f x @ p x: forall (x : X) (a : A), fst (f (x, a)) = x
f == idmap
      pose (g := fun x a => snd (f (x,a))).
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
f: X * A <~> X * A
p: (fun x : X => fst (f (x, a0))) == idmap
fh:= fun (x : X) (a : A) => MH a f x @ p x: forall (x : X) (a : A), fst (f (x, a)) = x
g:= fun (x : X) (a : A) => snd (f (x, a)): X -> A -> A
f == idmap
      assert (ge : forall x, IsEquiv (g x)).
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
f: X * A <~> X * A
p: (fun x : X => fst (f (x, a0))) == idmap
fh:= fun (x : X) (a : A) => MH a f x @ p x: forall (x : X) (a : A), fst (f (x, a)) = x
g:= fun (x : X) (a : A) => snd (f (x, a)): X -> A -> A
forall x : X, IsEquiv (g x)
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
f: X * A <~> X * A
p: (fun x : X => fst (f (x, a0))) == idmap
fh:= fun (x : X) (a : A) => MH a f x @ p x: forall (x : X) (a : A), fst (f (x, a)) = x
g:= fun (x : X) (a : A) => snd (f (x, a)): X -> A -> A
ge: forall x : X, IsEquiv (g x)
f == idmap
      {
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
f: X * A <~> X * A
p: (fun x : X => fst (f (x, a0))) == idmap
fh:= fun (x : X) (a : A) => MH a f x @ p x: forall (x : X) (a : A), fst (f (x, a)) = x
g:= fun (x : X) (a : A) => snd (f (x, a)): X -> A -> A
forall x : X, IsEquiv (g x) apply isequiv_from_functor_sigma.
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
f: X * A <~> X * A
p: (fun x : X => fst (f (x, a0))) == idmap
fh:= fun (x : X) (a : A) => MH a f x @ p x: forall (x : X) (a : A), fst (f (x, a)) = x
g:= fun (x : X) (a : A) => snd (f (x, a)): X -> A -> A
IsEquiv (functor_sigma idmap g)
        refine (isequiv_commsq' _ f
                  (equiv_sigma_prod0 X A) (equiv_sigma_prod0 X A) _).
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
f: X * A <~> X * A
p: (fun x : X => fst (f (x, a0))) == idmap
fh:= fun (x : X) (a : A) => MH a f x @ p x: forall (x : X) (a : A), fst (f (x, a)) = x
g:= fun (x : X) (a : A) => snd (f (x, a)): X -> A -> A
(fun x : {_ : X & A} => f (equiv_sigma_prod0 X A x)) ==
(fun x : {_ : X & A} =>
 equiv_sigma_prod0 X A (functor_sigma idmap g x))
        intros [x a]; cbn.
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
f: X * A <~> X * A
p: (fun x : X => fst (f (x, a0))) == idmap
fh:= fun (x : X) (a : A) => MH a f x @ p x: forall (x : X) (a : A), fst (f (x, a)) = x
g:= fun (x : X) (a : A) => snd (f (x, a)): X -> A -> A
x: X
a: A
f (x, a) = (x, g x a)
        apply path_prod; [ apply fh | reflexivity ]. }
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
f: X * A <~> X * A
p: (fun x : X => fst (f (x, a0))) == idmap
fh:= fun (x : X) (a : A) => MH a f x @ p x: forall (x : X) (a : A), fst (f (x, a)) = x
g:= fun (x : X) (a : A) => snd (f (x, a)): X -> A -> A
ge: forall x : X, IsEquiv (g x)
f == idmap
      intros [x a].
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
f: X * A <~> X * A
p: (fun x : X => fst (f (x, a0))) == idmap
fh:= fun (x : X) (a : A) => MH a f x @ p x: forall (x : X) (a : A), fst (f (x, a)) = x
g:= fun (x : X) (a : A) => snd (f (x, a)): X -> A -> A
ge: forall x : X, IsEquiv (g x)
x: X
a: A
f (x, a) = (x, a)
      pose (gisid := path_aut_rigid (Build_Equiv _ _ (g x) (ge x)) 1).
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
f: X * A <~> X * A
p: (fun x : X => fst (f (x, a0))) == idmap
fh:= fun (x : X) (a : A) => MH a f x @ p x: forall (x : X) (a : A), fst (f (x, a)) = x
g:= fun (x : X) (a : A) => snd (f (x, a)): X -> A -> A
ge: forall x : X, IsEquiv (g x)
x: X
a: A
gisid:= path_aut_rigid
  {| equiv_fun := g x; equiv_isequiv := ge x |}
  1: {| equiv_fun := g x; equiv_isequiv := ge x |} ==
1%equiv
f (x, a) = (x, a)
      apply path_prod.
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
f: X * A <~> X * A
p: (fun x : X => fst (f (x, a0))) == idmap
fh:= fun (x : X) (a : A) => MH a f x @ p x: forall (x : X) (a : A), fst (f (x, a)) = x
g:= fun (x : X) (a : A) => snd (f (x, a)): X -> A -> A
ge: forall x : X, IsEquiv (g x)
x: X
a: A
gisid:= path_aut_rigid
  {| equiv_fun := g x; equiv_isequiv := ge x |}
  1: {| equiv_fun := g x; equiv_isequiv := ge x |} ==
1%equiv
fst (f (x, a)) = fst (x, a)
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
f: X * A <~> X * A
p: (fun x : X => fst (f (x, a0))) == idmap
fh:= fun (x : X) (a : A) => MH a f x @ p x: forall (x : X) (a : A), fst (f (x, a)) = x
g:= fun (x : X) (a : A) => snd (f (x, a)): X -> A -> A
ge: forall x : X, IsEquiv (g x)
x: X
a: A
gisid:= path_aut_rigid
  {| equiv_fun := g x; equiv_isequiv := ge x |}
  1: {| equiv_fun := g x; equiv_isequiv := ge x |} ==
1%equiv
snd (f (x, a)) = snd (x, a)
      -
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
f: X * A <~> X * A
p: (fun x : X => fst (f (x, a0))) == idmap
fh:= fun (x : X) (a : A) => MH a f x @ p x: forall (x : X) (a : A), fst (f (x, a)) = x
g:= fun (x : X) (a : A) => snd (f (x, a)): X -> A -> A
ge: forall x : X, IsEquiv (g x)
x: X
a: A
gisid:= path_aut_rigid
  {| equiv_fun := g x; equiv_isequiv := ge x |}
  1: {| equiv_fun := g x; equiv_isequiv := ge x |} ==
1%equiv
fst (f (x, a)) = fst (x, a) apply fh.
      -
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
f: X * A <~> X * A
p: (fun x : X => fst (f (x, a0))) == idmap
fh:= fun (x : X) (a : A) => MH a f x @ p x: forall (x : X) (a : A), fst (f (x, a)) = x
g:= fun (x : X) (a : A) => snd (f (x, a)): X -> A -> A
ge: forall x : X, IsEquiv (g x)
x: X
a: A
gisid:= path_aut_rigid
  {| equiv_fun := g x; equiv_isequiv := ge x |}
  1: {| equiv_fun := g x; equiv_isequiv := ge x |} ==
1%equiv
snd (f (x, a)) = snd (x, a) apply gisid. }
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
Mker: forall f : X * A <~> X * A,
M' f == 1%equiv -> f == 1%equiv
IsEquiv L
    assert (Minj : forall f g, M' f == M' g -> f == g).
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
Mker: forall f : X * A <~> X * A,
M' f == 1%equiv -> f == 1%equiv
forall f g : X * A <~> X * A, M' f == M' g -> f == g
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
Mker: forall f : X * A <~> X * A,
M' f == 1%equiv -> f == 1%equiv
Minj: forall f g : X * A <~> X * A,
M' f == M' g -> f == g
IsEquiv L
    {
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
Mker: forall f : X * A <~> X * A,
M' f == 1%equiv -> f == 1%equiv
forall f g : X * A <~> X * A, M' f == M' g -> f == g intros f g p z.
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
Mker: forall f : X * A <~> X * A,
M' f == 1%equiv -> f == 1%equiv
f, g: X * A <~> X * A
p: M' f == M' g
z: X * A
f z = g z
      apply moveL_equiv_M.
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
Mker: forall f : X * A <~> X * A,
M' f == 1%equiv -> f == 1%equiv
f, g: X * A <~> X * A
p: M' f == M' g
z: X * A
g^-1 (f z) = z
      revert z.
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
Mker: forall f : X * A <~> X * A,
M' f == 1%equiv -> f == 1%equiv
f, g: X * A <~> X * A
p: M' f == M' g
forall z : X * A, g^-1 (f z) = z
      refine (Mker (g^-1 oE f) _).
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
Mker: forall f : X * A <~> X * A,
M' f == 1%equiv -> f == 1%equiv
f, g: X * A <~> X * A
p: M' f == M' g
M' (g^-1 oE f) == 1%equiv
      intros x.
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
Mker: forall f : X * A <~> X * A,
M' f == 1%equiv -> f == 1%equiv
f, g: X * A <~> X * A
p: M' f == M' g
x: X
M' (g^-1 oE f) x = 1%equiv x
      refine (MC f g^-1 x @ _).
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
Mker: forall f : X * A <~> X * A,
M' f == 1%equiv -> f == 1%equiv
f, g: X * A <~> X * A
p: M' f == M' g
x: X
M g^-1 (M f x) = 1%equiv x
      change ((M' g)^-1 (M f x) = x).
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
Mker: forall f : X * A <~> X * A,
M' f == 1%equiv -> f == 1%equiv
f, g: X * A <~> X * A
p: M' f == M' g
x: X
(M' g)^-1 (M f x) = x
      apply moveR_equiv_V, p. }
H: Univalence
X, A: Type
n: trunc_index
IsTrunc0: IsTrunc n.+1 X
H0: IsRigid A
H1: IsConnected (Tr n.+1) A
L:= fun e : point (BAut X) <~> point (BAut X) =>
equiv_functor_prod_r e: point (BAut X) <~> point (BAut X) ->
point (BAut X) * A <~> point (BAut X) * A
a0: A
M:= fun (f : X * A -> X * A) (x : X) => fst (f (x, a0)): (X * A -> X * A) -> X -> X
MH: forall (a : A) (f : X * A -> X * A) 
(x : X), fst (f (x, a)) = fst (f (x, a0))
MC: forall f g : X * A -> X * A,
M (g o f) == M g o M f
M':= aut_homomorphism_end M (fun x : X => 1) MC: X * A <~> X * A -> X <~> X
Mker: forall f : X * A <~> X * A,
M' f == 1%equiv -> f == 1%equiv
Minj: forall f g : X * A <~> X * A,
M' f == M' g -> f == g
IsEquiv L
    refine (isequiv_adjointify L M' _ _);
      intros e;
      apply path_equiv, path_arrow;
      try apply Minj;
      intros x; reflexivity. }
Defined.