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

Local Open Scope pointed_scope.

(** * The object classifier *)

(** We prove that type families correspond to fibrations [equiv_sigma_fibration] (Theorem 4.8.3) and the projection [pointed_type : pType -> Type] is an object classifier [ispullback_square_objectclassifier] (Theorem 4.8.4). *)

(** We denote the type of all maps into a type [Y] as follows, and refer to them "bundles over Y". *)
Definition Slice (Y : Type@{u}) := { X : Type@{u} & X -> Y }.
Definition pSlice (Y : pType@{u}) := { X : pType@{u} & X ->* Y }.

Definition sigma_fibration@{u v} {Y : Type@{u}} (P : Y -> Type@{u}) : Slice@{u v} Y
  := (sig@{u u} P; pr1).

Definition sigma_fibration_inverse {Y : Type@{u}} (p : Slice Y) : Y -> Type@{u}
  := hfiber p.2.

Theorem isequiv_sigma_fibration `{Univalence} {Y : Type}
  : IsEquiv (@sigma_fibration Y).
H: Univalence
Y: Type
IsEquiv sigma_fibration
Proof.
H: Univalence
Y: Type
IsEquiv sigma_fibration
  srapply isequiv_adjointify.
H: Univalence
Y: Type
Slice Y -> Y -> Type
H: Univalence
Y: Type
sigma_fibration o ?g == idmap
H: Univalence
Y: Type
?g o sigma_fibration == idmap
  -
H: Univalence
Y: Type
Slice Y -> Y -> Type exact sigma_fibration_inverse.
  -
H: Univalence
Y: Type
sigma_fibration o sigma_fibration_inverse == idmap intros [X p].
H: Univalence
Y, X: Type
p: X -> Y
sigma_fibration (sigma_fibration_inverse (X; p)) =
(X; p)
    srapply path_sigma; cbn.
H: Univalence
Y, X: Type
p: X -> Y
{x : _ & sigma_fibration_inverse (X; p) x} = X
H: Univalence
Y, X: Type
p: X -> Y
transport (fun X : Type => X -> Y) ?Goal pr1 = p
    +
H: Univalence
Y, X: Type
p: X -> Y
{x : _ & sigma_fibration_inverse (X; p) x} = X exact (path_universe (equiv_fibration_replacement _)^-1%equiv).
    +
H: Univalence
Y, X: Type
p: X -> Y
transport (fun X : Type => X -> Y)
  (path_universe
     (equiv_fibration_replacement (X; p).2)^-1%equiv)
  pr1 = p apply transport_arrow_toconst_path_universe.
  -
H: Univalence
Y: Type
sigma_fibration_inverse o sigma_fibration == idmap intro P.
H: Univalence
Y: Type
P: Y -> Type
sigma_fibration_inverse (sigma_fibration P) = P
    funext y; cbn.
H: Univalence
Y: Type
P: Y -> Type
y: Y
sigma_fibration_inverse (sigma_fibration P) y = P y
    exact ((path_universe (@hfiber_fibration  _ y P))^).
Defined.

(** Theorem 4.8.3. *)
Definition equiv_sigma_fibration `{Univalence} {Y : Type@{u}}
  : (Y -> Type@{u}) <~> { X : Type@{u} & X -> Y }
  := Build_Equiv _ _ _ isequiv_sigma_fibration.

(** The universal map is the forgetful map [pointed_type : pType -> Type]. *)

(** We construct the universal square for the object classifier. *)
Local Definition topmap {A : Type} (P : A -> Type) (e : sig P) : pType
  := [P e.1, e.2].

(** The square commutes definitionally. *)
Definition objectclassifier_square {A : Type} (P : A -> Type)
  : P o pr1 == pointed_type o (topmap P)
  := fun e : sig P => idpath (P e.1).

(** Theorem 4.8.4. *)
Theorem ispullback_objectclassifier_square {A : Type} (P : A -> Type)
  : IsPullback (objectclassifier_square P).
