Update ObjectClassifier.v and classify maps into BAut.

contrib/HoTTBook.v

@@ -695,12 +695,12 @@ Definition Book_4_8_2 := @HoTT.HFiber.equiv_fibration_replacement.
 (* ================================================== thm:nobject-classifier-appetizer *)
 (** Theorem 4.8.3 *)
 
-Definition Book_4_8_3 := @HoTT.ObjectClassifier.FamequivPow.
+Definition Book_4_8_3 := @HoTT.ObjectClassifier.equiv_sigma_fibration.
 
 (* ================================================== thm:object-classifier *)
 (** Theorem 4.8.4 *)
 
-Definition Book_4_8_4 := @HoTT.ObjectClassifier.objclasspb_is_fibrantreplacement.
+Definition Book_4_8_4 := @HoTT.ObjectClassifier.ispullback_objectclassifier_square.
 
 (* ================================================== weakfunext *)
 (** Definition 4.9.1 *)

theories/Basics/Overture.v

@@ -764,7 +764,7 @@ Class IsPointed (A : Type) := point : A.
 
 Arguments point A {_}.
 
-Record pType :=
+Cumulative Record pType :=
   { pointed_type : Type ;
     ispointed_type : IsPointed pointed_type }.
 

theories/Homotopy/ExactSequence.v

@@ -6,6 +6,7 @@ Require Import Pointed.
 Require Import ReflectiveSubuniverse Modality Modalities.Identity Modalities.Descent.
 Require Import Truncations.
 Require Import HFiber.
+Require Import ObjectClassifier.
 
 Local Open Scope succ_scope.
 Open Scope pointed_scope.
@@ -236,7 +237,7 @@ Global Instance isexact_pfib {X Y} (f : X ->* Y)
 Proof.
   exists (iscomplex_pfib f).
   exact _.
-Defined.    
+Defined.
 
 (** Fiber sequences can alternatively be defined as an equivalence to the fiber of some map. *)
 Definition FiberSeq (F X Y : pType) := { f : X ->* Y & F <~>* pfiber f }.
@@ -445,3 +446,16 @@ Definition Pi_les `{Univalence} {F X Y : pType} (i : F ->* X) (f : X ->* Y)
            `{IsExact purely F X Y i f}
   : LongExactSequence (Tr (-1)) (N3)
   := trunc_les (-1) (loops_les i f).
+
+(** * Classifying fiber sequences *)
+
+(** Fiber sequences correspond to pointed maps into the universe. *)
+Definition classify_fiberseq `{Univalence} {Y F : pType@{u}}
+  : (Y ->* Build_pType Type@{u} F) <~> { X : pType@{u} & FiberSeq F X Y }.
+Proof.
+  refine (_ oE _).
+  (** To apply [equiv_sigma_pfibration] we need to invert the equivalence on the fiber. *)
+  { do 2 (rapply equiv_functor_sigma_id; intro).
+    apply equiv_pequiv_inverse. }
+  exact ((equiv_sigma_assoc _ _)^-1 oE equiv_sigma_pfibration).
+Defined.

theories/ObjectClassifier.v

@@ -1,118 +1,174 @@
-(** We prove that Fam and Pow are equivalent.
-This equivalence is close to the existence of an object classifier.
-*)
+Require Import HoTT.Basics HoTT.Types HFiber Pullback Pointed Truncations.
+Require Import Modalities.ReflectiveSubuniverse Modalities.Identity.
 
-Require Import HoTT.Basics HoTT.Types.
-Require Import HFiber Pullback.
+Local Open Scope pointed_scope.
 
-Local Open Scope path_scope.
+(** * The object classifier *)
 
-Section AssumeUnivalence.
-Context `{ua:Univalence}.
+(** 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). *)
 
-Section FamPow.
-(** We consider Families and Powers over a fixed type [A] *)
-Variable A : Type.
-Definition Fam A:=sig (fun I:Type  => I->A).
-Definition p2f: (A->Type)-> Fam A:=  fun Q:(A->Type) => ( (sig Q) ; @pr1 _ _).
-Definition f2p: Fam A -> (A->Type):=
- fun F => let (I, f) := F in (fun a => (hfiber f a)).
+(** 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 }.
 
-(* This is generalized in Functorish.v *)
-Theorem transport_exp (U V:Type)(w:U<~>V): forall (f:U->A),
-  (transport (fun I:Type => I->A) (path_universe w) f) = (f o w^-1).
+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).
 Proof.
-  intros f; apply path_arrow; intros y.
-  refine (transport_arrow_toconst _ _ _ @ _).
-  apply ap.
-  by apply transport_path_universe_V.
-Qed.
+  srapply isequiv_adjointify.
+  - exact sigma_fibration_inverse.
+  - intros [X p].
+    srapply path_sigma; cbn.
+    + exact (path_universe (equiv_fibration_replacement _)^-1%equiv).
+    + apply transport_arrow_toconst_path_universe.
+  - intro P.
+    funext y; cbn.
+    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]. *)
 
