From 9caf5b0df865f3231dcee65fe072651dc9366d27 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sun, 18 Feb 2024 23:44:39 +0000 Subject: [PATCH 1/3] join construction Signed-off-by: Ali Caglayan --- theories/Colimits/Sequential.v | 6 +- theories/Homotopy/JoinConstruction.v | 324 +++++++++++++++++++++++++++ 2 files changed, 327 insertions(+), 3 deletions(-) create mode 100644 theories/Homotopy/JoinConstruction.v diff --git a/theories/Colimits/Sequential.v b/theories/Colimits/Sequential.v index a42de66a1ab..61d3cda4b7d 100644 --- a/theories/Colimits/Sequential.v +++ b/theories/Colimits/Sequential.v @@ -13,8 +13,8 @@ Local Open Scope nat_scope. Local Open Scope path_scope. (** [coe] is [transport idmap : (A = B) -> (A -> B)], but is described as the underlying map of an equivalence so that Coq knows that it is an equivalence. *) -Notation coe := (fun p => equiv_fun (equiv_path _ _ p)). -Notation "a ^+" := (@arr sequence_graph _ _ _ 1 a). +Local Notation coe := (fun p => equiv_fun (equiv_path _ _ p)). +Local Notation "a ^+" := (@arr sequence_graph _ _ _ 1 a). (** Mapping spaces into hprops from colimits of sequences can be characterized. *) Lemma equiv_colim_seq_rec `{Funext} (A : Sequence) (P : Type) `{IsHProp P} @@ -271,7 +271,7 @@ Coercion fibSequence : FibSequence >-> Funclass. Arguments fibSequence {A}. Arguments fibSequenceArr {A}. -Notation "b ^+f" := (fibSequenceArr _ _ b). +Local Notation "b ^+f" := (fibSequenceArr _ _ b). (** The Sigma of a fibered type sequence; Definition 4.3. *) Definition sig_seq {A} (B : FibSequence A) : Sequence. diff --git a/theories/Homotopy/JoinConstruction.v b/theories/Homotopy/JoinConstruction.v new file mode 100644 index 00000000000..e7fa2d24292 --- /dev/null +++ b/theories/Homotopy/JoinConstruction.v @@ -0,0 +1,324 @@ +Require Import Basics Types. +Require Import Limits.Pullback Colimits.Pushout Diagrams.Diagram Diagrams.Sequence Colimits.Colimit Colimits.Sequential. +Require Import Join.Core. +Require Import NullHomotopy. + +(** * The Join Construction *) + +(** ** Propositional Truncation *) + +(** Instead of using the propositional truncation defined in Truncations.Core, we instead give a simpler definition here out of simple HITs. This way we can break dependencies and also manage universe levels better. *) +(** TODO: this should be used in Truncations.Core instead of the other definition. *) + +Definition merely@{i j} (A : Type@{i}) : Type@{j}. +Proof. + (** The propositional truncation of a type will be the infinite join power, or the colimit of the sequence of the nth join power. First we define this sequence. *) + transparent assert (s : Sequence@{j j j}). + { snrapply Build_Sequence. + - exact (iterated_join A). + - intros n. + apply pushr. } + (** Then we define the colimit of this sequence. *) + exact (Colimit s). +Defined. + +Definition merely_in@{i j} {A : Type@{i}} (x : A) : merely A. +Proof. + snrapply colim. + 1: exact O. + exact x. +Defined. + +(** A sequence of null-homotopic maps has a contractible colimit. This is already proven in Sequential.v but we state the hypotheses a little differently here. *) +Lemma contr_seq_colimit_nullhomotopic `{Funext} (s : Sequence) (x : s O) + (is_null : forall n : nat, NullHomotopy (@arr (sequence_graph) s n n.+1%nat idpath)) + : Contr (Colimit s). +Proof. + snrapply contr_colim_seq_into_prop. + - intros n. + destruct n. + + exact x. + + exact (is_null n).1. + - intros n y. + symmetry. + exact ((is_null n).2 y). +Defined. + +Definition merely_rec@{i j k} (A : Type@{i}) (P : Type@{j}) `{IsHProp P} + : (A -> P) -> merely@{i k} A -> P. +Proof. + intros f. + apply Colimit_rec@{i k k k k k k}. + snrapply Cocone.Build_Cocone. + 2: intros ? ? ? ?; nrapply path_ishprop; exact _. + simpl. + intros n. + induction n. + 1: exact f. + snrapply Join_rec. + - exact f. + - exact IHn. + - intros ? ?; nrapply path_ishprop; exact _. +Defined. + +(* TODO: move *) +Lemma nullhomotopy_joinr (A B : Type) (x : A) : NullHomotopy (@joinr A B). +Proof. + exists (joinl x). + intros y. + symmetry. + apply jglue. +Defined. + +(* TODO: move *) +Lemma nullhomotopy_joinl (A B : Type) (y : B) : NullHomotopy (@joinl A B). +Proof. + exists (joinr y). + intros x. + apply jglue. +Defined. + +Global Instance ishprop_merely@{i j} `{Funext} (A : Type@{i}) + : IsHProp (merely@{i j} A). +Proof. + apply hprop_inhabited_contr. + rapply merely_rec. + intros x. + apply contr_seq_colimit_nullhomotopic. + - exact x. + - intros m. + simpl. + apply nullhomotopy_joinr. + exact x. +Defined. + +(** We can construct the homotopy image of a map [f : A -> B] using this definition of propositional truncation, which we will later show to be essentially small. *) +Definition himage@{i j} {A : Type@{i}} {B : Type@{j}} (f : A -> B) : Type@{j} + := {y : B & merely@{j j} (hfiber f y)}. + +(** ** Essentially Small and Locally Small Types *) + +(** A type in a universe [v] is essentially small, with respect to a strictly smaller universe [u], if there is a type in the universe [u] that is equivalent to it. *) +Definition IsEssentiallySmall@{u v | u < v} (A : Type@{v}) + := {B : Type@{u} & A <~> B}. + +(** A type is locally small if all of its path types are essentially small. *) +Definition IsLocallySmall@{u v | u < v} (A : Type@{v}) + := forall x y : A, IsEssentiallySmall@{u v} (x = y). + +(** Under univalence, being essentially small is a proposition. *) +Global Instance ishprop_isessentiallysmall@{u v} `{Univalence} (A : Type@{v}) + : IsHProp (IsEssentiallySmall@{u v} A). +Proof. + apply hprop_allpath. + intros [X e] [X' e']. + snrapply path_sigma. + - apply path_universe_uncurried. + exact (e' oE e^-1). + - apply path_equiv. + lhs nrapply (transport_equiv' (path_universe_uncurried (e' oE e^-1)) e). + funext x; simpl. + rewrite transport_const. + rewrite transport_path_universe. + apply ap, eissect. +Defined. + +(** Therefore, so is being locally small. *) +Global Instance ishprop_islocallysmall@{u v} `{Univalence} (A : Type@{v}) + : IsHProp (IsEssentiallySmall@{u v} A) := _. + +(** A sigma type is essentially small if both of its types are essentially small. *) +Definition isessentiallysmall_sigma@{u v k | u <= v, v < k} + `{Funext} (A : Type@{u}) (P : A -> Type@{v}) + (ies_A : IsEssentiallySmall@{u k} A) + (ies_P : forall x, IsEssentiallySmall@{v k} (P x)) + : IsEssentiallySmall@{v k} {x : A & P x}. +Proof. + eexists. + nrapply (equiv_functor_sigma'@{u v _ _ k k} ies_A.2). + nrapply (equiv_ind@{u v k} ies_A.2^-1%equiv). + 1: exact _. + intros x. + nrefine (equiv_path@{v k} _ _ _ oE _). + { apply ap. + symmetry. + apply eisretr. } + exact (ies_P ((ies_A.2)^-1%equiv x)).2. +Defined. + +(** Every small type is trivially essentially small *) +Definition isessentiallysmall_small@{u v} (A : Type@{u}) + : IsEssentiallySmall@{u v} A. +Proof. + exists A. + exact equiv_idmap. +Defined. + +(** The join of two essentially small types is essentially small. *) +Definition isessentiallysmall_join@{u1 u2 v k} (A : Type@{u1}) (B : Type@{u2}) + (ies_A : IsEssentiallySmall@{v k} A) (ies_B : IsEssentiallySmall@{v k} B) + : IsEssentiallySmall@{v k} (Join@{u1 u2 v} A B). +Proof. + exists (Join@{u1 u2 v} ies_A.1 ies_B.1). + apply equiv_functor_join. + - apply ies_A.2. + - apply ies_B.2. +Defined. + +(** And by induction, the iterated join of an essentially small type is essentially small. *) +Definition isessentiallysmall_iterated_join@{u v k} (A : Type@{u}) + (ies_A : IsEssentiallySmall@{v k} A) (n : nat) + : IsEssentiallySmall@{v k} (iterated_join A n). +Proof. + induction n. + 1: exact ies_A. + exact (isessentiallysmall_join A (iterated_join A n) ies_A IHn). +Defined. + +(** A sequential colimit of essentially small types is essentially small. *) +Definition isessentiallysmall_seq_colimit@{u v k} `{Funext} (s : Sequence@{v v v}) + (is : forall n, IsEssentiallySmall@{u k} (s n)) + : IsEssentiallySmall@{v k} (Colimit s). +Proof. + (** First we build a sequence in the universe [u] from a sequence [s] by replacing each type with a type in the universe [v] with the small version. *) + transparent assert (s' : Sequence@{u u u}). + { snrapply Build_Sequence. + - intros n. + exact (is n).1. + - hnf; intros n. + nrefine ((is n.+1%nat).2 o _ o (is n).2^-1%equiv). + apply arr; reflexivity. } + (** We also need a lifted version of [s'] since the record types involved are not cumulative. *) + transparent assert (s'' : Sequence@{v v v}). + { snrapply Build_Sequence. + - intros n. + exact (s' n). + - hnf; intros n. + apply (arr (G:=sequence_graph) s'). + reflexivity. } + exists (Colimit s'). + snrefine (equiv_functor_colimit (G:=sequence_graph) (D1 := s) (D2 := s'') _ _ _). + { snrapply Build_diagram_equiv. + { snrapply Build_DiagramMap. + - intros n. + exact (is n).2. + - intros n ? p; destruct p; intros x; simpl. + simpl. + f_ap; f_ap. + apply eissect. } + exact _. } + 1,2: exact _. +Defined. + +(** ** Fiber-wise Joins of Maps *) + +(** The fiber-wise join of two maps is the generalization of the join of two spaces, which can be thought of as the fiber-wise join of maps [A -> 1] and [B -> 1]. The fiber-wise join of two maps [f : A -> X] and [g : B -> X] is the pushout of the projections of the pullback of [f] and [g]. *) +Definition FiberwiseJoin@{a b x k} + {A : Type@{a}} {B : Type@{b}} (X : Type@{x}) (f : A -> X) (g : B -> X) + : Type@{k}. +Proof. + nrapply Pushout@{k k k k}. + - exact (pullback_pr1@{_ _ _ k} (f := f) (g := g)). + - exact (pullback_pr2@{_ _ _ k}(f := f) (g := g)). +Defined. + +(** We can iterate the fiber-wise join for a single map [f : A -> X] to get the fiber-wise join powers. We need to mutually recursively define a type and also a map out of that type. This isn't currently possible with Coq, so we package up both pieces of data in a sigma type and then later project out of it. *) +Record Fiberwise_join_power_data@{u v k} + {A : Type@{u}} {X : Type@{v}} (f : A -> X) : Type@{k} := { + fiberwise_join_power_data : Type@{v}; + fiberwise_join_power_data_map : fiberwise_join_power_data -> X; +}. + +Fixpoint fiberwise_join_power_and_map@{u v k | u <= v, v < k} + {A : Type@{u}} {X : Type@{v}} (f : A -> X) (n : nat) + : @Fiberwise_join_power_data@{u v k} A X f . +Proof. + destruct n. + - exists Empty. + apply Empty_rec. + - pose (map := (fiberwise_join_power_data_map _ (fiberwise_join_power_and_map A X f n))). + exists (FiberwiseJoin@{u v v v} X f map). + snrapply (Pushout_rec@{v v v v v} X f map). + intros [x [y p]]. + exact p. +Defined. + +Definition fiberwise_join_power@{u v k | u <= v, v < k} + {A : Type@{u}} {X : Type@{v}} (f : A -> X) (n : nat) + := fiberwise_join_power_data _ (fiberwise_join_power_and_map@{u v k} f n). + +Definition fiberwise_join_power_map@{u v k | u <= v, v < k} + {A : Type@{u}} {X : Type@{v}} (f : A -> X) (n : nat) + : fiberwise_join_power@{u v k} f n -> X + := fiberwise_join_power_data_map _ (fiberwise_join_power_and_map@{u v k} f n). + +(** Between successive powers there is an inclusion map. *) +Definition fiberwise_join_power_incl@{u v k | u <= v, v < k} + {A : Type@{u}} {X : Type@{v}} (f : A -> X) (n : nat) + : fiberwise_join_power f n -> fiberwise_join_power f n.+1. +Proof. + destruct n. + - apply Empty_rec. + - apply pushr. +Defined. + +(** This inclusion map commutes appropriately with the maps to [X]. *) +Lemma fiberwise_join_power_incl_comm@{u v k | u <= v, v < k} + {A : Type@{u}} {X : Type@{v}} (f : A -> X) (n : nat) + : fiberwise_join_power_map f n.+1 o fiberwise_join_power_incl f n + == fiberwise_join_power_map f n. +Proof. + destruct n. + 1: nrapply Empty_ind. + intros x. + reflexivity. +Defined. + +(** ** Infinite Fiber-wise Join Powers *) + +(** The sequence of fiber-wise join power consists of the nth fiber-wise join power and the inclusion map. *) +Definition seq_fiberwise_join_power@{u v k | u <= v, v < k} + {A : Type@{u}} {X : Type@{v}} (f : A -> X) + : Sequence@{v v v}. +Proof. + snrapply Build_Sequence. + - exact (fiberwise_join_power@{u v k} f). + - exact (fiberwise_join_power_incl@{u v k} f). +Defined. + +(** Infinite fiber-wise join powers are defined as the colimit of the sequence of fiber-wise join powers. *) +Definition infinite_fiberwise_join_power@{u v k | u <= v, v < k} + {A : Type@{u}} {X : Type@{v}} (f : A -> X) + := Colimit (seq_fiberwise_join_power@{u v k} f). + +Definition infinite_fiberwise_join_power_map@{u v k | u <= v, v < k} + {A : Type@{u}} {X : Type@{v}} (f : A -> X) + : infinite_fiberwise_join_power@{u v k} f -> X. +Proof. + snrapply Colimit_rec. + snrapply Cocone.Build_Cocone. + - exact (fiberwise_join_power_map@{u v k} f). + - simpl; intros n ? p; destruct p. + apply fiberwise_join_power_incl_comm. +Defined. + +(** Here is our main theorem, it says that for any map [f : A -> X] from a small type [A] into a locally small type [X], image is an essentially small type. *) +Theorem isessentiallysmall_infinite_fiberwise_join_power@{u v k | u <= v, v < k} + `{Funext} {A : Type@{u}} {X : Type@{v}} (f : A -> X) + (ils_X : IsLocallySmall@{v k} X) + : IsEssentiallySmall@{v k} (himage@{u v} f). +Proof. + apply isessentiallysmall_sigma. + 1: apply isessentiallysmall_small. + intros a. + unfold merely. + apply isessentiallysmall_seq_colimit. + simpl. + intros n. + unfold hfiber. + apply isessentiallysmall_iterated_join. + apply isessentiallysmall_sigma. + 1: apply isessentiallysmall_small. + intros x. + apply ils_X. +Defined. From 1a3413d6d3b2befba20af0b1767d8ae4dabec9cf Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 28 Sep 2024 13:23:14 +0100 Subject: [PATCH 2/3] more flexible universes for functoriality of join Signed-off-by: Ali Caglayan --- theories/Homotopy/Join/Core.v | 96 +++++++++++++++++++++++------------ 1 file changed, 64 insertions(+), 32 deletions(-) diff --git a/theories/Homotopy/Join/Core.v b/theories/Homotopy/Join/Core.v index c6c480aa472..5c5a94fcce6 100644 --- a/theories/Homotopy/Join/Core.v +++ b/theories/Homotopy/Join/Core.v @@ -109,8 +109,11 @@ Arguments JoinRecData : clear implicits. Arguments Build_JoinRecData {A B P}%_type_scope (jl jr jg)%_function_scope. (** We use the name [join_rec] for the version of [Join_rec] defined on this data. *) -Definition join_rec {A B P : Type} (f : JoinRecData A B P) - : Join A B $-> P +Definition join_rec + @{a b ab p abp big | a <= ab, b <= ab, ab <= abp, p <= abp, abp < big} + {A : Type@{a}} {B : Type@{b}} {P : Type@{p}} + (f : JoinRecData@{a b p} A B P) + : Hom (A:=Type@{abp}) (Join@{a b ab} A B) P := Join_rec (jl f) (jr f) (jg f). Definition join_rec_beta_jg {A B P : Type} (f : JoinRecData A B P) (a : A) (b : B) @@ -481,6 +484,9 @@ Proof. apply diamond_symm. Defined. +(* Unset Printing Notations. *) +Set Printing Universes. + (** * Functoriality of Join. *) Section FunctorJoin. @@ -489,18 +495,29 @@ Section FunctorJoin. : JoinRecData A B (Join C D) := {| jl := joinl o f; jr := joinr o g; jg := fun a b => jglue (f a) (g b); |}. - Definition functor_join {A B C D} (f : A -> C) (g : B -> D) - : Join A B -> Join C D - := join_rec (functor_join_recdata f g). + Definition functor_join + @{a b c d ab cd abcd big | a <= ab, b <= ab, c <= cd, d <= cd, ab <= abcd, + cd <= abcd, abcd < big} + {A : Type@{a}} {B : Type@{b}} {C : Type@{c}} {D : Type@{d}} + (f : A -> C) (g : B -> D) + : Join@{a b ab} A B -> Join@{c d cd} C D + := join_rec@{a b ab cd abcd big} (functor_join_recdata f g). Definition functor_join_beta_jglue {A B C D : Type} (f : A -> C) (g : B -> D) (a : A) (b : B) : ap (functor_join f g) (jglue a b) = jglue (f a) (g b) := join_rec_beta_jg _ a b. - Definition functor_join_compose {A B C D E F} - (f : A -> C) (g : B -> D) (h : C -> E) (i : D -> F) - : functor_join (h o f) (i o g) == functor_join h i o functor_join f g. + Definition functor_join_compose + @{a b c d e f ab cd ef abcd cdef abef abcdef s + | a <= ab, b <= ab, c <= cd, d <= cd, e <= ef, f <= ef, + ab <= abcd, cd <= abcd, cd <= cdef, ef <= cdef, ab <= abef, ef <= abef, + abcd < s, cdef < s, abef < s} + {A : Type@{a}} {B : Type@{b}} {C : Type@{c}} {D : Type@{d}} {E : Type@{e}} + {F : Type@{f}} (f : A -> C) (g : B -> D) (h : C -> E) (i : D -> F) + : functor_join@{a b e f ab ef abef s} (h o f) (i o g) + == functor_join@{c d e f cd ef cdef s} h i + o functor_join@{a b c d ab cd abcd s} f g. Proof. snrapply Join_ind_FlFr. 1,2: reflexivity. @@ -513,8 +530,9 @@ Section FunctorJoin. apply functor_join_beta_jglue. Defined. - Definition functor_join_idmap {A B} - : functor_join idmap idmap == (idmap : Join A B -> Join A B). + Definition functor_join_idmap@{a b ab s} {A : Type@{a}} {B : Type@{b}} + : functor_join@{a b a b ab ab ab s} idmap idmap + == (idmap : Join A B -> Join A B). Proof. snrapply Join_ind_FlFr. 1,2: reflexivity. @@ -525,9 +543,12 @@ Section FunctorJoin. symmetry; apply ap_idmap. Defined. - Definition functor2_join {A B C D} {f f' : A -> C} {g g' : B -> D} + Definition functor2_join@{a b c d ab cd abcd s} + {A : Type@{a}} {B : Type@{b}} {C : Type@{c}} {D : Type@{d}} + {f f' : A -> C} {g g' : B -> D} (h : f == f') (k : g == g') - : functor_join f g == functor_join f' g'. + : functor_join@{a b c d ab cd abcd s} f g + == functor_join@{a b c d ab cd abcd s} f' g'. Proof. srapply Join_ind_FlFr. - simpl; intros; apply ap, h. @@ -539,26 +560,37 @@ Section FunctorJoin. apply join_natsq. Defined. - Global Instance isequiv_functor_join {A B C D} - (f : A -> C) `{!IsEquiv f} (g : B -> D) `{!IsEquiv g} - : IsEquiv (functor_join f g). - Proof. - snrapply isequiv_adjointify. - - apply (functor_join f^-1 g^-1). - - etransitivity. - 1: symmetry; apply functor_join_compose. - etransitivity. - 1: exact (functor2_join (eisretr f) (eisretr g)). - apply functor_join_idmap. - - etransitivity. - 1: symmetry; apply functor_join_compose. - etransitivity. - 1: exact (functor2_join (eissect f) (eissect g)). - apply functor_join_idmap. - Defined. - - Definition equiv_functor_join {A B C D} (f : A <~> C) (g : B <~> D) - : Join A B <~> Join C D := Build_Equiv _ _ (functor_join f g) _. + Global Instance isequiv_functor_join + @{a b c d ab cd abcd s | a <= ab, b <= ab, c <= cd, d <= cd, ab <= abcd, + cd <= abcd, abcd < s} + {A : Type@{a}} {B : Type@{b}} {C : Type@{c}} {D : Type@{d}} + (f : A -> C) `{!IsEquiv@{a c} f} (g : B -> D) `{!IsEquiv@{b d} g} + : IsEquiv@{ab cd} (functor_join@{a b c d ab cd abcd s} f g). + Proof. + snrapply isequiv_adjointify@{ab cd}. + - exact (functor_join@{c d a b cd ab abcd s} + (equiv_inv@{a c} (f:=f)) (equiv_inv@{b d} (f:=g))). + - nrapply transitive_pointwise_paths@{s s s}. + 1: snrapply symmetric_pointwise_paths@{s s s}. + 1: snrapply functor_join_compose@{c d a b c d cd ab cd abcd abcd abcd abcd s}. + nrapply transitive_pointwise_paths@{s s s}. + 1: exact (functor2_join@{c d c d cd cd cd s} (eisretr@{a c} f) (eisretr@{b d} g)). + rapply functor_join_idmap@{c d cd s}. + - nrapply transitive_pointwise_paths@{s s s}. + 1: snrapply symmetric_pointwise_paths@{s s s}. + 1: rapply functor_join_compose@{a b c d a b ab cd ab abcd abcd abcd abcd s}. + nrapply transitive_pointwise_paths@{s s s}. + 1: exact (functor2_join@{a b a b ab ab ab s} (eissect@{a c} f) (eissect@{b d} g)). + apply functor_join_idmap@{a b ab s}. + Defined. + + Definition equiv_functor_join + @{a b c d ab cd abcd s | a <= ab, b <= ab, c <= cd, d <= cd, ab <= abcd, + cd <= abcd, abcd < s} + {A : Type@{a}} {B : Type@{b}} {C : Type@{c}} {D : Type@{d}} + (f : Equiv@{a c} A C) (g : Equiv@{b d} B D) + : Equiv@{ab cd} (Join@{a b ab} A B) (Join@{c d cd} C D) + := Build_Equiv@{ab cd} _ _ (functor_join@{a b c d ab cd abcd s} f g) _. Global Instance is0bifunctor_join : Is0Bifunctor Join. Proof. From a2ba1471b32887aae2aef11a9eece3c5ffee04c3 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 28 Sep 2024 20:04:53 +0100 Subject: [PATCH 3/3] wip adapting join construction to new smallness Signed-off-by: Ali Caglayan --- theories/Diagrams/Sequence.v | 21 ++++ theories/Homotopy/JoinConstruction.v | 155 +++++++++++++++------------ 2 files changed, 107 insertions(+), 69 deletions(-) diff --git a/theories/Diagrams/Sequence.v b/theories/Diagrams/Sequence.v index 27c3ce26dc9..a3de26e1bcc 100644 --- a/theories/Diagrams/Sequence.v +++ b/theories/Diagrams/Sequence.v @@ -17,6 +17,12 @@ Defined. Definition Sequence := Diagram sequence_graph. +Definition sequence_arr (X : Sequence) (n : nat) : X n -> X n.+1. +Proof. + snrapply arr. + exact idpath. +Defined. + Definition Build_Sequence (X : nat -> Type) (f : forall n, X n -> X n.+1) @@ -29,6 +35,21 @@ Proof. apply f. Defined. +Definition Build_SequenceMap + {X Y : Sequence} + (f : forall n, X n -> Y n) + (H : forall n, f n.+1 o (sequence_arr X n) == (sequence_arr Y n) o f n) + : DiagramMap X Y. +Proof. + snrapply Build_DiagramMap. + - exact f. + - intros i j; revert j. + snrapply paths_ind. + intros x. + symmetry. + apply H. +Defined. + (** A useful lemma to show than two sequences are equivalent. *) Definition equiv_sequence (D1 D2 : Sequence) diff --git a/theories/Homotopy/JoinConstruction.v b/theories/Homotopy/JoinConstruction.v index e7fa2d24292..c409d0c62ca 100644 --- a/theories/Homotopy/JoinConstruction.v +++ b/theories/Homotopy/JoinConstruction.v @@ -2,6 +2,9 @@ Require Import Basics Types. Require Import Limits.Pullback Colimits.Pushout Diagrams.Diagram Diagrams.Sequence Colimits.Colimit Colimits.Sequential. Require Import Join.Core. Require Import NullHomotopy. +Require Import Universes.Smallness. + +Local Set Printing Universes. (** * The Join Construction *) @@ -97,7 +100,7 @@ Definition himage@{i j} {A : Type@{i}} {B : Type@{j}} (f : A -> B) : Type@{j} := {y : B & merely@{j j} (hfiber f y)}. (** ** Essentially Small and Locally Small Types *) - +(* (** A type in a universe [v] is essentially small, with respect to a strictly smaller universe [u], if there is a type in the universe [u] that is equivalent to it. *) Definition IsEssentiallySmall@{u v | u < v} (A : Type@{v}) := {B : Type@{u} & A <~> B}. @@ -121,17 +124,17 @@ Proof. rewrite transport_const. rewrite transport_path_universe. apply ap, eissect. -Defined. +Defined. *) (** Therefore, so is being locally small. *) -Global Instance ishprop_islocallysmall@{u v} `{Univalence} (A : Type@{v}) - : IsHProp (IsEssentiallySmall@{u v} A) := _. +(* Global Instance ishprop_islocallysmall@{u v} `{Univalence} (A : Type@{v}) + : IsHProp (IsEssentiallySmall@{u v} A) := _. *) (** A sigma type is essentially small if both of its types are essentially small. *) -Definition isessentiallysmall_sigma@{u v k | u <= v, v < k} +(* Definition isessentiallysmall_sigma@{u v k | u <= v, v < k} `{Funext} (A : Type@{u}) (P : A -> Type@{v}) - (ies_A : IsEssentiallySmall@{u k} A) - (ies_P : forall x, IsEssentiallySmall@{v k} (P x)) + (ies_A : IsSmall@{u k} A) + (ies_P : forall x, Ismall@{v k} (P x)) : IsEssentiallySmall@{v k} {x : A & P x}. Proof. eexists. @@ -144,73 +147,100 @@ Proof. symmetry. apply eisretr. } exact (ies_P ((ies_A.2)^-1%equiv x)).2. -Defined. +Defined. *) (** Every small type is trivially essentially small *) -Definition isessentiallysmall_small@{u v} (A : Type@{u}) +(* Definition isessentiallysmall_small@{u v} (A : Type@{u}) : IsEssentiallySmall@{u v} A. Proof. exists A. exact equiv_idmap. -Defined. - -(** The join of two essentially small types is essentially small. *) -Definition isessentiallysmall_join@{u1 u2 v k} (A : Type@{u1}) (B : Type@{u2}) - (ies_A : IsEssentiallySmall@{v k} A) (ies_B : IsEssentiallySmall@{v k} B) - : IsEssentiallySmall@{v k} (Join@{u1 u2 v} A B). +Defined. *) + +(** The join of two small types is small. *) +Global Instance issmall_join@{u k l big | l < big, u <= l, k <= l} + (A : Type@{k}) (B : Type@{k}) + (sA : IsSmall@{u k} A) (sB : IsSmall@{u k} B) + : IsSmall@{u k} (Join@{k k k} A B) + := Build_IsSmall@{u k} + (Join@{k k k} A B) + (Join@{u u u} (smalltype@{u k} A) (smalltype@{u k} B)) + (equiv_functor_join@{u u k k u k l big} + (equiv_smalltype@{u k} A) + (equiv_smalltype@{u k} B)). + +(** And by induction, the iterated join of a small type is small. *) +Definition issmall_iterated_join@{v k vk big | v <= vk, k <= vk, vk < big} + (A : Type@{k}) (sA : IsSmall@{v k} A) (n : nat) + : IsSmall@{v k} (iterated_join@{k} A n). Proof. - exists (Join@{u1 u2 v} ies_A.1 ies_B.1). - apply equiv_functor_join. - - apply ies_A.2. - - apply ies_B.2. -Defined. - -(** And by induction, the iterated join of an essentially small type is essentially small. *) -Definition isessentiallysmall_iterated_join@{u v k} (A : Type@{u}) - (ies_A : IsEssentiallySmall@{v k} A) (n : nat) - : IsEssentiallySmall@{v k} (iterated_join A n). -Proof. - induction n. - 1: exact ies_A. - exact (isessentiallysmall_join A (iterated_join A n) ies_A IHn). + simple_induction' n. + - exact sA. + - by nrapply issmall_join@{v k vk big}. Defined. (** A sequential colimit of essentially small types is essentially small. *) -Definition isessentiallysmall_seq_colimit@{u v k} `{Funext} (s : Sequence@{v v v}) - (is : forall n, IsEssentiallySmall@{u k} (s n)) - : IsEssentiallySmall@{v k} (Colimit s). +Definition issmall_seq_colimit@{u k uk | u <= uk, k <= uk} `{Funext} (s : Sequence@{k k k}) + (ss : forall n, IsSmall@{u k} (s n)) + : IsSmall@{u k} (Colimit@{k k k k k k k} s). Proof. (** First we build a sequence in the universe [u] from a sequence [s] by replacing each type with a type in the universe [v] with the small version. *) - transparent assert (s' : Sequence@{u u u}). - { snrapply Build_Sequence. + snrefine (let s' : Sequence@{u u u} := _ in _). + { snrapply Build_Sequence@{u u u}. - intros n. - exact (is n).1. + exact (smalltype@{u k} (s n)). - hnf; intros n. - nrefine ((is n.+1%nat).2 o _ o (is n).2^-1%equiv). - apply arr; reflexivity. } + intros x. + refine (equiv_inv@{u k} + (f := @equiv_smalltype@{u k} _ (ss n.+1%nat)) _). + snrapply (sequence_arr s n). + exact (equiv_fun@{u k} (equiv_smalltype@{u k} _) x). } + exists (Colimit@{u u u u u u u} s'). + snrapply (equiv_functor_colimit (D1 := s) (D2 := s')). + - snrapply Build_diagram_equiv. + + snrapply Build_SequenceMap. + * intros n. + exact (equiv_smalltype@{u k} (s n))^-1. + * intros n f. + simpl. + f_ap; f_ap; symmetry. + apply eisretr. + + exact _. + - exact _. + - exact _. +Admitted. + +(* (** We also need a lifted version of [s'] since the record types involved are not cumulative. *) - transparent assert (s'' : Sequence@{v v v}). - { snrapply Build_Sequence. - - intros n. - exact (s' n). - - hnf; intros n. - apply (arr (G:=sequence_graph) s'). - reflexivity. } - exists (Colimit s'). - snrefine (equiv_functor_colimit (G:=sequence_graph) (D1 := s) (D2 := s'') _ _ _). + snrefine (let s'' : Sequence@{uk uk uk} := _ in _). + { snrapply Build_Sequence@{uk uk uk}. + - exact s'. + - snrapply (sequence_arr@{uk uk uk} s'). } + exists (Colimit@{u u u u u u u} s'). + About equiv_functor_colimit + @{u0 u1 u u u u u u7 u8 u9 + u10 u11 u12 u13 u14 u15 u16 u17 u18 u19 + u20 u21 u22 u23 u24 u25 u26 u27 u28 u29}. + snrefine (equiv_functor_colimit + @{u0 u1 u2 u3 u4 u5 u6 u7 u8 u9 + u10 u11 u12 u13 u14 u15 u16 u17 u18 u19 + u20 u21 u22 u23 u24 u25 u26 u27 u28 u29} + (G:=sequence_graph) (D1 := s'') (D2 := s') _ _ _). { snrapply Build_diagram_equiv. { snrapply Build_DiagramMap. - intros n. - exact (is n).2. + exact (equiv_smalltype@{u k} (s' n))^-1. - intros n ? p; destruct p; intros x; simpl. simpl. - f_ap; f_ap. - apply eissect. } + f_ap; f_ap. } exact _. } - 1,2: exact _. + (* 1: snrapply iscolimit_colimit. *) + 1: exact _. + 1: exact _. Defined. +*) -(** ** Fiber-wise Joins of Maps *) +(** ** Fiber-wise joins of maps *) (** The fiber-wise join of two maps is the generalization of the join of two spaces, which can be thought of as the fiber-wise join of maps [A -> 1] and [B -> 1]. The fiber-wise join of two maps [f : A -> X] and [g : B -> X] is the pushout of the projections of the pullback of [f] and [g]. *) Definition FiberwiseJoin@{a b x k} @@ -303,22 +333,9 @@ Proof. Defined. (** Here is our main theorem, it says that for any map [f : A -> X] from a small type [A] into a locally small type [X], image is an essentially small type. *) -Theorem isessentiallysmall_infinite_fiberwise_join_power@{u v k | u <= v, v < k} +Definition isessentiallysmall_infinite_fiberwise_join_power + @{u v k | u <= v, v < k} `{Funext} {A : Type@{u}} {X : Type@{v}} (f : A -> X) - (ils_X : IsLocallySmall@{v k} X) - : IsEssentiallySmall@{v k} (himage@{u v} f). -Proof. - apply isessentiallysmall_sigma. - 1: apply isessentiallysmall_small. - intros a. - unfold merely. - apply isessentiallysmall_seq_colimit. - simpl. - intros n. - unfold hfiber. - apply isessentiallysmall_iterated_join. - apply isessentiallysmall_sigma. - 1: apply isessentiallysmall_small. - intros x. - apply ils_X. -Defined. + (ils_X : IsLocallySmall@{u v k} 1 X) + : IsSmall@{v k} (himage@{u v} f) + := _.