From ddec6f77ee10e447a6f236d1aa93ed187ee2004e Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 12 Jul 2016 09:51:00 +0100 Subject: [PATCH] feat(category.pushout): finish second way of formulating universal property --- .../category/constructions/functor.hlean | 5 ++ .../category/constructions/pushout.hlean | 56 +++++++++++++++++-- hott/algebra/category/functor/basic.hlean | 2 +- hott/algebra/category/iso.hlean | 2 +- hott/types/sigma.hlean | 7 +++ 5 files changed, 66 insertions(+), 6 deletions(-) diff --git a/hott/algebra/category/constructions/functor.hlean b/hott/algebra/category/constructions/functor.hlean index 336032d94..a115924fa 100644 --- a/hott/algebra/category/constructions/functor.hlean +++ b/hott/algebra/category/constructions/functor.hlean @@ -169,6 +169,11 @@ namespace functor (λa, id) (λa, !natural_map_inv_of_eq ⬝ ap (λx, hom_of_eq x⁻¹) !ap010_assoc) + definition assoc_iso [constructor] (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) + : H ∘f (G ∘f F) ≅ (H ∘f G) ∘f F := + iso.MK (assoc_natural H G F) (assoc_natural_rev H G F) + (nat_trans_eq (λa, proof !id_id qed)) (nat_trans_eq (λa, proof !id_id qed)) + definition id_left_natural [constructor] (F : C ⇒ D) : functor.id ∘f F ⟹ F := change_natural_map (hom_of_eq !functor.id_left) diff --git a/hott/algebra/category/constructions/pushout.hlean b/hott/algebra/category/constructions/pushout.hlean index ba94a1fc2..7f7afc033 100644 --- a/hott/algebra/category/constructions/pushout.hlean +++ b/hott/algebra/category/constructions/pushout.hlean @@ -183,6 +183,17 @@ namespace category { intro e₁ e₂ e₃ g f, refine (eq_of_rel (tr (paths_rel_of_Q _)))⁻¹, apply EE} end + definition Cpushout_coh [constructor] : Cpushout_inl ∘f F ≅ Cpushout_inr ∘f G := + begin + fapply natural_iso.MK, + { intro c, exact class_of [DE (λ c, c) F G c]}, + { intro c c' f, refine eq_of_rel (tr (paths_rel_of_Q !cohDE))}, + { intro c, exact class_of [ED (λ c, c) F G c]}, + { intro c, refine eq_of_rel (tr (paths_rel_of_Q !DED))}, + { intro c, refine eq_of_rel (tr (paths_rel_of_Q !EDE))}, + end + +--(class_of [DE (λ c, c) F G s]) variables ⦃x x' x₁ x₂ x₃ : Cpushout⦄ include H K local notation `R` := bpushout_prehom_index (λ c, c) F G @@ -295,8 +306,8 @@ namespace category end definition Cpushout_functor_coh (c : C) : natural_map (to_hom Cpushout_functor_inr) (G c) ∘ - Cpushout_functor (class_of [DE (λ c, c) F G c]) ∘ natural_map (to_inv Cpushout_functor_inl) (F c) - = natural_map (to_hom η) c := + Cpushout_functor (natural_map (to_hom Cpushout_coh) c) ∘ + natural_map (to_inv Cpushout_functor_inl) (F c) = natural_map (to_hom η) c := !id_leftright ⬝ !Cpushout_functor_list_singleton definition Cpushout_functor_unique_ob [unfold 13] (L : Cpushout ⇒ X) (η₁ : L ∘f Cpushout_inl ≅ H) @@ -318,7 +329,8 @@ namespace category definition Cpushout_functor_unique_nat_singleton (L : Cpushout ⇒ X) (η₁ : L ∘f Cpushout_inl ≅ H) (η₂ : L ∘f Cpushout_inr ≅ K) - (p : Πs, natural_map (to_hom η₂) (to_fun_ob G s) ∘ to_fun_hom L (class_of [DE (λ c, c) F G s]) ∘ + (p : Πs, natural_map (to_hom η₂) (to_fun_ob G s) ∘ + to_fun_hom L (natural_map (to_hom Cpushout_coh) s) ∘ natural_map (to_inv η₁) (to_fun_ob F s) = natural_map (to_hom η) s) (r : R x x') : Cpushout_functor_reduction_rule r ∘ Cpushout_functor_unique_ob L η₁ η₂ x = Cpushout_functor_unique_ob L η₁ η₂ x' ∘ L (class_of [r]) := @@ -341,7 +353,8 @@ namespace category definition Cpushout_functor_unique [constructor] (L : Cpushout ⇒ X) (η₁ : L ∘f Cpushout_inl ≅ H) (η₂ : L ∘f Cpushout_inr ≅ K) - (p : Πs, natural_map (to_hom η₂) (to_fun_ob G s) ∘ to_fun_hom L (class_of [DE (λ c, c) F G s]) ∘ + (p : Πs, natural_map (to_hom η₂) (to_fun_ob G s) ∘ + to_fun_hom L (natural_map (to_hom Cpushout_coh) s) ∘ natural_map (to_inv η₁) (to_fun_ob F s) = natural_map (to_hom η) s) : L ≅ Cpushout_functor := begin @@ -391,6 +404,41 @@ namespace category apply is_prop.elimo end + local attribute prod.eq_pr1 prod.eq_pr2 [reducible] + definition Cpushout_equiv {C D E : Precategory} {X : Category} (F : C ⇒ D) (G : C ⇒ E) : + (Cpushout F G ⇒ X) ≃ Σ(H : (D ⇒ X) × (E ⇒ X)), H.1 ∘f F ≅ H.2 ∘f G := + begin + fapply equiv.MK, + { intro K, refine ⟨(K ∘f Cpushout_inl F G, K ∘f Cpushout_inr F G), _⟩, + exact !assoc_iso⁻¹ⁱ ⬝i (K ∘fi Cpushout_coh F G) ⬝i !assoc_iso}, + { intro v, cases v with w η, cases w with K L, exact Cpushout_functor η}, + { exact abstract begin intro v, cases v with w η, cases w with K L, esimp at *, + fapply sigma_eq, + { fapply prod_eq: esimp; apply eq_of_iso, + { exact Cpushout_functor_inl η}, + { exact Cpushout_functor_inr η}}, + esimp, apply iso_pathover, apply hom_pathover, + rewrite [ap_compose' _ pr₁, ap_compose' _ pr₂, prod_eq_pr1, prod_eq_pr2], + rewrite [-+respect_hom_of_eq (precomposition_functor _ _), +hom_of_eq_eq_of_iso], + apply nat_trans_eq, intro c, esimp [category.to_precategory], + rewrite [+id_left, +id_right, Cpushout_functor_list_singleton] end end}, + { exact abstract begin intro K, esimp, + refine eq_base_of_is_prop_sigma _ !is_trunc_succ _ _, rotate 1, + { refine Cpushout_universal F G (K ∘f Cpushout_inl F G) (K ∘f Cpushout_inr F G) _, + exact !assoc_iso⁻¹ⁱ ⬝i (K ∘fi Cpushout_coh F G) ⬝i !assoc_iso}, + { esimp, fconstructor, esimp, split, + { fapply natural_iso.mk', + { intro c, reflexivity}, + { intro c c' f, rewrite [▸*, id_right, Cpushout_functor_list_singleton, id_left]}}, + { fapply natural_iso.mk', + { intro c, reflexivity}, + { intro c c' f, rewrite [▸*, id_right, Cpushout_functor_list_singleton, id_left]}}, + intro c, rewrite [▸*, id_left, id_right, Cpushout_functor_list_singleton]}, + { esimp, fconstructor, + { split: reflexivity}, + intro c, reflexivity} end end} + end + /- Pushout of groupoids with a type of basepoints -/ section variables {S : Type} {C D E : Groupoid} (k : S → C) (F : C ⇒ D) (G : C ⇒ E) diff --git a/hott/algebra/category/functor/basic.hlean b/hott/algebra/category/functor/basic.hlean index 129972287..457b26020 100644 --- a/hott/algebra/category/functor/basic.hlean +++ b/hott/algebra/category/functor/basic.hlean @@ -273,7 +273,7 @@ namespace functor ap010_assoc K (H ∘f G) F a], end - definition hom_pathover_functor_left_functor_right {c₁ c₂ : C} {p : c₁ = c₂} (F G : C ⇒ D) + definition hom_pathover_functor {c₁ c₂ : C} {p : c₁ = c₂} (F G : C ⇒ D) {f₁ : F c₁ ⟶ G c₁} {f₂ : F c₂ ⟶ G c₂} (q : to_fun_hom G (hom_of_eq p) ∘ f₁ = f₂ ∘ to_fun_hom F (hom_of_eq p)) : f₁ =[p] f₂ := hom_pathover (hom_whisker_right _ (respect_hom_of_eq G _)⁻¹ ⬝ q ⬝ diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean index c81e2cad6..da2ac7408 100644 --- a/hott/algebra/category/iso.hlean +++ b/hott/algebra/category/iso.hlean @@ -164,7 +164,7 @@ namespace iso mk (to_hom H2 ∘ to_hom H1) _ infixl ` ⬝i `:75 := iso.trans - postfix [parsing_only] `⁻¹ⁱ`:(max + 1) := iso.symm + postfix `⁻¹ⁱ`:(max + 1) := iso.symm definition change_hom [constructor] (H : a ≅ b) (f : a ⟶ b) (p : to_hom H = f) : a ≅ b := iso.MK f (to_inv H) (p ▸ to_left_inverse H) (p ▸ to_right_inverse H) diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index 3d87a67b9..c8cac8253 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -502,6 +502,13 @@ namespace sigma [HA : is_trunc (n.+1) A] : is_trunc (n.+1) (Σa, B a) := @(is_trunc_sigma B (n.+1)) _ (λa, !is_trunc_succ_of_is_prop) + /- if the total space is a mere proposition, you can equate two points in the base type by + finding points in their fibers -/ + definition eq_base_of_is_prop_sigma {A : Type} (B : A → Type) (H : is_prop (Σa, B a)) {a a' : A} + (b : B a) (b' : B a') : a = a' := + (is_prop.elim ⟨a, b⟩ ⟨a', b'⟩)..1 + + end sigma attribute sigma.is_trunc_sigma [instance] [priority 1490]