-Theorem FamequivPow : (A->Type)<~>(Fam A).
+(** We construct the universal square for the object classifier. *)
+Local Definition topmap {A : Type} (P : A -> Type) (e : sig P) : pType
+  := Build_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).
 Proof.
-apply (equiv_adjointify p2f f2p).
-(* Theorem right (F:Fam A) : F = (p2ff2p F) *)
- +intros [I f]. set (e:=equiv_path_sigma _ (@exist Type (fun I0 : Type => I0 -> A) I f)
-  ({a : A & hfiber f a} ; @pr1 _ _)). simpl in e.
-  enough (X:{p : I = {a : A & @hfiber I A f a} &
-     @transport _ (fun I0 : Type => I0 -> A) _ _ p f = @pr1 _ _}) by apply (e X)^.
-  set (w:=@equiv_fibration_replacement A I f).
-  exists (path_universe w). 
-  transitivity (f o w^-1);[apply transport_exp|apply path_forall;by (intros [a [i p]])].
- (* Theorem left (P:A -> Type) : (f2pp2f P) = P *)
- + intro P. by_extensionality a.
- apply ((path_universe (@hfiber_fibration  _ a P))^).
+  srapply isequiv_adjointify.
+  - intros [a [F p]].
+    exact (a; transport idmap p^ (point F)).
+  - intros [a [[T t] p]]; cbn in p.
+    refine (path_sigma' _ (idpath a) _).
+    by induction p.
+  - reflexivity.
 Defined.
 
-(** We construct the universal diagram for the object classifier *)
-Definition topmap {B} (f:B->A) (b:B): pType :=
-  Build_pType (hfiber f (f b)) (b ; idpath (f b)).
+(** ** Classifying bundles with specified fiber *)
 
-Local Definition help_objclasspb_is_fibrantreplacement (P:A-> Type): (sig P)->
-  (Pullback P (@pr1 _ (fun u :Type => u))):=
-(fun (X : {a : A & P a}) => (fun (a : A) (q : P a) => (a; ((P a; q); 1))) X.1 X.2).
+Local Notation "( X , x )" := (Build_pType X x).
 
-Local Definition help_objclasspb_is_fibrantreplacement2 (P:A-> Type):
- (Pullback P (@pr1 _ (fun u :Type => u))) -> (sig P).
-intros [a [[T t] p]]. exact (a;(transport (fun X => X) (p^) t)).
+(** 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 }.
+Proof.
+  refine (_ oE (issig_pmap _ _)^-1).
+  srapply (equiv_functor_sigma' equiv_sigma_fibration); intro P; cbn.
+  refine (_ oE (equiv_path_universe@{u u v} _ _)^-1%equiv).
+  refine (equiv_functor_equiv _ equiv_idmap).
+  apply hfiber_fibration.
 Defined.
 
-Lemma objclasspb_is_fibrantreplacement (P:A-> Type): (sig P) <~> (Pullback P (@pr1 _ (fun u :Type => u))).
+(** 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 }.
 Proof.
-exists (help_objclasspb_is_fibrantreplacement P).
-srapply isequiv_adjointify.
-- exact (help_objclasspb_is_fibrantreplacement2 P).
-- intros [a [[T t] p]].
-  refine (path_sigma' _ (idpath a) _).
-  simpl in p. by path_induction.
-- intros [a p]; apply idpath.
+  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) } } } })).
+  - refine (_ oE _).
+    + do 5 (rapply equiv_functor_sigma_id; intro).
+      apply equiv_path_sigma.
+    + make_equiv_contr_basedpaths.
+  - refine (_ oE _).
+    2: { do 5 (rapply equiv_functor_sigma_id; intro).
+         exact (equiv_path_inverse _ _ oE equiv_moveL_equiv_M _ _). }
+    make_equiv.
 Defined.
 
-End FamPow.
-
-Section Subobjectclassifier.
-(** We prove that hProp is the subobject classifier *)
-(** In fact, the proof works for general mere predicates on [Type], 
-not just [IsHProp], truncations and modalities are important examples.*)
-Variable A : Type.
-Variable isP : Type -> Type.
-Variable ishprop_isP : forall I, IsHProp (isP I).
-Definition IsPfibered {I} (f:I->A):=forall i, isP (hfiber f i).
-Definition PFam := (sig (fun F:Fam A => IsPfibered (pr2 F))).
-(* Bug: abstract should accept more than one tactic.
-https://coq.inria.fr/bugs/show_bug.cgi?id=3609
-Alternatively, we would like to use [Program] here.
-6a99db1c31fe267fdef7be755fa169fb6a87e3cf
-Instead we split the [Definition] and first make a [Local Definition] *)
-Local Definition pow2Pfam_pf (P:forall a:A, {X :Type & isP X}): 
-           IsPfibered (pr2 (p2f A (pr1 o P))). 
+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 }.
 Proof.
-intro i. cbn. 
-rewrite <- (path_universe_uncurried (@hfiber_fibration A i (pr1 o P))).
-apply ((P i).2).
-Qed.
+  refine (_ oE (equiv_sig_coind _ _)^-1).
+  apply (equiv_functor_sigma' equiv_sigma_fibration); intro P; cbn.
+  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]. *)
 