A: Type
P: A -> Type
IsPullback (objectclassifier_square P)
Proof.
A: Type
P: A -> Type
IsPullback (objectclassifier_square P)
  srapply isequiv_adjointify.
A: Type
P: A -> Type
Pullback P pointed_type -> {x : _ & P x}
A: Type
P: A -> Type
pullback_corec (objectclassifier_square P) o ?g ==
idmap
A: Type
P: A -> Type
?g o pullback_corec (objectclassifier_square P) ==
idmap
  -
A: Type
P: A -> Type
Pullback P pointed_type -> {x : _ & P x} intros [a [F p]].
A: Type
P: A -> Type
a: A
F: pType
p: P a = F
{x : _ & P x}
    exact (a; transport idmap p^ (point F)).
  -
A: Type
P: A -> Type
pullback_corec (objectclassifier_square P)
o (fun X : Pullback P pointed_type =>
   (fun (a : A) (proj2 : {c : pType & P a = c}) =>
    (fun (F : pType) (p : P a = F) =>
     (a; transport idmap p^ pt)) proj2.1 proj2.2) X.1
     X.2) == idmap intros [a [[T t] p]]; cbn in p.
A: Type
P: A -> Type
a: A
T: Type
t: IsPointed T
p: P a = T
pullback_corec (objectclassifier_square P)
  (a; transport idmap p^ pt) = (a; [T, t]; p)
    refine (path_sigma' _ (idpath a) _).
A: Type
P: A -> Type
a: A
T: Type
t: IsPointed T
p: P a = T
transport (fun b : A => {c : pType & P b = c}) 1
  (topmap P (a; transport idmap p^ pt);
  objectclassifier_square P (a; transport idmap p^ pt)) =
([T, t]; p)
    by induction p.
  -
A: Type
P: A -> Type
(fun X : Pullback P pointed_type =>
 (fun (a : A) (proj2 : {c : pType & P a = c}) =>
  (fun (F : pType) (p : P a = F) =>
   (a; transport idmap p^ pt)) proj2.1 proj2.2) X.1
   X.2) o pullback_corec (objectclassifier_square P) ==
idmap reflexivity.
Defined.

(** ** Classifying bundles with specified fiber *)

(** Bundles over [B] with fiber [F] correspond to pointed maps into the universe pointed at [F]. *)
Proposition equiv_sigma_fibration_p@{u v +} `{Univalence} {Y : pType@{u}} {F : Type@{u}}
  : (Y ->* [Type@{u}, F]) <~> { p : Slice@{u v} Y & hfiber p.2 (point Y) <~> F }.
H: Univalence
Y: pType
F: Type
(Y ->* [Type, F]) <~>
{p : Slice Y & hfiber p.2 pt <~> F}
Proof.
H: Univalence
Y: pType
F: Type
(Y ->* [Type, F]) <~>
{p : Slice Y & hfiber p.2 pt <~> F}
  refine (_ oE (issig_pmap _ _)^-1).
H: Univalence
Y: pType
F: Type
{f : Y -> [Type, F] & f pt = pt} <~>
{p : Slice Y & hfiber p.2 pt <~> F}
  srapply (equiv_functor_sigma' equiv_sigma_fibration); intro P; cbn.
H: Univalence
Y: pType
F: Type
P: Y -> Type
P pt = F <~> (hfiber pr1 pt <~> F)
  refine (_ oE (equiv_path_universe@{u u v} _ _)^-1%equiv).
H: Univalence
Y: pType
F: Type
P: Y -> Type
(P pt <~> F) <~> (hfiber pr1 pt <~> F)
  refine (equiv_functor_equiv _ equiv_idmap).
H: Univalence
Y: pType
F: Type
P: Y -> Type
P pt <~> hfiber pr1 pt
  apply hfiber_fibration.
Defined.

(** If the fiber [F] is pointed we may upgrade the right-hand side to pointed fiber sequences. *)
Lemma equiv_pfiber_fibration_pfibration@{u v} {Y F : pType@{u}}
  : { p : Slice@{u v} Y & hfiber p.2 (point Y) <~> F}
      <~> { p : pSlice@{u v} Y & pfiber p.2 <~>* F }.
Y, F: pType
{p : Slice Y & hfiber p.2 pt <~> F} <~>
{p : pSlice Y & pfiber p.2 <~>* F}
Proof.
Y, F: pType
{p : Slice Y & hfiber p.2 pt <~> F} <~>
{p : pSlice Y & pfiber p.2 <~>* F}
  equiv_via
    (sig@{v u} (fun X : Type@{u} =>
                  { x : X &
                        { p : X -> Y &
                                  { eq : p x = point Y &
                                         { e : hfiber p (point Y) <~> F
                                               & e^-1 (point F) = (x; eq) } } } })).
Y, F: pType
{p : Slice Y & hfiber p.2 pt <~> F} <~>
{X : Type &
{x : X &
{p : X -> Y &
{eq : p x = pt &
{e : hfiber p pt <~> F & e^-1 pt = (x; eq)}}}}}
Y, F: pType
{X : Type &
{x : X &
{p : X -> Y &
{eq : p x = pt &
{e : hfiber p pt <~> F & e^-1 pt = (x; eq)}}}}} <~>
{p : pSlice Y & pfiber p.2 <~>* F}
  -
Y, F: pType
{p : Slice Y & hfiber p.2 pt <~> F} <~>
{X : Type &
{x : X &
{p : X -> Y &
{eq : p x = pt &
{e : hfiber p pt <~> F & e^-1 pt = (x; eq)}}}}} refine (_ oE _).
Y, F: pType
?Goal0 <~>
{X : Type &
{x : X &
{p : X -> Y &
{eq : p x = pt &
{e : hfiber p pt <~> F & e^-1 pt = (x; eq)}}}}}
Y, F: pType
{p : Slice Y & hfiber p.2 pt <~> F} <~> ?Goal0
    +
Y, F: pType
?Goal0 <~>
{X : Type &
{x : X &
{p : X -> Y &
{eq : p x = pt &
{e : hfiber p pt <~> F & e^-1 pt = (x; eq)}}}}} do 5 (rapply equiv_functor_sigma_id; intro).
Y, F: pType
a: Type
a0: a
a1: a -> Y
a2: a1 a0 = pt
a3: hfiber a1 pt <~> F
?Goal1 a3 <~> a3^-1 pt = (a0; a2)
      apply equiv_path_sigma.
    +
Y, F: pType
{p : Slice Y & hfiber p.2 pt <~> F} <~>
{a : Type &
{a0 : a &
{a1 : a -> Y &
{a2 : a1 a0 = pt &
{a3 : hfiber a1 pt <~> F &
{p : (a3^-1 pt).1 = (a0; a2).1 &
transport (fun x : a => a1 x = pt) p (a3^-1 pt).2 =
(a0; a2).2}}}}}} cbn; make_equiv_contr_basedpaths.
  -
Y, F: pType
{X : Type &
{x : X &
{p : X -> Y &
{eq : p x = pt &
{e : hfiber p pt <~> F & e^-1 pt = (x; eq)}}}}} <~>
{p : pSlice Y & pfiber p.2 <~>* F} refine (_ oE _).
Y, F: pType
?Goal <~> {p : pSlice Y & pfiber p.2 <~>* F}
Y, F: pType
{X : Type &
{x : X &
{p : X -> Y &
{eq : p x = pt &
{e : hfiber p pt <~> F & e^-1 pt = (x; eq)}}}}} <~>
?Goal
    2: {
Y, F: pType
{X : Type &
{x : X &
{p : X -> Y &
{eq : p x = pt &
{e : hfiber p pt <~> F & e^-1 pt = (x; eq)}}}}} <~>
?Goal do 5 (rapply equiv_functor_sigma_id; intro).
Y, F: pType
a: Type
a0: a
a1: a -> Y
a2: a1 a0 = pt
a3: hfiber a1 pt <~> F
a3^-1 pt = (a0; a2) <~> ?Goal0 a3
         exact (equiv_path_inverse _ _ oE equiv_moveL_equiv_M _ _). }
Y, F: pType
{a : Type &
{a0 : a &
{a1 : a -> Y &
{a2 : a1 a0 = pt &
{a3 : hfiber a1 pt <~> F & a3 (a0; a2) = pt}}}}} <~>
{p : pSlice Y & pfiber p.2 <~>* F}
    make_equiv.
Defined.

Definition equiv_sigma_pfibration@{u v +} `{Univalence} {Y F : pType@{u}}
  : (Y ->* [Type@{u}, F]) <~> { p : pSlice@{u v} Y & pfiber p.2 <~>* F}
  := equiv_pfiber_fibration_pfibration oE equiv_sigma_fibration_p.

(** * The classifier for O-local types *)

(** Families of O-local types correspond to bundles with O-local fibers. *)
Theorem equiv_sigma_fibration_O@{u v} `{Univalence} {O : Subuniverse} {Y : Type@{u}}
  : (Y -> Type_@{u v} O) <~> { p : { X : Type@{u} & X -> Y } & MapIn O p.2 }.
H: Univalence
O: Subuniverse
Y: Type
(Y -> Type_ O) <~>
{p : {X : Type & X -> Y} & MapIn O p.2}
Proof.
H: Univalence
O: Subuniverse
Y: Type
(Y -> Type_ O) <~>
{p : {X : Type & X -> Y} & MapIn O p.2}
  refine (_ oE (equiv_sig_coind@{u v u v v v u} _ _)^-1).
H: Univalence
O: Subuniverse
Y: Type
{f : Y -> Type & forall x : Y, In O (f x)} <~>
{p : {X : Type & X -> Y} & MapIn O p.2}
  apply (equiv_functor_sigma'@{v u v v v v} equiv_sigma_fibration@{u v}); intro P; cbn.
H: Univalence
O: Subuniverse
Y: Type
P: Y -> Type
(forall x : Y, In O (P x)) <~> MapIn O pr1
  rapply equiv_forall_inO_mapinO_pr1.
Defined.

(** ** Classifying O-local bundles with specified fiber *)

(** We consider a pointed base [Y], and the universe of O-local types [Type_ O] pointed at some O-local type [F]. *)

(** Pointed maps into [Type_ O] correspond to O-local bundles with fiber [F] over the base point of [Y]. *)
Proposition equiv_sigma_fibration_Op@{u v +} `{Univalence} {O : Subuniverse}
            {Y : pType@{u}} {F : Type@{u}} `{inO : In O F}
  : (Y ->* [Type_ O, (F; inO)])
      <~> { p : { q : Slice@{u v} Y & MapIn O q.2 } & hfiber p.1.2 (point Y) <~> F }.
H: Univalence
O: Subuniverse
Y: pType
F: Type
inO: In O F
(Y ->* [Type_ O, (F; inO)]) <~>
{p : {q : Slice Y & MapIn O q.2} &
hfiber (p.1).2 pt <~> F}
Proof.
H: Univalence
O: Subuniverse
Y: pType
F: Type
inO: In O F
(Y ->* [Type_ O, (F; inO)]) <~>
{p : {q : Slice Y & MapIn O q.2} &
hfiber (p.1).2 pt <~> F}
  refine (_ oE (issig_pmap _ _)^-1); cbn.
H: Univalence
O: Subuniverse
Y: pType
F: Type
inO: In O F
{f : Y -> Type_ O & f pt = (F; inO)} <~>
{p : {q : Slice Y & MapIn O q.2} &
hfiber (p.1).2 pt <~> F}
  srapply (equiv_functor_sigma' equiv_sigma_fibration_O); intro P; cbn.
H: Univalence
O: Subuniverse
Y: pType
F: Type
inO: In O F
P: Y -> Type_ O
P pt = (F; inO) <~> (hfiber pr1 pt <~> F)
  refine (_ oE (equiv_path_sigma_hprop _ _)^-1%equiv); cbn.
H: Univalence
O: Subuniverse
Y: pType
F: Type
inO: In O F
P: Y -> Type_ O
(P pt).1 = F <~> (hfiber pr1 pt <~> F)
  refine (_ oE (equiv_path_universe _ _)^-1%equiv).
H: Univalence
O: Subuniverse
Y: pType
F: Type
inO: In O F
P: Y -> Type_ O
((P pt).1 <~> F) <~> (hfiber pr1 pt <~> F)
  refine (equiv_functor_equiv _ equiv_idmap).
H: Univalence
O: Subuniverse
Y: pType
F: Type
inO: In O F
P: Y -> Type_ O
(P pt).1 <~> hfiber pr1 pt
  exact (hfiber_fibration (point Y) _).
Defined.

(** When the base [Y] is connected, the fibers being O-local follow from the fact that the fiber [F] over the base point is. *)
Proposition equiv_sigma_fibration_Op_connected@{u v +} `{Univalence} {O : Subuniverse}
            {Y : pType@{u}} `{IsConnected 0 Y} {F : Type@{u}} `{inO : In O F}
  : (Y ->* [Type_ O, (F; inO)])
       <~> { p : Slice@{u v} Y & hfiber p.2 (point Y) <~> F }.
H: Univalence
O: Subuniverse
Y: pType
H0: IsConnected (Tr 0) Y
F: Type
inO: In O F
(Y ->* [Type_ O, (F; inO)]) <~>
{p : Slice Y & hfiber p.2 pt <~> F}
Proof.
H: Univalence
O: Subuniverse
Y: pType
H0: IsConnected (Tr 0) Y
F: Type
inO: In O F
(Y ->* [Type_ O, (F; inO)]) <~>
{p : Slice Y & hfiber p.2 pt <~> F}
  refine (_ oE equiv_sigma_fibration_Op).
H: Univalence
O: Subuniverse
Y: pType
H0: IsConnected (Tr 0) Y
F: Type
inO: In O F
{p : {q : Slice Y & MapIn O q.2} &
hfiber (p.1).2 pt <~> F} <~>
{p : Slice Y & hfiber p.2 pt <~> F}
  refine (_ oE (equiv_sigma_assoc' _ (fun p _ => hfiber p.2 (point Y) <~> F))^-1%equiv).
H: Univalence
O: Subuniverse
Y: pType
H0: IsConnected (Tr 0) Y
F: Type
inO: In O F
{a : {X : Type & X -> Y} &
{_ : MapIn O a.2 & hfiber a.2 pt <~> F}} <~>
{p : Slice Y & hfiber p.2 pt <~> F}
  srapply equiv_functor_sigma_id; intro; cbn.
H: Univalence
O: Subuniverse
Y: pType
H0: IsConnected (Tr 0) Y
F: Type
inO: In O F
a: {X : Type & X -> Y}
{_ : MapIn O a.2 & hfiber a.2 pt <~> F} <~>
(hfiber a.2 pt <~> F)
  refine (_ oE equiv_sigma_symm0 _ _).
H: Univalence
O: Subuniverse
Y: pType
H0: IsConnected (Tr 0) Y
F: Type
inO: In O F
a: {X : Type & X -> Y}
{_ : hfiber a.2 pt <~> F & MapIn O a.2} <~>
(hfiber a.2 pt <~> F)
  apply equiv_sigma_contr; intro e.
H: Univalence
O: Subuniverse
Y: pType
H0: IsConnected (Tr 0) Y
F: Type
inO: In O F
a: {X : Type & X -> Y}
e: hfiber a.2 pt <~> F
Contr (MapIn O a.2)
  rapply contr_inhabited_hprop.
H: Univalence
O: Subuniverse
Y: pType
H0: IsConnected (Tr 0) Y
F: Type
inO: In O F
a: {X : Type & X -> Y}
e: hfiber a.2 pt <~> F
MapIn O a.2
  rapply conn_point_elim.
H: Univalence
O: Subuniverse
Y: pType
H0: IsConnected (Tr 0) Y
F: Type
inO: In O F
a: {X : Type & X -> Y}
e: hfiber a.2 pt <~> F
In O (hfiber a.2 pt)
  exact (inO_equiv_inO F e^-1).
Defined.

(** *** Classifying O-local bundles with specified pointed fiber *)

(** When the fiber [F] is pointed, the right-hand side can be upgraded to pointed fiber sequences with O-local fibers.  *)
Proposition equiv_sigma_pfibration_O `{Univalence} (O : Subuniverse)
            {Y F : pType} `{inO : In O F}
  : (Y ->* [Type_ O, (pointed_type F; inO)])
      <~> { p : { q : pSlice Y & MapIn O q.2 } & pfiber p.1.2 <~>* F }.
H: Univalence
O: Subuniverse
Y, F: pType
inO: In O F
(Y ->* [Type_ O, (F; inO)]) <~>
{p : {q : pSlice Y & MapIn O q.2} &
pfiber (p.1).2 <~>* F}
Proof.
H: Univalence
O: Subuniverse
Y, F: pType
inO: In O F
(Y ->* [Type_ O, (F; inO)]) <~>
{p : {q : pSlice Y & MapIn O q.2} &
pfiber (p.1).2 <~>* F}
  refine (_ oE equiv_sigma_fibration_Op).
H: Univalence
O: Subuniverse
Y, F: pType
inO: In O F
{p : {q : Slice Y & MapIn O q.2} &
hfiber (p.1).2 pt <~> F} <~>
{p : {q : pSlice Y & MapIn O q.2} &
pfiber (p.1).2 <~>* F}
  refine (_ oE equiv_sigma_symm' _ (fun q => hfiber q.2 (point Y) <~> F)).
H: Univalence
O: Subuniverse
Y, F: pType
inO: In O F
{aq : {a : {X : Type & X -> Y} & hfiber a.2 pt <~> F}
& MapIn O (aq.1).2} <~>
{p : {q : pSlice Y & MapIn O q.2} &
pfiber (p.1).2 <~>* F}
  refine (equiv_sigma_symm' (fun q => pfiber q.2 <~>* F) _ oE _).
H: Univalence
O: Subuniverse
Y, F: pType
inO: In O F
{aq : {a : {X : Type & X -> Y} & hfiber a.2 pt <~> F}
& MapIn O (aq.1).2} <~>
{ap : {a : {X : pType & X ->* Y} & pfiber a.2 <~>* F}
& MapIn O (ap.1).2}
  by rapply (equiv_functor_sigma' equiv_pfiber_fibration_pfibration).
Defined.

(** When moreover the base [Y] is connected, the right-hand side is exactly the type of pointed fiber sequences, since the fibers being O-local follow from [F] being O-local and [Y] connected. *)
Definition equiv_sigma_pfibration_O_connected@{u v +} `{Univalence} (O : Subuniverse)
          {Y F : pType@{u}} `{IsConnected 0 Y} `{inO : In O F}
  : (Y ->* [Type_ O, (pointed_type F; inO)])
      <~> { p : pSlice@{u v} Y & pfiber p.2 <~>* F }
  := equiv_pfiber_fibration_pfibration oE equiv_sigma_fibration_Op_connected.

(** As a corollary, pointed maps into the universe of O-local types are just pointed maps into the universe, when the base [Y] is connected. *)
Definition equiv_pmap_typeO_type_connected `{Univalence} {O : Subuniverse}
      {Y : pType@{u}} `{IsConnected 0 Y} {F : Type@{u}} `{inO : In O F}
  : (Y ->* [Type_ O, (F; inO)]) <~> (Y ->* [Type@{u}, F])
  := equiv_sigma_fibration_p^-1 oE equiv_sigma_fibration_Op_connected.