(* -*- mode: coq; mode: visual-line -*-  *)
Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Constant.
Require Import HoTT.Truncations.
Require Import ObjectClassifier Homotopy.ExactSequence Pointed.

Local Open Scope type_scope.
Local Open Scope path_scope.

(** * BAut(X) *)

(** ** Basics *)

(** [BAut X] is the type of types that are merely equal to [X]. It is connected, by [is0connected_component] and any two points are merely equal by [merely_path_component]. *)
Definition BAut (X : Type@{u}) := { Z : Type@{u} & merely (Z = X) }.

Coercion BAut_pr1 X : BAut X -> Type := pr1.

Global Instance ispointed_baut {X : Type} : IsPointed (BAut X) := (X; tr 1).

(** We also define a pointed version [pBAut X], since the coercion [BAut_pr1] doesn't work if [BAut X] is a [pType]. *)
Definition pBAut (X : Type) : pType
  := [BAut X, _].

Definition path_baut `{Univalence} {X} (Z Z' : BAut X)
: (Z <~> Z') <~> (Z = Z' :> BAut X)
  := equiv_path_sigma_hprop _ _ oE equiv_path_universe _ _.

Definition ap_pr1_path_baut `{Univalence} {X}
           {Z Z' : BAut X} (f : Z <~> Z')
: ap (BAut_pr1 X) (path_baut Z Z' f) = path_universe f.
H: Univalence
X: Type
Z, Z': BAut X
f: Z <~> Z'
ap (BAut_pr1 X) (path_baut Z Z' f) = path_universe f
Proof.
H: Univalence
X: Type
Z, Z': BAut X
f: Z <~> Z'
ap (BAut_pr1 X) (path_baut Z Z' f) = path_universe f
  unfold path_baut, BAut_pr1; simpl.
H: Univalence
X: Type
Z, Z': BAut X
f: Z <~> Z'
ap pr1
  (path_sigma_hprop Z Z' (path_universe_uncurried f)) =
path_universe f
  apply ap_pr1_path_sigma_hprop.
Defined.

Definition transport_path_baut `{Univalence} {X}
           {Z Z' : BAut X} (f : Z <~> Z') (z : Z)
: transport (fun (W:BAut X) => W) (path_baut Z Z' f) z = f z.
H: Univalence
X: Type
Z, Z': BAut X
f: Z <~> Z'
z: Z
transport (fun W : BAut X => W) (path_baut Z Z' f) z =
f z
Proof.
H: Univalence
X: Type
Z, Z': BAut X
f: Z <~> Z'
z: Z
transport (fun W : BAut X => W) (path_baut Z Z' f) z =
f z
  refine (transport_compose idmap (BAut_pr1 X) _ _ @ _).
H: Univalence
X: Type
Z, Z': BAut X
f: Z <~> Z'
z: Z
transport idmap (ap (BAut_pr1 X) (path_baut Z Z' f)) z =
f z
  refine (_ @ transport_path_universe f z).
H: Univalence
X: Type
Z, Z': BAut X
f: Z <~> Z'
z: Z
transport idmap (ap (BAut_pr1 X) (path_baut Z Z' f)) z =
transport idmap (path_universe f) z
  apply ap10, ap, ap_pr1_path_baut.
Defined.

(** The following tactic, which applies when trying to prove an hprop, replaces all assumed elements of [BAut X] by [X] itself. With [Univalence], this would work for any 0-connected type, but using [merely_path_component] we can avoid univalence. *)
Ltac baut_reduce :=
  progress repeat
    match goal with
      | [ Z : BAut ?X |- _ ]
        => let Zispoint := fresh "Zispoint" in
           assert (Zispoint := merely_path_component (point (BAut X)) Z);
           revert Zispoint;
           refine (@Trunc_ind _ _ _ _ _);
           intro Zispoint;
           destruct Zispoint
    end.

(** ** Truncation *)

(** If [X] is an [n.+1]-type, then [BAut X] is an [n.+2]-type. *)
Global Instance trunc_baut `{Univalence} {n X} `{IsTrunc n.+1 X}
: IsTrunc n.+2 (BAut X).
H: Univalence
n: trunc_index
X: Type
IsTrunc0: IsTrunc n.+1 X
IsTrunc n.+2 (BAut X)
Proof.
H: Univalence
n: trunc_index
X: Type
IsTrunc0: IsTrunc n.+1 X
IsTrunc n.+2 (BAut X)
  apply istrunc_S.
H: Univalence
n: trunc_index
X: Type
IsTrunc0: IsTrunc n.+1 X
forall x y : BAut X, IsTrunc n.+1 (x = y)
  intros Z W.
H: Univalence
n: trunc_index
X: Type
IsTrunc0: IsTrunc n.+1 X
Z, W: BAut X
IsTrunc n.+1 (Z = W)
  baut_reduce.
H: Univalence
n: trunc_index
X: Type
IsTrunc0: IsTrunc n.+1 X
IsTrunc n.+1 (pt = pt)
  exact (@istrunc_equiv_istrunc _ _ (path_baut _ _) n.+1 _).
Defined.

(** If [X] is truncated, then so is every element of [BAut X]. *)
Global Instance trunc_el_baut {n X} `{Funext} `{IsTrunc n X} (Z : BAut X)
  : IsTrunc n Z
  := ltac:(by baut_reduce).

(** ** Operations on [BAut] *)

(** Multiplying by a fixed type *)

Definition baut_prod_r (X A : Type)
  : BAut X -> BAut (X * A)
  := fun Z:BAut X =>
       (Z * A ; Trunc_functor (-1) (ap (fun W => W * A)) (pr2 Z))
       : BAut (X * A).

Definition ap_baut_prod_r `{Univalence} (X A : Type)
           {Z W : BAut X} (e : Z <~> W)
  : ap (baut_prod_r X A) (path_baut Z W e)
    = path_baut (baut_prod_r X A Z) (baut_prod_r X A W) (equiv_functor_prod_r e).
H: Univalence
X, A: Type
Z, W: BAut X
e: Z <~> W
ap (baut_prod_r X A) (path_baut Z W e) =
path_baut (baut_prod_r X A Z) (baut_prod_r X A W)
  (equiv_functor_prod_r e)
Proof.
H: Univalence
X, A: Type
Z, W: BAut X
e: Z <~> W
ap (baut_prod_r X A) (path_baut Z W e) =
path_baut (baut_prod_r X A Z) (baut_prod_r X A W)
  (equiv_functor_prod_r e)
  cbn.
H: Univalence
X, A: Type
Z, W: BAut X
e: Z <~> W
ap (baut_prod_r X A)
  (path_sigma_hprop Z W (path_universe_uncurried e)) =
path_sigma_hprop (baut_prod_r X A Z)
  (baut_prod_r X A W)
  (path_universe_uncurried (equiv_functor_prod_r e))
  apply moveL_equiv_M; cbn; unfold pr1_path.
H: Univalence
X, A: Type
Z, W: BAut X
e: Z <~> W
ap pr1
  (ap (baut_prod_r X A)
     (path_sigma_hprop Z W (path_universe_uncurried e))) =
path_universe_uncurried (equiv_functor_prod_r e)
  rewrite <- (ap_compose (baut_prod_r X A) pr1 (path_sigma_hprop Z W _)).
H: Univalence
X, A: Type
Z, W: BAut X
e: Z <~> W
ap (fun x : BAut X => (baut_prod_r X A x).1)
  (path_sigma_hprop Z W (path_universe_uncurried e)) =
path_universe_uncurried (equiv_functor_prod_r e)
  rewrite <- ((ap_compose pr1 (fun Z => Z * A) (path_sigma_hprop Z W _))^).
H: Univalence
X, A: Type
Z, W: BAut X
e: Z <~> W
ap (fun Z : Type => Z * A)
  (ap pr1
     (path_sigma_hprop Z W (path_universe_uncurried e))) =
path_universe_uncurried (equiv_functor_prod_r e)
  rewrite ap_pr1_path_sigma_hprop.
H: Univalence
X, A: Type
Z, W: BAut X
e: Z <~> W
ap (fun Z : Type => Z * A) (path_universe_uncurried e) =
path_universe_uncurried (equiv_functor_prod_r e)
  apply moveL_equiv_M; cbn.
H: Univalence
X, A: Type
Z, W: BAut X
e: Z <~> W
equiv_path (Z * A) (W * A)
  (ap (fun Z : Type => Z * A)
     (path_universe_uncurried e)) =
equiv_functor_prod_r e
  apply ap_prod_r_path_universe.
Qed.

(** ** Centers *)

(** The following lemma says that to define a section of a family [P] of hsets over [BAut X], it is equivalent to define an element of [P X] which is fixed by all automorphisms of [X]. *)
Lemma baut_ind_hset `{Univalence} X
      (** It ought to be possible to allow more generally [P : BAut X -> Type], but the proof would get more complicated, and this version suffices for present applications. *)
      (P : Type -> Type) `{forall (Z : BAut X), IsHSet (P Z)}
: { e : P (point (BAut X)) &
    forall g : X <~> X, transport P (path_universe g) e = e }
  <~> (forall (Z:BAut X), P Z).
H: Univalence
X: Type
P: Type -> Type
H0: forall Z : BAut X, IsHSet (P Z)
{e : P pt &
forall g : X <~> X,
transport P (path_universe g) e = e} <~>
(forall Z : BAut X, P Z)
Proof.
H: Univalence
X: Type
P: Type -> Type
H0: forall Z : BAut X, IsHSet (P Z)
{e : P pt &
forall g : X <~> X,
transport P (path_universe g) e = e} <~>
(forall Z : BAut X, P Z)
  refine (equiv_sig_ind _ oE _).
H: Univalence
X: Type
P: Type -> Type
H0: forall Z : BAut X, IsHSet (P Z)
{e : P pt &
forall g : X <~> X,
transport P (path_universe g) e = e} <~>
(forall (x : Type) (y : merely (x = X)), P (x; y))
  (** We use the fact that maps out of a propositional truncation into an hset are equivalent to weakly constant functions. *)
  refine ((equiv_functor_forall'
             (P := fun Z => { f : (Z=X) -> P Z & WeaklyConstant f })
             1
             (fun Z => equiv_merely_rec_hset _ _)) oE _); simpl.
H: Univalence
X: Type
P: Type -> Type
H0: forall Z : BAut X, IsHSet (P Z)
Z: Type
Z = X -> IsHSet (P Z)
H: Univalence
X: Type
P: Type -> Type
H0: forall Z : BAut X, IsHSet (P Z)
{e : P X &
forall g : X <~> X,
transport P (path_universe g) e = e} <~>
(forall a : Type,
 {f : a = X -> P a & WeaklyConstant f})
  {
H: Univalence
X: Type
P: Type -> Type
H0: forall Z : BAut X, IsHSet (P Z)
Z: Type
Z = X -> IsHSet (P Z) intros p.
H: Univalence
X: Type
P: Type -> Type
H0: forall Z : BAut X, IsHSet (P Z)
Z: Type
p: Z = X
IsHSet (P Z) change (IsHSet (P (BAut_pr1 X (Z ; tr p)))).
H: Univalence
X: Type
P: Type -> Type
H0: forall Z : BAut X, IsHSet (P Z)
Z: Type
p: Z = X
IsHSet (P (Z; tr p)) exact _. }
H: Univalence
X: Type
P: Type -> Type
H0: forall Z : BAut X, IsHSet (P Z)
{e : P X &
forall g : X <~> X,
transport P (path_universe g) e = e} <~>
(forall a : Type,
 {f : a = X -> P a & WeaklyConstant f})
  unfold WeaklyConstant.
H: Univalence
X: Type
P: Type -> Type
H0: forall Z : BAut X, IsHSet (P Z)
{e : P X &
forall g : X <~> X,
transport P (path_universe g) e = e} <~>
(forall a : Type,
 {f : a = X -> P a & forall x y : a = X, f x = f y})
  (** Now we peel away a bunch of contractible types. *)
  refine (equiv_sig_coind _ _ oE _).
H: Univalence
X: Type
P: Type -> Type
H0: forall Z : BAut X, IsHSet (P Z)
{e : P X &
forall g : X <~> X,
transport P (path_universe g) e = e} <~>
{f : forall x : Type, x = X -> P x &
forall (x : Type) (x0 y : x = X), f x x0 = f x y}
  srapply equiv_functor_sigma'.
H: Univalence
X: Type
P: Type -> Type
H0: forall Z : BAut X, IsHSet (P Z)
P X <~> (forall x : Type, x = X -> P x)
H: Univalence
X: Type
P: Type -> Type
H0: forall Z : BAut X, IsHSet (P Z)
forall a : P X,
(fun e : P X =>
 forall g : X <~> X,
 transport P (path_universe g) e = e) a <~>
(fun f : forall x : Type, x = X -> P x =>
 forall (x : Type) (x0 y : x = X), f x x0 = f x y)
  (?f a)
  1:apply (equiv_paths_ind_r X (fun x _ => P x)).
H: Univalence
X: Type
P: Type -> Type
H0: forall Z : BAut X, IsHSet (P Z)
forall a : P X,
(fun e : P X =>
 forall g : X <~> X,
 transport P (path_universe g) e = e) a <~>
(fun f : forall x : Type, x = X -> P x =>
 forall (x : Type) (x0 y : x = X), f x x0 = f x y)
  (equiv_paths_ind_r X
     (fun (x : Type) (_ : x = X) => P x) a)
  intros p; cbn.
H: Univalence
X: Type
P: Type -> Type
H0: forall Z : BAut X, IsHSet (P Z)
p: P X
(forall g : X <~> X,
 transport P (path_universe g) p = p) <~>
(forall (x : Type) (x0 y : x = X),
 paths_ind_r X (fun (x1 : Type) (_ : x1 = X) => P x1)
   p x x0 =
 paths_ind_r X (fun (x1 : Type) (_ : x1 = X) => P x1)
   p x y)
  refine (equiv_paths_ind_r X _ oE _).
H: Univalence
X: Type
P: Type -> Type
H0: forall Z : BAut X, IsHSet (P Z)
p: P X
(forall g : X <~> X,
 transport P (path_universe g) p = p) <~>
(forall y : X = X,
 paths_ind_r X (fun (x : Type) (_ : x = X) => P x) p X
   1 =
 paths_ind_r X (fun (x : Type) (_ : x = X) => P x) p X
   y)
  srapply equiv_functor_forall'.
H: Univalence
X: Type
P: Type -> Type
H0: forall Z : BAut X, IsHSet (P Z)
p: P X
X = X <~> (X <~> X)
H: Univalence
X: Type
P: Type -> Type
H0: forall Z : BAut X, IsHSet (P Z)
p: P X
forall b : X = X,
(fun a : X <~> X =>
 transport P (path_universe a) p = p) (?f b) <~>
(fun b0 : X = X =>
 paths_ind_r X (fun (x : Type) (_ : x = X) => P x) p X
   1 =
 paths_ind_r X (fun (x : Type) (_ : x = X) => P x) p X
   b0) b
  1:apply equiv_equiv_path.
H: Univalence
X: Type
P: Type -> Type
H0: forall Z : BAut X, IsHSet (P Z)
p: P X
forall b : X = X,
(fun a : X <~> X =>
 transport P (path_universe a) p = p)
  (equiv_equiv_path X X b) <~>
(fun b0 : X = X =>
 paths_ind_r X (fun (x : Type) (_ : x = X) => P x) p X
   1 =
 paths_ind_r X (fun (x : Type) (_ : x = X) => P x) p X
   b0) b
  intros e; cbn.
H: Univalence
X: Type
P: Type -> Type
H0: forall Z : BAut X, IsHSet (P Z)
p: P X
e: X = X
transport P (path_universe (transport idmap e)) p = p <~>
p =
paths_ind_r X (fun (x : Type) (_ : x = X) => P x) p X
  e
  refine (_ oE equiv_moveL_transport_V _ _ _ _).
H: Univalence
X: Type
P: Type -> Type
H0: forall Z : BAut X, IsHSet (P Z)
p: P X
e: X = X
p = transport P (path_universe (transport idmap e))^ p <~>
p =
paths_ind_r X (fun (x : Type) (_ : x = X) => P x) p X
  e 
  apply equiv_concat_r.
H: Univalence
X: Type
P: Type -> Type
H0: forall Z : BAut X, IsHSet (P Z)
p: P X
e: X = X
transport P (path_universe (transport idmap e))^ p =
paths_ind_r X (fun (x : Type) (_ : x = X) => P x) p X
  e
  rewrite path_universe_transport_idmap, paths_ind_r_transport.
H: Univalence
X: Type
P: Type -> Type
H0: forall Z : BAut X, IsHSet (P Z)
p: P X
e: X = X
transport P e^ p = transport P e^ p
  reflexivity.
Defined.

(** This implies that if [X] is a set, then the center of [BAut X] is the set of automorphisms of [X] that commute with every other automorphism (i.e. the center, in the usual sense, of the group of automorphisms of [X]). *)

Definition center_baut `{Univalence} X `{IsHSet X}
: { f : X <~> X & forall g:X<~>X, g o f == f o g }
  <~> (forall Z:BAut X, Z = Z).
H: Univalence
X: Type
IsHSet0: IsHSet X
{f : X <~> X & forall g : X <~> X, g o f == f o g} <~>
(forall Z : BAut X, Z = Z)
Proof.
H: Univalence
X: Type
IsHSet0: IsHSet X
{f : X <~> X & forall g : X <~> X, g o f == f o g} <~>
(forall Z : BAut X, Z = Z)
  refine (equiv_functor_forall_id
            (fun Z => equiv_path_sigma_hprop Z Z) oE _).
H: Univalence
X: Type
IsHSet0: IsHSet X
{f : X <~> X &
forall g : X <~> X,
(fun x : X => g (f x)) == (fun x : X => f (g x))} <~>
(forall a : {Z : Type & merely (Z = X)}, a.1 = a.1)
  refine (baut_ind_hset X (fun Z => Z = Z) oE _).
H: Univalence
X: Type
IsHSet0: IsHSet X
{f : X <~> X &
forall g : X <~> X,
(fun x : X => g (f x)) == (fun x : X => f (g x))} <~>
{e : pt = pt &
forall g : X <~> X,
transport (fun Z : Type => Z = Z) (path_universe g) e =
e}
  simpl.
H: Univalence
X: Type
IsHSet0: IsHSet X
{f : X <~> X &
forall g : X <~> X,
(fun x : X => g (f x)) == (fun x : X => f (g x))} <~>
{e : X = X &
forall g : X <~> X,
transport (fun Z : Type => Z = Z) (path_universe g) e =
e}
  refine (equiv_functor_sigma' (equiv_path_universe X X) _); intros f.
H: Univalence
X: Type
IsHSet0: IsHSet X
f: X <~> X
(forall g : X <~> X,
 (fun x : X => g (f x)) == (fun x : X => f (g x))) <~>
(forall g : X <~> X,
 transport (fun Z : Type => Z = Z) (path_universe g)
   (equiv_path_universe X X f) =
 equiv_path_universe X X f)
  apply equiv_functor_forall_id; intros g; simpl.
H: Univalence
X: Type
IsHSet0: IsHSet X
f, g: X <~> X
(fun x : X => g (f x)) == (fun x : X => f (g x)) <~>
transport (fun Z : Type => Z = Z) (path_universe g)
  (path_universe_uncurried f) =
path_universe_uncurried f
  refine (_ oE equiv_path_arrow _ _).
H: Univalence
X: Type
IsHSet0: IsHSet X
f, g: X <~> X
(fun x : X => g (f x)) = (fun x : X => f (g x)) <~>
transport (fun Z : Type => Z = Z) (path_universe g)
  (path_universe_uncurried f) =
path_universe_uncurried f
  refine (_ oE equiv_path_equiv (g oE f) (f oE g)).
H: Univalence
X: Type
IsHSet0: IsHSet X
f, g: X <~> X
g oE f = f oE g <~>
transport (fun Z : Type => Z = Z) (path_universe g)
  (path_universe_uncurried f) =
path_universe_uncurried f
  revert g.
H: Univalence
X: Type
IsHSet0: IsHSet X
f: X <~> X
forall g : X <~> X,
g oE f = f oE g <~>
transport (fun Z : Type => Z = Z) (path_universe g)
  (path_universe_uncurried f) =
path_universe_uncurried f equiv_intro (equiv_path X X) g.
H: Univalence
X: Type
IsHSet0: IsHSet X
f: X <~> X
g: X = X
equiv_path X X g oE f = f oE equiv_path X X g <~>
transport (fun Z : Type => Z = Z)
  (path_universe (equiv_path X X g))
  (path_universe_uncurried f) =
path_universe_uncurried f
  revert f.
H: Univalence
X: Type
IsHSet0: IsHSet X
g: X = X
forall f : X <~> X,
equiv_path X X g oE f = f oE equiv_path X X g <~>
transport (fun Z : Type => Z = Z)
  (path_universe (equiv_path X X g))
  (path_universe_uncurried f) =
path_universe_uncurried f equiv_intro (equiv_path X X) f.
H: Univalence
X: Type
IsHSet0: IsHSet X
g, f: X = X
equiv_path X X g oE equiv_path X X f =
equiv_path X X f oE equiv_path X X g <~>
transport (fun Z : Type => Z = Z)
  (path_universe (equiv_path X X g))
  (path_universe_uncurried (equiv_path X X f)) =
path_universe_uncurried (equiv_path X X f)
  refine (_ oE equiv_concat_l (equiv_path_pp _ _) _).
H: Univalence
X: Type
IsHSet0: IsHSet X
g, f: X = X
equiv_path X X (f @ g) =
equiv_path X X f oE equiv_path X X g <~>
transport (fun Z : Type => Z = Z)
  (path_universe (equiv_path X X g))
  (path_universe_uncurried (equiv_path X X f)) =
path_universe_uncurried (equiv_path X X f)
  refine (_ oE equiv_concat_r (equiv_path_pp _ _)^ _).
H: Univalence
X: Type
IsHSet0: IsHSet X
g, f: X = X
equiv_path X X (f @ g) = equiv_path X X (g @ f) <~>
transport (fun Z : Type => Z = Z)
  (path_universe (equiv_path X X g))
  (path_universe_uncurried (equiv_path X X f)) =
path_universe_uncurried (equiv_path X X f)
  refine (_ oE (equiv_ap (equiv_path X X) _ _)^-1).
H: Univalence
X: Type
IsHSet0: IsHSet X
g, f: X = X
f @ g = g @ f <~>
transport (fun Z : Type => Z = Z)
  (path_universe (equiv_path X X g))
  (path_universe_uncurried (equiv_path X X f)) =
path_universe_uncurried (equiv_path X X f)
  refine (equiv_concat_l (transport_paths_lr _ _) _ oE _).
H: Univalence
X: Type
IsHSet0: IsHSet X
g, f: X = X
f @ g = g @ f <~>
((path_universe (equiv_path X X g))^ @
 path_universe_uncurried (equiv_path X X f)) @
path_universe (equiv_path X X g) =
path_universe_uncurried (equiv_path X X f)
  refine (equiv_concat_l (concat_pp_p _ _ _) _ oE _).
H: Univalence
X: Type
IsHSet0: IsHSet X
g, f: X = X
f @ g = g @ f <~>
(path_universe (equiv_path X X g))^ @
(path_universe_uncurried (equiv_path X X f) @
 path_universe (equiv_path X X g)) =
path_universe_uncurried (equiv_path X X f)
  refine (equiv_moveR_Vp _ _ _ oE _).
H: Univalence
X: Type
IsHSet0: IsHSet X
g, f: X = X
f @ g = g @ f <~>
path_universe_uncurried (equiv_path X X f) @
path_universe (equiv_path X X g) =
path_universe (equiv_path X X g) @
path_universe_uncurried (equiv_path X X f)
  refine (equiv_concat_l _ _ oE equiv_concat_r _ _).
H: Univalence
X: Type
IsHSet0: IsHSet X
g, f: X = X
path_universe_uncurried (equiv_path X X f) @
path_universe (equiv_path X X g) = f @ g
H: Univalence
X: Type
IsHSet0: IsHSet X
g, f: X = X
g @ f =
path_universe (equiv_path X X g) @
path_universe_uncurried (equiv_path X X f)
  -
H: Univalence
X: Type
IsHSet0: IsHSet X
g, f: X = X
path_universe_uncurried (equiv_path X X f) @
path_universe (equiv_path X X g) = f @ g apply concat2; apply eissect.
  -
H: Univalence
X: Type
IsHSet0: IsHSet X
g, f: X = X
g @ f =
path_universe (equiv_path X X g) @
path_universe_uncurried (equiv_path X X f) symmetry; apply concat2; apply eissect.
Defined.

(** We show that this equivalence takes the identity equivalence to the identity in the center.  We have to be careful in this proof never to [simpl] or [unfold] too many things, or Coq will produce gigantic terms that take it forever to compute with. *)
Definition id_center_baut `{Univalence} X `{IsHSet X}
: center_baut X (exist
                   (fun (f:X<~>X) => forall (g:X<~>X), g o f == f o g)
                   (equiv_idmap X)
                   (fun (g:X<~>X) (x:X) => idpath (g x)))
  = fun Z => idpath Z.
H: Univalence
X: Type
IsHSet0: IsHSet X
center_baut X
  (1%equiv; fun (g : X <~> X) (x : X) => 1) =
(fun Z : BAut X => 1)
Proof.
H: Univalence
X: Type
IsHSet0: IsHSet X
center_baut X
  (1%equiv; fun (g : X <~> X) (x : X) => 1) =
(fun Z : BAut X => 1)
  apply path_forall; intros Z.
H: Univalence
X: Type
IsHSet0: IsHSet X
Z: BAut X
center_baut X
  (1%equiv; fun (g : X <~> X) (x : X) => 1) Z = 1
  assert (IsHSet (Z.1 = Z.1)) by exact _.
H: Univalence
X: Type
IsHSet0: IsHSet X
Z: BAut X
X0: IsHSet (Z.1 = Z.1)
center_baut X
  (1%equiv; fun (g : X <~> X) (x : X) => 1) Z = 1
  baut_reduce.
H: Univalence
X: Type
IsHSet0: IsHSet X
X0: IsHSet (pt.1 = pt.1)
center_baut X
  (1%equiv; fun (g : X <~> X) (x : X) => 1) pt = 1
  exact (ap (path_sigma_hprop _ _) path_universe_1
            @ path_sigma_hprop_1 _).
Defined.

(** Similarly, if [X] is a 1-type, we can characterize the 2-center of [BAut X]. *)

(** Coq is too eager about unfolding some things appearing in this proof. *)
Section Center2BAut.
  Local Arguments equiv_path_equiv : simpl never.
  Local Arguments equiv_path2_universe : simpl never.

  Definition center2_baut `{Univalence} X `{IsTrunc 1 X}
  : { f : forall x:X, x=x & forall (g:X<~>X) (x:X), ap g (f x) = f (g x) }
      <~> (forall Z:BAut X, (idpath Z) = (idpath Z)).
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
{f : forall x : X, x = x &
forall (g : X <~> X) (x : X), ap g (f x) = f (g x)} <~>
(forall Z : BAut X, 1 = 1)
  Proof.
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
{f : forall x : X, x = x &
forall (g : X <~> X) (x : X), ap g (f x) = f (g x)} <~>
(forall Z : BAut X, 1 = 1)
    refine ((equiv_functor_forall_id
               (fun Z => (equiv_concat_lr _ _)
                           oE (equiv_ap (equiv_path_sigma_hprop Z Z) 1%path 1%path))) oE _).
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
Z: {Z : Type & merely (Z = X)}
1 = equiv_path_sigma_hprop Z Z 1
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
Z: {Z : Type & merely (Z = X)}
equiv_path_sigma_hprop Z Z 1 = 1
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
{f : forall x : X, x = x &
forall (g : X <~> X) (x : X), ap g (f x) = f (g x)} <~>
(forall a : {Z : Type & merely (Z = X)}, 1 = 1)
    {
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
Z: {Z : Type & merely (Z = X)}
1 = equiv_path_sigma_hprop Z Z 1 symmetry; apply path_sigma_hprop_1. }
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
Z: {Z : Type & merely (Z = X)}
equiv_path_sigma_hprop Z Z 1 = 1
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
{f : forall x : X, x = x &
forall (g : X <~> X) (x : X), ap g (f x) = f (g x)} <~>
(forall a : {Z : Type & merely (Z = X)}, 1 = 1)
    {
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
Z: {Z : Type & merely (Z = X)}
equiv_path_sigma_hprop Z Z 1 = 1 apply path_sigma_hprop_1. }
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
{f : forall x : X, x = x &
forall (g : X <~> X) (x : X), ap g (f x) = f (g x)} <~>
(forall a : {Z : Type & merely (Z = X)}, 1 = 1)
    assert (forall Z:BAut X, IsHSet (idpath Z.1 = idpath Z.1)) by exact _.
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: forall Z : BAut X, IsHSet (1 = 1)
{f : forall x : X, x = x &
forall (g : X <~> X) (x : X), ap g (f x) = f (g x)} <~>
(forall a : {Z : Type & merely (Z = X)}, 1 = 1)
    refine (baut_ind_hset X (fun Z => idpath Z = idpath Z) oE _).
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: forall Z : BAut X, IsHSet (1 = 1)
{f : forall x : X, x = x &
forall (g : X <~> X) (x : X), ap g (f x) = f (g x)} <~>
{e : 1 = 1 &
forall g : X <~> X,
transport (fun Z : Type => 1 = 1) (path_universe g) e =
e}
    simple refine (equiv_functor_sigma' _ _).
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: forall Z : BAut X, IsHSet (1 = 1)
(forall x : X, x = x) <~> 1 = 1
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: forall Z : BAut X, IsHSet (1 = 1)
forall a : forall x : X, x = x,
(fun f : forall x : X, x = x =>
 forall (g : X <~> X) (x : X), ap g (f x) = f (g x)) a <~>
(fun e : 1 = 1 =>
 forall g : X <~> X,
 transport (fun Z : Type => 1 = 1) (path_universe g) e =
 e) (?f a)
    {
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: forall Z : BAut X, IsHSet (1 = 1)
(forall x : X, x = x) <~> 1 = 1 refine (_ oE equiv_path2_universe 1 1).
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: forall Z : BAut X, IsHSet (1 = 1)
path_universe 1%equiv = path_universe 1%equiv <~>
1 = 1
      apply equiv_concat_lr.
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: forall Z : BAut X, IsHSet (1 = 1)
1 = path_universe 1%equiv
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: forall Z : BAut X, IsHSet (1 = 1)
path_universe 1%equiv = 1
      -
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: forall Z : BAut X, IsHSet (1 = 1)
1 = path_universe 1%equiv symmetry; apply path_universe_1.
      -
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: forall Z : BAut X, IsHSet (1 = 1)
path_universe 1%equiv = 1 apply path_universe_1. }
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: forall Z : BAut X, IsHSet (1 = 1)
forall a : forall x : X, x = x,
(fun f : forall x : X, x = x =>
 forall (g : X <~> X) (x : X), ap g (f x) = f (g x)) a <~>
(fun e : 1 = 1 =>
 forall g : X <~> X,
 transport (fun Z : Type => 1 = 1) (path_universe g) e =
 e)
  ((equiv_concat_lr path_universe_1^ path_universe_1
    oE equiv_path2_universe 1 1) a)
    intros f.
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: forall Z : BAut X, IsHSet (1 = 1)
f: forall x : X, x = x
(fun f : forall x : X, x = x =>
 forall (g : X <~> X) (x : X), ap g (f x) = f (g x)) f <~>
(fun e : 1 = 1 =>
 forall g : X <~> X,
 transport (fun Z : Type => 1 = 1) (path_universe g) e =
 e)
  ((equiv_concat_lr path_universe_1^ path_universe_1
    oE equiv_path2_universe 1 1) f)
    apply equiv_functor_forall_id; intros g.
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: forall Z : BAut X, IsHSet (1 = 1)
f: forall x : X, x = x
g: X <~> X
(forall x : X, ap g (f x) = f (g x)) <~>
transport (fun Z : Type => 1 = 1) (path_universe g)
  ((equiv_concat_lr path_universe_1^ path_universe_1
    oE equiv_path2_universe 1 1) f) =
(equiv_concat_lr path_universe_1^ path_universe_1
 oE equiv_path2_universe 1 1) f
    refine (_ oE equiv_path3_universe _ _).
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: forall Z : BAut X, IsHSet (1 = 1)
f: forall x : X, x = x
g: X <~> X
path2_universe (fun x : X => ap g (f x)) =
path2_universe (fun x : X => f (g x)) <~>
transport (fun Z : Type => 1 = 1) (path_universe g)
  ((equiv_concat_lr path_universe_1^ path_universe_1
    oE equiv_path2_universe 1 1) f) =
(equiv_concat_lr path_universe_1^ path_universe_1
 oE equiv_path2_universe 1 1) f
    refine (dpath_paths2 (path_universe g) _ _ oE _).
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: forall Z : BAut X, IsHSet (1 = 1)
f: forall x : X, x = x
g: X <~> X
path2_universe (fun x : X => ap g (f x)) =
path2_universe (fun x : X => f (g x)) <~>
((concat_1p (path_universe g))^ @
 whiskerR
   ((equiv_concat_lr path_universe_1^ path_universe_1
     oE equiv_path2_universe 1 1) f) (path_universe g)) @
concat_1p (path_universe g) =
((concat_p1 (path_universe g))^ @
 whiskerL (path_universe g)
   ((equiv_concat_lr path_universe_1^ path_universe_1
     oE equiv_path2_universe 1 1) f)) @
concat_p1 (path_universe g)
    cbn.
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: forall Z : BAut X, IsHSet (1 = 1)
f: forall x : X, x = x
g: X <~> X
path2_universe (fun x : X => ap g (f x)) =
path2_universe (fun x : X => f (g x)) <~>
((concat_1p (path_universe g))^ @
 whiskerR
   ((path_universe_1^ @ equiv_path2_universe 1 1 f) @
    path_universe_1) (path_universe g)) @
concat_1p (path_universe g) =
((concat_p1 (path_universe g))^ @
 whiskerL (path_universe g)
   ((path_universe_1^ @ equiv_path2_universe 1 1 f) @
    path_universe_1)) @ concat_p1 (path_universe g)
    change (equiv_idmap X == equiv_idmap X) in f.
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: forall Z : BAut X, IsHSet (1 = 1)
f: 1%equiv == 1%equiv
g: X <~> X
path2_universe (fun x : X => ap g (f x)) =
path2_universe (fun x : X => f (g x)) <~>
((concat_1p (path_universe g))^ @
 whiskerR
   ((path_universe_1^ @ equiv_path2_universe 1 1 f) @
    path_universe_1) (path_universe g)) @
concat_1p (path_universe g) =
((concat_p1 (path_universe g))^ @
 whiskerL (path_universe g)
   ((path_universe_1^ @ equiv_path2_universe 1 1 f) @
    path_universe_1)) @ concat_p1 (path_universe g)
    refine (equiv_concat_lr _ _).
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: forall Z : BAut X, IsHSet (1 = 1)
f: 1%equiv == 1%equiv
g: X <~> X
((concat_1p (path_universe g))^ @
 whiskerR
   ((path_universe_1^ @ equiv_path2_universe 1 1 f) @
    path_universe_1) (path_universe g)) @
concat_1p (path_universe g) =
path2_universe (fun x : X => ap g (f x))
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: forall Z : BAut X, IsHSet (1 = 1)
f: 1%equiv == 1%equiv
g: X <~> X
path2_universe (fun x : X => f (g x)) =
((concat_p1 (path_universe g))^ @
 whiskerL (path_universe g)
   ((path_universe_1^ @ equiv_path2_universe 1 1 f) @
    path_universe_1)) @ 
concat_p1 (path_universe g)
    -
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: forall Z : BAut X, IsHSet (1 = 1)
f: 1%equiv == 1%equiv
g: X <~> X
((concat_1p (path_universe g))^ @
 whiskerR
   ((path_universe_1^ @ equiv_path2_universe 1 1 f) @
    path_universe_1) (path_universe g)) @
concat_1p (path_universe g) =
path2_universe (fun x : X => ap g (f x)) refine (_ @ (path2_universe_postcompose_idmap f g)^).
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: forall Z : BAut X, IsHSet (1 = 1)
f: 1%equiv == 1%equiv
g: X <~> X
((concat_1p (path_universe g))^ @
 whiskerR
   ((path_universe_1^ @ equiv_path2_universe 1 1 f) @
    path_universe_1) (path_universe g)) @
concat_1p (path_universe g) =
((((concat_1p (path_universe g))^ @
   whiskerR path_universe_1^ (path_universe g)) @
  whiskerR (equiv_path2_universe 1 1 f)
    (path_universe g)) @
 whiskerR path_universe_1 (path_universe g)) @
concat_1p (path_universe g)
      abstract (rewrite !whiskerR_pp, !concat_pp_p; reflexivity).
    -
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: forall Z : BAut X, IsHSet (1 = 1)
f: 1%equiv == 1%equiv
g: X <~> X
path2_universe (fun x : X => f (g x)) =
((concat_p1 (path_universe g))^ @
 whiskerL (path_universe g)
   ((path_universe_1^ @ equiv_path2_universe 1 1 f) @
    path_universe_1)) @ concat_p1 (path_universe g) refine (path2_universe_precompose_idmap f g @ _).
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: forall Z : BAut X, IsHSet (1 = 1)
f: 1%equiv == 1%equiv
g: X <~> X
((((concat_p1 (path_universe g))^ @
   whiskerL (path_universe g) path_universe_1^) @
  whiskerL (path_universe g)
    (equiv_path2_universe 1 1 f)) @
 whiskerL (path_universe g) path_universe_1) @
concat_p1 (path_universe g) =
((concat_p1 (path_universe g))^ @
 whiskerL (path_universe g)
   ((path_universe_1^ @ equiv_path2_universe 1 1 f) @
    path_universe_1)) @ concat_p1 (path_universe g)
      abstract (rewrite !whiskerL_pp, !concat_pp_p; reflexivity).
  Defined.

  (** Once again we compute it on the identity.  In this case it seems to be unavoidable to do some [simpl]ing (or at least [cbn]ing), making this proof somewhat slower. *)
  Definition id_center2_baut `{Univalence} X `{IsTrunc 1 X}
  : center2_baut X (exist
                      (fun (f:forall x:X, x=x) =>
                         forall (g:X<~>X) (x:X), ap g (f x) = f (g x))
                      (fun x => idpath x)
                      (fun (g:X<~>X) (x:X) => idpath (idpath (g x))))
    = fun Z => idpath (idpath Z).
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
center2_baut X
  (fun x : X => 1; fun (g : X <~> X) (x : X) => 1) =
(fun Z : BAut X => 1)
  Proof.
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
center2_baut X
  (fun x : X => 1; fun (g : X <~> X) (x : X) => 1) =
(fun Z : BAut X => 1)
    apply path_forall; intros Z.
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
Z: BAut X
center2_baut X
  (fun x : X => 1; fun (g : X <~> X) (x : X) => 1) Z =
1
    assert (IsHSet (idpath Z.1 = idpath Z.1)) by exact _.
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
Z: BAut X
X0: IsHSet (1 = 1)
center2_baut X
  (fun x : X => 1; fun (g : X <~> X) (x : X) => 1) Z =
1
    baut_reduce.
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: IsHSet (1 = 1)
center2_baut X
  (fun x : X => 1; fun (g : X <~> X) (x : X) => 1) pt =
1
    cbn.
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: IsHSet (1 = 1)
((path_sigma_hprop_1 pt)^ @
 ap (path_sigma_hprop pt pt)
   ((path_universe_1^ @
     equiv_path2_universe 1 1 (fun x : X => 1)) @
    path_universe_1)) @ path_sigma_hprop_1 pt = 1 unfold functor_forall, sig_rect, merely_rec_hset.
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: IsHSet (1 = 1)
((path_sigma_hprop_1 pt)^ @
 ap (path_sigma_hprop pt pt)
   ((path_universe_1^ @
     equiv_path2_universe 1 1 (fun x : X => 1)) @
    path_universe_1)) @ path_sigma_hprop_1 pt = 1 cbn.
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: IsHSet (1 = 1)
((path_sigma_hprop_1 pt)^ @
 ap (path_sigma_hprop pt pt)
   ((path_universe_1^ @
     equiv_path2_universe 1 1 (fun x : X => 1)) @
    path_universe_1)) @ path_sigma_hprop_1 pt = 1
    rewrite equiv_path2_universe_1.
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: IsHSet (1 = 1)
((path_sigma_hprop_1 pt)^ @
 ap (path_sigma_hprop pt pt)
   ((path_universe_1^ @ 1) @ path_universe_1)) @
path_sigma_hprop_1 pt = 1
    rewrite !concat_p1, !concat_Vp.
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: IsHSet (1 = 1)
((path_sigma_hprop_1 pt)^ @
 ap (path_sigma_hprop pt pt) 1) @
path_sigma_hprop_1 pt = 1
    simpl.
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: IsHSet (1 = 1)
((path_sigma_hprop_1 pt)^ @ 1) @ path_sigma_hprop_1 pt =
1
    rewrite !concat_p1, !concat_Vp.
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
X0: IsHSet (1 = 1)
1 = 1
    reflexivity.
  Defined.

End Center2BAut.

Section ClassifyingMaps.

  (** ** Maps into [BAut F] classify bundles with fiber [F] *)

  (** The property of being merely equivalent to a given type [F] defines a subuniverse. *)
  Definition subuniverse_merely_equiv (F : Type) : Subuniverse.
F: Type
Subuniverse
  Proof.
F: Type
Subuniverse
    rapply (Build_Subuniverse (fun E => merely (E <~> F))).
F: Type
forall T U : Type,
merely (T <~> F) ->
forall f : T -> U, IsEquiv f -> merely (U <~> F)
    intros T U mere_eq f iseq_f.
F, T, U: Type
mere_eq: merely (T <~> F)
f: T -> U
iseq_f: IsEquiv f
merely (U <~> F)
    strip_truncations.
F, T, U: Type
f: T -> U
iseq_f: IsEquiv f
mere_eq: T <~> F
merely (U <~> F)
    pose (feq:=Build_Equiv _ _ f iseq_f).
F, T, U: Type
f: T -> U
iseq_f: IsEquiv f
mere_eq: T <~> F
feq:= {| equiv_fun := f; equiv_isequiv := iseq_f |}: T <~> U
merely (U <~> F)
    exact (tr (mere_eq oE feq^-1)).
  Defined.

  (** The universe of O-local types for [subuniverse_merely_equiv F] is equivalent to [BAut F]. *)
  Proposition equiv_baut_typeO `{Univalence} {F : Type}
    :  BAut F <~> Type_ (subuniverse_merely_equiv F).
H: Univalence
F: Type
BAut F <~> Type_ (subuniverse_merely_equiv F)
  Proof.
H: Univalence
F: Type
BAut F <~> Type_ (subuniverse_merely_equiv F)
    srapply equiv_functor_sigma_id; intro X; cbn.
H: Univalence
F, X: Type
Trunc (-1) (X = F) <~> Trunc (-1) (X <~> F)
    rapply Trunc_functor_equiv.
H: Univalence
F, X: Type
X = F <~> (X <~> F)
    exact (equiv_path_universe _ _)^-1%equiv.
  Defined.

  (** Consequently, maps into [BAut F] correspond to bundles with fibers merely equivalent to [F]. *)
  Corollary equiv_map_baut_fibration `{Univalence} {Y : pType} {F : Type}
    : (Y -> BAut F) <~> { p : Slice Y & forall y:Y, merely (hfiber p.2 y <~> F) }.
H: Univalence
Y: pType
F: Type
(Y -> BAut F) <~>
{p : Slice Y &
forall y : Y, merely (hfiber p.2 y <~> F)}
  Proof.
H: Univalence
Y: pType
F: Type
(Y -> BAut F) <~>
{p : Slice Y &
forall y : Y, merely (hfiber p.2 y <~> F)}
    refine (_ oE equiv_postcompose' equiv_baut_typeO).
H: Univalence
Y: pType
F: Type
(Y -> Type_ (subuniverse_merely_equiv F)) <~>
{p : Slice Y &
forall y : Y, merely (hfiber p.2 y <~> F)}
    refine (_ oE equiv_sigma_fibration_O).
H: Univalence
Y: pType
F: Type
{p : {X : Type & X -> Y} &
MapIn (subuniverse_merely_equiv F) p.2} <~>
{p : Slice Y &
forall y : Y, merely (hfiber p.2 y <~> F)}
    snrapply equiv_functor_sigma_id; intro p.
H: Univalence
Y: pType
F: Type
p: {X : Type & X -> Y}
(fun p : {X : Type & X -> Y} =>
 MapIn (subuniverse_merely_equiv F) p.2) p <~>
(fun p : Slice Y =>
 forall y : Y, merely (hfiber p.2 y <~> F)) p
    rapply equiv_functor_forall_id; intro y.
H: Univalence
Y: pType
F: Type
p: {X : Type & X -> Y}
y: Y
In (subuniverse_merely_equiv F) (hfiber p.2 y) <~>
merely (hfiber p.2 y <~> F)
    by apply Trunc_functor_equiv.
  Defined.

  (** The pointed version of [equiv_baut_typeO] above. *)
  Proposition pequiv_pbaut_typeOp@{u v +} `{Univalence} {F : Type@{u}}
    : pBAut@{u v} F <~>* [Type_ (subuniverse_merely_equiv F), (F; tr equiv_idmap)].
H: Univalence
F: Type
pBAut F <~>*
[Type_ (subuniverse_merely_equiv F), (F; tr 1%equiv)]
  Proof.
H: Univalence
F: Type
pBAut F <~>*
[Type_ (subuniverse_merely_equiv F), (F; tr 1%equiv)]
    snrapply Build_pEquiv'; cbn.
H: Univalence
F: Type
BAut F <~> Type_ (subuniverse_merely_equiv F)
H: Univalence
F: Type
?Goal ispointed_baut = (F; tr 1%equiv)
    1: exact equiv_baut_typeO.
H: Univalence
F: Type
equiv_baut_typeO ispointed_baut = (F; tr 1%equiv)
    by apply path_sigma_hprop.
  Defined.

  Definition equiv_pmap_pbaut_pfibration `{Univalence} {Y F : pType@{u}}
    : (Y ->* pBAut@{u v} F) <~> { p : { q : pSlice Y & forall y:Y, merely (hfiber q.2 y <~> F) } &
                                      pfiber p.1.2 <~>* F }
    := (equiv_sigma_pfibration_O (subuniverse_merely_equiv F))
         oE pequiv_pequiv_postcompose pequiv_pbaut_typeOp.

  (** When [Y] is connected, pointed maps into [pBAut F] correspond to maps into the universe sending the base point to [F]. *)
  Proposition equiv_pmap_pbaut_type_p `{Univalence}
              {Y : pType@{u}} {F : Type@{u}} `{IsConnected 0 Y}
    : (Y ->* pBAut F) <~> (Y ->* [Type@{u}, F]).
H: Univalence
Y: pType
F: Type
H0: IsConnected (Tr 0) Y
(Y ->* pBAut F) <~> (Y ->* [Type, F])
  Proof.
H: Univalence
Y: pType
F: Type
H0: IsConnected (Tr 0) Y
(Y ->* pBAut F) <~> (Y ->* [Type, F])
    refine (_ oE pequiv_pequiv_postcompose pequiv_pbaut_typeOp).
H: Univalence
Y: pType
F: Type
H0: IsConnected (Tr 0) Y
(Y ->**
 [Type_ (subuniverse_merely_equiv F), (F; tr 1%equiv)]) <~>
(Y ->* [Type, F])
    rapply equiv_pmap_typeO_type_connected.
  Defined.

  (** When [Y] is connected, [pBAut F] classifies fiber sequences over [Y] with fiber [F]. *)
  Definition equiv_pmap_pbaut_pfibration_connected `{Univalence} {Y F : pType} `{IsConnected 0 Y}
    : (Y ->* pBAut F) <~> { X : pType & FiberSeq F X Y }
    := classify_fiberseq oE equiv_pmap_pbaut_type_p.

End ClassifyingMaps.