-Definition pow2Pfam (P:forall a:A, {X :Type & isP X}): PFam:=
-  (p2f A (fun a => (pr1 (P a))); pow2Pfam_pf P).
+(** 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 }.
+Proof.
+  refine (_ oE (issig_pmap _ _)^-1); cbn.
+  srapply (equiv_functor_sigma' equiv_sigma_fibration_O); intro P; cbn.
+  refine (_ oE (equiv_path_sigma_hprop _ _)^-1%equiv); cbn.
+  refine (_ oE (equiv_path_universe _ _)^-1%equiv).
+  refine (equiv_functor_equiv _ equiv_idmap).
+  exact (hfiber_fibration (point Y) _).
+Defined.
 
-Local Definition Pfam2pow_pf (F:PFam)(a:A):isP (f2p A F.1 a). 
-unfold f2p. by destruct F as [[I f] p].
-Qed.
+(** 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 }.
+Proof.
+  refine (_ oE equiv_sigma_fibration_Op).
+  refine (_ oE (equiv_sigma_assoc' _ (fun p _ => hfiber p.2 (point Y) <~> F))^-1%equiv).
+  srapply equiv_functor_sigma_id; intro; cbn.
+  refine (_ oE equiv_sigma_symm0 _ _).
+  apply equiv_sigma_contr; intro e.
+  rapply contr_inhabited_hprop.
+  rapply conn_point_elim@{u v u u u u u u u}.
+  apply (inO_equiv_inO F e^-1).
+Defined.
 
-Definition Pfam2pow (F:PFam) (a:A): {X :Type & isP X}:=
-   ((f2p A F.1 a); (Pfam2pow_pf F a)).
+(** *** Classifying O-local bundles with specified pointed fiber *)
 
-Theorem PowisoPFam : (forall a:A, {X :Type & isP X})<~>PFam.
+(** 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 }.
 Proof.
-apply (equiv_adjointify pow2Pfam Pfam2pow).
- + intros [[B f] q]. apply path_sigma_hprop. cbn.
-  refine (@eisretr _ _ (FamequivPow A) _ (B;f)).
-+ intro P. apply path_forall. intro a.
- assert (f2p A (p2f A (pr1 o P)) a = (pr1 (P a))).
-- set (p:=@eissect _ _ (FamequivPow A) _).
-  apply (ap10 (p (pr1 o P)) a).
-- by apply path_sigma_hprop.
+  refine (_ oE equiv_sigma_fibration_Op).
+  refine (_ oE equiv_sigma_symm' _ (fun q => hfiber q.2 (point Y) <~> F)).
+  refine (equiv_sigma_symm' (fun q => pfiber q.2 <~>* F) _ oE _).
+  by rapply (equiv_functor_sigma' equiv_pfiber_fibration_pfibration).
 Defined.
-End Subobjectclassifier.
 
-End AssumeUnivalence.
+(** 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 unverse 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.

theories/Pointed/Core.v

@@ -49,7 +49,7 @@ Class IsTrunc_pFam n {A} (X : pFam A)
   := trunc_pfam_is_trunc : forall x, IsTrunc n (X.1 x).
 
 (** Pointed dependent functions *)
-Record pForall (A : pType) (P : pFam A) := {
+Cumulative Record pForall (A : pType) (P : pFam A) := {
   pointed_fun : forall x, P x ;
   dpoint_eq : pointed_fun (point A) = dpoint P ;
 }.

theories/Pointed/Loops.v

@@ -370,7 +370,8 @@ Local Notation "( X , x )" := (Build_pType X x).
 
 (* We can convert between families of loops in a type and loops in Type at that type. *)
 Definition loops_type@{i j k} `{Univalence} (A : Type@{i})
-  : pEquiv@{j j k} (loops@{j} (Type@{i}, A)) (A <~> A, equiv_idmap).
+  : pEquiv@{j j k} (loops@{j} (Build_pType@{j} Type@{i} A))
+          (A <~> A, equiv_idmap).
 Proof.
   apply issig_pequiv'.
   exists (equiv_equiv_path A A).

theories/Pointed/pEquiv.v

@@ -116,3 +116,11 @@ Definition equiv_pequiv_precompose `{Funext} {A B C : pType} (f : A <~>* B)
 Definition equiv_pequiv_postcompose `{Funext} {A B C : pType} (f : B <~>* C)
   : (A ->* B) <~> (A ->* C)
   := equiv_postcompose_cat_equiv f.
+
+Proposition equiv_pequiv_inverse `{Funext} {A B : pType}
+  : (A <~>* B) <~> (B <~>* A).
+Proof.
+  refine (issig_pequiv' _ _ oE _ oE (issig_pequiv' A B)^-1).
+  srapply (equiv_functor_sigma' (equiv_equiv_inverse _ _)); intro e; cbn.
+  exact (equiv_moveR_equiv_V _ _ oE equiv_path_inverse _ _).
+Defined.