From 219f7ae11a0b43147398a9243f8fb4174d54c810 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 27 Feb 2015 00:45:21 -0500 Subject: [PATCH] feat(hott/algebra/precategory): general cleanup in precategories, define uncurrying functor --- hott/algebra/category/constructions.hlean | 3 +- hott/algebra/groupoid.hlean | 2 +- hott/algebra/precategory/basic.hlean | 87 +++++++++-- hott/algebra/precategory/constructions.hlean | 18 +-- hott/algebra/precategory/functor.hlean | 35 ++--- hott/algebra/precategory/morphism.hlean | 16 +- hott/algebra/precategory/nat_trans.hlean | 16 +- hott/algebra/precategory/yoneda.hlean | 151 ++++++++++++++++--- hott/equiv_precomp.hlean | 87 ----------- hott/init/axioms/funext_of_ua.hlean | 8 +- hott/truncation.hlean | 23 --- hott/types/pointed.hlean | 10 +- 12 files changed, 247 insertions(+), 209 deletions(-) delete mode 100644 hott/equiv_precomp.hlean delete mode 100644 hott/truncation.hlean diff --git a/hott/algebra/category/constructions.hlean b/hott/algebra/category/constructions.hlean index e3f36d8fc..7d5060fc2 100644 --- a/hott/algebra/category/constructions.hlean +++ b/hott/algebra/category/constructions.hlean @@ -22,8 +22,7 @@ namespace category definition Category_hset [reducible] : Category := Category.mk hset category_hset - --RENAME AND CLEANUP - definition set_category_equiv_iso (a b : Category_hset) : (a ≅ b) = (a ≃ b) := sorry + definition isomorphic_hset_eq_equiv (a b : Category_hset) : (a ≅ b) = (a ≃ b) := sorry end hset namespace ops diff --git a/hott/algebra/groupoid.hlean b/hott/algebra/groupoid.hlean index dc9eebc91..be9d025f7 100644 --- a/hott/algebra/groupoid.hlean +++ b/hott/algebra/groupoid.hlean @@ -25,7 +25,7 @@ namespace category precategory.rec_on C groupoid.mk H definition groupoid_of_1_type.{l} (A : Type.{l}) - [H : is_trunc (succ zero) A] : groupoid.{l l} A := + [H : is_trunc 1 A] : groupoid.{l l} A := groupoid.mk (λ (a b : A), a = b) (λ (a b : A), have ish : is_hset (a = b), from is_trunc_eq nat.zero a b, ish) diff --git a/hott/algebra/precategory/basic.hlean b/hott/algebra/precategory/basic.hlean index 051ad9a8d..41f86243c 100644 --- a/hott/algebra/precategory/basic.hlean +++ b/hott/algebra/precategory/basic.hlean @@ -27,7 +27,7 @@ namespace category -- input ⟶ using \--> (this is a different arrow than \-> (→)) infixl [parsing-only] `⟶`:25 := precategory.hom namespace hom - infixl `⟶` := precategory.hom -- if you open this namespace, hom a b is printed as a ⟶ b + infixl `⟶`:25 := precategory.hom -- if you open this namespace, hom a b is printed as a ⟶ b end hom abbreviation hom := @precategory.hom @@ -39,28 +39,83 @@ namespace category abbreviation id_right := @precategory.id_right section basic_lemmas - variables {ob : Type} [C : precategory ob] - variables {a b c d : ob} {h : c ⟶ d} {g : hom b c} {f f' : hom a b} {i : a ⟶ a} - include C + variables {ob : Type} [C : precategory ob] + variables {a b c d : ob} {h : c ⟶ d} {g : hom b c} {f f' : hom a b} {i : a ⟶ a} + include C - definition id [reducible] := ID a + definition id [reducible] := ID a - definition id_compose (a : ob) : ID a ∘ ID a = ID a := !id_left + definition id_compose (a : ob) : ID a ∘ ID a = ID a := !id_left - definition left_id_unique (H : Π{b} {f : hom b a}, i ∘ f = f) : i = id := - calc i = i ∘ id : id_right - ... = id : H + definition left_id_unique (H : Π{b} {f : hom b a}, i ∘ f = f) : i = id := + calc i = i ∘ id : id_right + ... = id : H - definition right_id_unique (H : Π{b} {f : hom a b}, f ∘ i = f) : i = id := - calc i = id ∘ i : id_left - ... = id : H + definition right_id_unique (H : Π{b} {f : hom a b}, f ∘ i = f) : i = id := + calc i = id ∘ i : id_left + ... = id : H + + definition homset [reducible] (x y : ob) : hset := + hset.mk (hom x y) _ + + definition is_hprop_eq_hom [instance] : is_hprop (f = f') := + !is_trunc_eq - definition homset [reducible] (x y : ob) : hset := - hset.mk (hom x y) _ - definition is_hprop_eq_hom [instance] : is_hprop (f = f') := - !is_trunc_eq end basic_lemmas + context squares + parameters {ob : Type} [C : precategory ob] + local infixl `⟶`:25 := @precategory.hom ob C + local infixr `∘` := @precategory.comp ob C _ _ _ + definition compose_squares {xa xb xc ya yb yc : ob} + {xg : xb ⟶ xc} {xf : xa ⟶ xb} {yg : yb ⟶ yc} {yf : ya ⟶ yb} + {wa : xa ⟶ ya} {wb : xb ⟶ yb} {wc : xc ⟶ yc} + (xyab : wb ∘ xf = yf ∘ wa) (xybc : wc ∘ xg = yg ∘ wb) + : wc ∘ (xg ∘ xf) = (yg ∘ yf) ∘ wa := + calc + wc ∘ (xg ∘ xf) = (wc ∘ xg) ∘ xf : assoc + ... = (yg ∘ wb) ∘ xf : xybc + ... = yg ∘ (wb ∘ xf) : assoc + ... = yg ∘ (yf ∘ wa) : xyab + ... = (yg ∘ yf) ∘ wa : assoc + + set_option unifier.max_steps 30000 + definition compose_squares_2x2 {xa xb xc ya yb yc za zb zc : ob} + {xg : xb ⟶ xc} {xf : xa ⟶ xb} {yg : yb ⟶ yc} {yf : ya ⟶ yb} {zg : zb ⟶ zc} {zf : za ⟶ zb} + {va : ya ⟶ za} {vb : yb ⟶ zb} {vc : yc ⟶ zc} {wa : xa ⟶ ya} {wb : xb ⟶ yb} {wc : xc ⟶ yc} + (xyab : wb ∘ xf = yf ∘ wa) (xybc : wc ∘ xg = yg ∘ wb) + (yzab : vb ∘ yf = zf ∘ va) (yzbc : vc ∘ yg = zg ∘ vb) + : (vc ∘ wc) ∘ (xg ∘ xf) = (zg ∘ zf) ∘ (va ∘ wa) := + calc + (vc ∘ wc) ∘ (xg ∘ xf) = vc ∘ (wc ∘ (xg ∘ xf)) : (assoc vc wc (xg ∘ xf))⁻¹ᵖ + ... = vc ∘ ((yg ∘ yf) ∘ wa) : {compose_squares xyab xybc} + ... = (vc ∘ (yg ∘ yf)) ∘ wa : assoc vc (yg ∘ yf) wa + ... = ((zg ∘ zf) ∘ va) ∘ wa : {compose_squares yzab yzbc} + ... = (zg ∘ zf) ∘ (va ∘ wa) : (assoc (zg ∘ zf) va wa)⁻¹ᵖ + set_option unifier.max_steps 20000 + + definition square_precompose {xa xb xc yb yc : ob} + {xg : xb ⟶ xc} {yg : yb ⟶ yc} {wb : xb ⟶ yb} {wc : xc ⟶ yc} + (H : wc ∘ xg = yg ∘ wb) (xf : xa ⟶ xb) : wc ∘ xg ∘ xf = yg ∘ wb ∘ xf := + calc + wc ∘ xg ∘ xf = (wc ∘ xg) ∘ xf : assoc + ... = (yg ∘ wb) ∘ xf : H + ... = yg ∘ wb ∘ xf : assoc + + definition square_postcompose {xb xc yb yc yd : ob} + {xg : xb ⟶ xc} {yg : yb ⟶ yc} {wb : xb ⟶ yb} {wc : xc ⟶ yc} + (H : wc ∘ xg = yg ∘ wb) (yh : yc ⟶ yd) : (yh ∘ wc) ∘ xg = (yh ∘ yg) ∘ wb := + calc + (yh ∘ wc) ∘ xg = yh ∘ wc ∘ xg : assoc + ... = yh ∘ yg ∘ wb : H + ... = (yh ∘ yg) ∘ wb : assoc + + definition square_prepostcompose {xa xb xc yb yc yd : ob} + {xg : xb ⟶ xc} {yg : yb ⟶ yc} {wb : xb ⟶ yb} {wc : xc ⟶ yc} + (H : wc ∘ xg = yg ∘ wb) (yh : yc ⟶ yd) (xf : xa ⟶ xb) + : (yh ∘ wc) ∘ (xg ∘ xf) = (yh ∘ yg) ∘ (wb ∘ xf) := + square_precompose (square_postcompose H yh) xf + end squares structure Precategory : Type := (carrier : Type) diff --git a/hott/algebra/precategory/constructions.hlean b/hott/algebra/precategory/constructions.hlean index 30392d97c..c54a9e8f0 100644 --- a/hott/algebra/precategory/constructions.hlean +++ b/hott/algebra/precategory/constructions.hlean @@ -95,7 +95,7 @@ namespace category : precategory (obC × obD) := precategory.mk (λ a b, hom (pr1 a) (pr1 b) × hom (pr2 a) (pr2 b)) (λ a b, !is_trunc_prod) - (λ a b c g f, (pr1 g ∘ pr1 f , pr2 g ∘ pr2 f) ) + (λ a b c g f, (pr1 g ∘ pr1 f , pr2 g ∘ pr2 f)) (λ a, (id, id)) (λ a b c d h g f, pair_eq !assoc !assoc ) (λ a b f, prod_eq !id_left !id_left ) @@ -153,21 +153,21 @@ namespace category section precategory_functor open morphism functor nat_trans - definition precategory_functor [instance] [reducible] (C D : Precategory) + definition precategory_functor [instance] [reducible] (D C : Precategory) : precategory (functor C D) := precategory.mk (λa b, nat_trans a b) - (λ a b, @nat_trans.to_hset C D a b) + (λ a b, @is_hset_nat_trans C D a b) (λ a b c g f, nat_trans.compose g f) (λ a, nat_trans.id) (λ a b c d h g f, !nat_trans.assoc) (λ a b f, !nat_trans.id_left) (λ a b f, !nat_trans.id_right) - definition Precategory_functor [reducible] (C D : Precategory) : Precategory := - precategory.Mk (precategory_functor C D) + definition Precategory_functor [reducible] (D C : Precategory) : Precategory := + precategory.Mk (precategory_functor D C) - definition Precategory_functor_rev [reducible] (C D : Precategory) : Precategory := - Precategory_functor D C + -- definition Precategory_functor_rev [reducible] (C D : Precategory) : Precategory := + -- Precategory_functor D C /- we prove that if a natural transformation is pointwise an iso, then it is an iso -/ variables {C D : Precategory} {F G : C ⇒ D} (η : F ⟹ G) [iso : Π(a : C), is_iso (η a)] @@ -199,13 +199,13 @@ namespace category apply is_hset.elim end - definition nat_trans_is_iso.mk : is_iso η := + definition nat_trans_iso.mk : is_iso η := is_iso.mk (nat_trans_left_inverse η) (nat_trans_right_inverse η) end precategory_functor namespace ops - infixr `^c`:35 := Precategory_functor_rev + infixr `^c`:35 := Precategory_functor infixr `×f`:30 := product.prod_functor infixr `ᵒᵖᶠ`:(max+1) := opposite.opposite_functor end ops diff --git a/hott/algebra/precategory/functor.hlean b/hott/algebra/precategory/functor.hlean index 007bdda2b..2c4e42931 100644 --- a/hott/algebra/precategory/functor.hlean +++ b/hott/algebra/precategory/functor.hlean @@ -28,7 +28,7 @@ namespace functor -- The following lemmas will later be used to prove that the type of -- precategories forms a precategory itself - protected definition compose (G : functor D E) (F : functor C D) : functor C E := + protected definition compose [reducible] (G : functor D E) (F : functor C D) : functor C E := functor.mk (λ x, G (F x)) (λ a b f, G (F f)) @@ -41,6 +41,11 @@ namespace functor infixr `∘f`:60 := compose + protected definition id [reducible] {C : Precategory} : functor C C := + mk (λa, a) (λ a b f, f) (λ a, idp) (λ a b c f g, idp) + + protected definition ID [reducible] (C : Precategory) : functor C C := id + definition functor_eq_mk'' {F₁ F₂ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)} {H₂ : Π(a b : C), hom a b → hom (F₂ a) (F₂ b)} (id₁ id₂ comp₁ comp₂) (pF : F₁ = F₂) (pH : pF ▹ H₁ = H₂) @@ -71,39 +76,17 @@ namespace functor (pH : Π(a b : C) (f : hom a b), H₁ a b f = H₂ a b f) : functor.mk F H₁ id₁ comp₁ = functor.mk F H₂ id₂ comp₂ := functor_eq_mk'' id₁ id₂ comp₁ comp₂ idp - (eq_of_homotopy (λc, eq_of_homotopy (λc', eq_of_homotopy (λf, pH c c' f)))) + (eq_of_homotopy (λc, eq_of_homotopy (λc', eq_of_homotopy (pH c c')))) definition functor_eq_mk {F₁ F₂ : C ⇒ D} : Π(p : obF F₁ ∼ obF F₂), (Π(a b : C) (f : hom a b), transport (λF, hom (F a) (F b)) (eq_of_homotopy p) (F₁ f) = F₂ f) → F₁ = F₂ := - functor.rec_on F₁ (λO₁ H₁ id₁ comp₁, functor.rec_on F₂ (λO₂ H₂ id₂ comp₂ p q, !functor_eq_mk' q)) - - -- protected definition congr - -- {C : Precategory} {D : Precategory} - -- (F : C → D) - -- (foo2 : Π ⦃a b : C⦄, hom a b → hom (F a) (F b)) - -- (foo3a foo3b : Π (a : C), foo2 (ID a) = ID (F a)) - -- (foo4a foo4b : Π {a b c : C} (g : @hom C C b c) (f : @hom C C a b), - -- foo2 (g ∘ f) = foo2 g ∘ foo2 f) - -- (p3 : foo3a = foo3b) (p4 : @foo4a = @foo4b) - -- : functor.mk F foo2 foo3a @foo4a = functor.mk F foo2 foo3b @foo4b - -- := - -- begin - -- apply (eq.rec_on p3), intros, - -- apply (eq.rec_on p4), intros, - -- apply idp, - -- end - + functor.rec_on F₁ (λO₁ H₁ id₁ comp₁, functor.rec_on F₂ (λO₂ H₂ id₂ comp₂ p, !functor_eq_mk')) protected definition assoc {A B C D : Precategory} (H : functor C D) (G : functor B C) (F : functor A B) : H ∘f (G ∘f F) = (H ∘f G) ∘f F := !functor_eq_mk_constant (λa b f, idp) - protected definition id {C : Precategory} : functor C C := - mk (λa, a) (λ a b f, f) (λ a, idp) (λ a b c f g, idp) - - protected definition ID (C : Precategory) : functor C C := id - protected definition id_left (F : functor C D) : id ∘f F = F := functor.rec_on F (λF1 F2 F3 F4, !functor_eq_mk_constant (λa b f, idp)) @@ -173,7 +156,7 @@ namespace category namespace ops - abbreviation PreCat := Precat_of_strict_cats + abbreviation SPreCat := Precat_of_strict_cats --attribute precat_of_strict_precats [instance] end ops diff --git a/hott/algebra/precategory/morphism.hlean b/hott/algebra/precategory/morphism.hlean index 49802096c..4733d48ba 100644 --- a/hott/algebra/precategory/morphism.hlean +++ b/hott/algebra/precategory/morphism.hlean @@ -63,17 +63,17 @@ namespace morphism (Hl : g ∘ f = id) (Hr : f ∘ g' = id) : g = g' := by rewrite [-(id_right g), -Hr, assoc, Hl, id_left] - theorem retraction_eq_intro [H : is_section f] (H2 : f ∘ h = id) : retraction_of f = h - := left_inverse_eq_right_inverse !retraction_compose H2 + theorem retraction_eq_intro [H : is_section f] (H2 : f ∘ h = id) : retraction_of f = h := + left_inverse_eq_right_inverse !retraction_compose H2 - theorem section_eq_intro [H : is_retraction f] (H2 : h ∘ f = id) : section_of f = h - := (left_inverse_eq_right_inverse H2 !compose_section)⁻¹ + theorem section_eq_intro [H : is_retraction f] (H2 : h ∘ f = id) : section_of f = h := + (left_inverse_eq_right_inverse H2 !compose_section)⁻¹ - theorem inverse_eq_intro_right [H : is_iso f] (H2 : f ∘ h = id) : f⁻¹ = h - := left_inverse_eq_right_inverse !inverse_compose H2 + theorem inverse_eq_intro_right [H : is_iso f] (H2 : f ∘ h = id) : f⁻¹ = h := + left_inverse_eq_right_inverse !inverse_compose H2 - theorem inverse_eq_intro_left [H : is_iso f] (H2 : h ∘ f = id) : f⁻¹ = h - := (left_inverse_eq_right_inverse H2 !compose_inverse)⁻¹ + theorem inverse_eq_intro_left [H : is_iso f] (H2 : h ∘ f = id) : f⁻¹ = h := + (left_inverse_eq_right_inverse H2 !compose_inverse)⁻¹ theorem section_of_eq_retraction_of (f : a ⟶ b) [Hl : is_section f] [Hr : is_retraction f] : retraction_of f = section_of f := diff --git a/hott/algebra/precategory/nat_trans.hlean b/hott/algebra/precategory/nat_trans.hlean index 500d552a8..863e709c6 100644 --- a/hott/algebra/precategory/nat_trans.hlean +++ b/hott/algebra/precategory/nat_trans.hlean @@ -20,7 +20,7 @@ namespace nat_trans attribute natural_map [coercion] - protected definition compose (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H := + protected definition compose [reducible] (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H := nat_trans.mk (λ a, η a ∘ θ a) (λ a b f, @@ -33,6 +33,12 @@ namespace nat_trans infixr `∘n`:60 := compose + protected definition id [reducible] {C D : Precategory} {F : functor C D} : nat_trans F F := + mk (λa, id) (λa b f, !id_right ⬝ !id_left⁻¹) + + protected definition ID [reducible] {C D : Precategory} (F : functor C D) : nat_trans F F := + id + local attribute is_hprop_eq_hom [instance] definition nat_trans_eq_mk' {η₁ η₂ : Π (a : C), hom (F a) (G a)} (nat₁ : Π (a b : C) (f : hom a b), G f ∘ η₁ a = η₁ b ∘ F f) @@ -48,12 +54,6 @@ namespace nat_trans η₃ ∘n (η₂ ∘n η₁) = (η₃ ∘n η₂) ∘n η₁ := nat_trans_eq_mk (λa, !assoc) - protected definition id {C D : Precategory} {F : functor C D} : nat_trans F F := - mk (λa, id) (λa b f, !id_right ⬝ !id_left⁻¹) - - protected definition ID {C D : Precategory} (F : functor C D) : nat_trans F F := - id - protected definition id_left (η : F ⟹ G) : id ∘n η = η := nat_trans_eq_mk (λa, !id_left) @@ -79,7 +79,7 @@ namespace nat_trans end set_option apply.class_instance false - protected definition to_hset : is_hset (F ⟹ G) := + definition is_hset_nat_trans : is_hset (F ⟹ G) := begin apply is_trunc_is_equiv_closed, apply (equiv.to_is_equiv !sigma_char), apply is_trunc_sigma, diff --git a/hott/algebra/precategory/yoneda.hlean b/hott/algebra/precategory/yoneda.hlean index 200025792..24fd66c6f 100644 --- a/hott/algebra/precategory/yoneda.hlean +++ b/hott/algebra/precategory/yoneda.hlean @@ -42,9 +42,8 @@ open is_equiv equiv namespace functor open prod nat_trans - variables {C D E : Precategory} - - definition functor_curry_ob (F : C ×c D ⇒ E) (c : C) : E ^c D := + variables {C D E : Precategory} (F : C ×c D ⇒ E) (G : C ⇒ E ^c D) + definition functor_curry_ob [reducible] (c : C) : E ^c D := functor.mk (λd, F (c,d)) (λd d' g, F (id, g)) (λd, !respect_id) @@ -52,9 +51,9 @@ namespace functor F (id, g' ∘ g) = F (id ∘ id, g' ∘ g) : {(id_compose c)⁻¹} ... = F ((id,g') ∘ (id, g)) : idp ... = F (id,g') ∘ F (id, g) : respect_comp F qed) - local abbreviation Fob := @functor_curry_ob - definition functor_curry_mor (F : C ×c D ⇒ E) ⦃c c' : C⦄ (f : c ⟶ c') : Fob F c ⟹ Fob F c' := + + definition functor_curry_hom ⦃c c' : C⦄ (f : c ⟶ c') : Fob F c ⟹ Fob F c' := nat_trans.mk (λd, F (f, id)) (λd d' g, proof calc F (id, g) ∘ F (f, id) = F (id ∘ f, g ∘ id) : respect_comp F @@ -64,36 +63,146 @@ namespace functor ... = F (f ∘ id, id ∘ g) : {(id_left g)⁻¹} ... = F (f, id) ∘ F (id, g) : (respect_comp F (f, id) (id, g))⁻¹ᵖ qed) + local abbreviation Fhom := @functor_curry_hom - local abbreviation Fmor := @functor_curry_mor - definition functor_curry_mor_def (F : C ×c D ⇒ E) ⦃c c' : C⦄ (f : c ⟶ c') (d : D) : - (Fmor F f) d = F (f, id) := idp + definition functor_curry_hom_def ⦃c c' : C⦄ (f : c ⟶ c') (d : D) : + (Fhom F f) d = homF F (f, id) := idp - definition functor_curry_id (F : C ×c D ⇒ E) (c : C) : Fmor F (ID c) = nat_trans.id := + definition functor_curry_id (c : C) : Fhom F (ID c) = nat_trans.id := nat_trans_eq_mk (λd, respect_id F _) - definition functor_curry_comp (F : C ×c D ⇒ E) ⦃c c' c'' : C⦄ (f' : c' ⟶ c'') (f : c ⟶ c') - : Fmor F (f' ∘ f) = Fmor F f' ∘n Fmor F f := + definition functor_curry_comp ⦃c c' c'' : C⦄ (f' : c' ⟶ c'') (f : c ⟶ c') + : Fhom F (f' ∘ f) = Fhom F f' ∘n Fhom F f := nat_trans_eq_mk (λd, calc - natural_map (Fmor F (f' ∘ f)) d = F (f' ∘ f, id) : functor_curry_mor_def - ... = F (f' ∘ f, id ∘ id) : {(id_compose d)⁻¹} - ... = F ((f',id) ∘ (f, id)) : idp - ... = F (f',id) ∘ F (f, id) : respect_comp F - ... = natural_map ((Fmor F f') ∘ (Fmor F f)) d : idp) + natural_map (Fhom F (f' ∘ f)) d = F (f' ∘ f, id) : functor_curry_hom_def + ... = F (f' ∘ f, id ∘ id) : {(id_compose d)⁻¹} + ... = F ((f',id) ∘ (f, id)) : idp + ... = F (f',id) ∘ F (f, id) : respect_comp F + ... = natural_map ((Fhom F f') ∘ (Fhom F f)) d : idp) ---respect_comp F (g, id) (f, id) - definition functor_curry (F : C ×c D ⇒ E) : C ⇒ E ^c D := + definition functor_curry [reducible] : C ⇒ E ^c D := functor.mk (functor_curry_ob F) - (functor_curry_mor F) + (functor_curry_hom F) (functor_curry_id F) (functor_curry_comp F) + definition functor_uncurry_ob [reducible] (p : C ×c D) : E := + obF (G p.1) p.2 + local abbreviation Gob := @functor_uncurry_ob - definition is_equiv_functor_curry : is_equiv (@functor_curry C D E) := sorry + definition functor_uncurry_hom ⦃p p' : C ×c D⦄ (f : hom p p') : Gob G p ⟶ Gob G p' := + homF (obF G p'.1) f.2 ∘ natural_map (homF G f.1) p.2 + local abbreviation Ghom := @functor_uncurry_hom + + definition functor_uncurry_id (p : C ×c D) : Ghom G (ID p) = id := + calc + Ghom G (ID p) = homF (obF G p.1) id ∘ natural_map (homF G id) p.2 : idp + ... = id ∘ natural_map (homF G id) p.2 : ap (λx, x ∘ _) (respect_id (obF G p.1) p.2) + ... = id ∘ natural_map nat_trans.id p.2 : {respect_id G p.1} + ... = id : id_compose + + definition functor_uncurry_comp ⦃p p' p'' : C ×c D⦄ (f' : p' ⟶ p'') (f : p ⟶ p') + : Ghom G (f' ∘ f) = Ghom G f' ∘ Ghom G f := + calc + Ghom G (f' ∘ f) + = homF (obF G p''.1) (f'.2 ∘ f.2) ∘ natural_map (homF G (f'.1 ∘ f.1)) p.2 : idp + ... = (homF (obF G p''.1) f'.2 ∘ homF (obF G p''.1) f.2) + ∘ natural_map (homF G (f'.1 ∘ f.1)) p.2 : {respect_comp (obF G p''.1) f'.2 f.2} + ... = (homF (obF G p''.1) f'.2 ∘ homF (obF G p''.1) f.2) + ∘ natural_map (homF G f'.1 ∘ homF G f.1) p.2 : {respect_comp G f'.1 f.1} + ... = (homF (obF G p''.1) f'.2 ∘ homF (obF G p''.1) f.2) + ∘ (natural_map (homF G f'.1) p.2 ∘ natural_map (homF G f.1) p.2) : idp + ... = (homF (obF G p''.1) f'.2 ∘ homF (obF G p''.1) f.2) + ∘ (natural_map (homF G f'.1) p.2 ∘ natural_map (homF G f.1) p.2) : idp + ... = (homF (obF G p''.1) f'.2 ∘ natural_map (homF G f'.1) p'.2) + ∘ (homF (obF G p'.1) f.2 ∘ natural_map (homF G f.1) p.2) : + square_prepostcompose (!naturality⁻¹ᵖ) _ _ + ... = Ghom G f' ∘ Ghom G f : idp + + definition functor_uncurry [reducible] : C ×c D ⇒ E := + functor.mk (functor_uncurry_ob G) + (functor_uncurry_hom G) + (functor_uncurry_id G) + (functor_uncurry_comp G) + -- open pi + -- definition functor_eq_mk'1 {F₁ F₂ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)} + -- {H₂ : Π(a b : C), hom a b → hom (F₂ a) (F₂ b)} (id₁ id₂ comp₁ comp₂) + -- (pF : F₁ = F₂) (pH : Π(a b : C) (f : hom a b), pF ▹ (H₁ a b f) = H₂ a b f) + -- : functor.mk F₁ H₁ id₁ comp₁ = functor.mk F₂ H₂ id₂ comp₂ := + -- functor_eq_mk'' id₁ id₂ comp₁ comp₂ pF + -- (eq_of_homotopy (λc, eq_of_homotopy (λc', eq_of_homotopy (λf, + -- begin + -- apply concat, rotate_left 1, exact (pH c c' f), + -- apply concat, rotate_left 1, + -- exact (pi_transport_constant pF (H₁ c c') f), + -- apply (apD10' f), + -- apply concat, rotate_left 1, + -- exact (pi_transport_constant pF (H₁ c) c'), + -- apply (apD10' c'), + -- apply concat, rotate_left 1, + -- exact (pi_transport_constant pF H₁ c), + -- apply idp + -- end)))) + + -- definition functor_eq_mk1 {F₁ F₂ : C ⇒ D} : Π(p : obF F₁ = obF F₂), + -- (Π(a b : C) (f : hom a b), transport (λF, hom (F a) (F b)) p (F₁ f) = F₂ f) + -- → F₁ = F₂ := + -- functor.rec_on F₁ (λO₁ H₁ id₁ comp₁, functor.rec_on F₂ (λO₂ H₂ id₂ comp₂ p, !functor_eq_mk'1)) + + --set_option pp.notation false + definition functor_uncurry_functor_curry : functor_uncurry (functor_curry F) = F := + functor_eq_mk (λp, ap (obF F) !prod.eta) + begin + intros (cd, cd', fg), + cases cd with (c,d), cases cd' with (c',d'), cases fg with (f,g), + have H : (functor_uncurry (functor_curry F)) (f, g) = F (f,g), + from calc + (functor_uncurry (functor_curry F)) (f, g) = homF F (id, g) ∘ homF F (f, id) : idp + ... = F (id ∘ f, g ∘ id) : respect_comp F (id,g) (f,id) + ... = F (f, g ∘ id) : {id_left f} + ... = F (f,g) : {id_right g}, + rewrite H, + apply sorry + end + --set_option pp.implicit true + definition functor_curry_functor_uncurry : functor_curry (functor_uncurry G) = G := + begin + fapply functor_eq_mk, + {intro c, + fapply functor_eq_mk, + {intro d, apply idp}, + {intros (d, d', g), + have H : homF (functor_curry (functor_uncurry G) c) g = homF (G c) g, + from calc + homF (functor_curry (functor_uncurry G) c) g + = homF (G c) g ∘ natural_map (homF G (ID c)) d : idp + ... = homF (G c) g ∘ natural_map (ID (G c)) d + : ap (λx, homF (G c) g ∘ natural_map x d) (respect_id G c) + ... = homF (G c) g : id_right, + rewrite H, +-- esimp {idp}, + apply sorry + } + }, + apply sorry + end definition equiv_functor_curry : (C ×c D ⇒ E) ≃ (C ⇒ E ^c D) := - equiv.mk _ !is_equiv_functor_curry + equiv.MK functor_curry + functor_uncurry + functor_curry_functor_uncurry + functor_uncurry_functor_curry + + + definition functor_prod_flip_ob : C ×c D ⇒ D ×c C := + functor.mk sorry sorry sorry sorry + + + definition contravariant_yoneda_embedding : Cᵒᵖ ⇒ set ^c C := + functor_curry !yoneda.representable_functor + end functor + -- Coq uses unit/counit definitions as basic -- open yoneda precategory.product precategory.opposite functor morphism diff --git a/hott/equiv_precomp.hlean b/hott/equiv_precomp.hlean deleted file mode 100644 index 6dc438e8f..000000000 --- a/hott/equiv_precomp.hlean +++ /dev/null @@ -1,87 +0,0 @@ -/- -Copyright (c) 2014 Jakob von Raumer. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Module: equiv_precomp -Author: Jakob von Raumer - -Ported from Coq HoTT --/ - --- This file is nowhere used. Do we want to keep it? -open eq function funext - -namespace is_equiv - context - - --Precomposition of arbitrary functions with f - definition precompose {A B : Type} (f : A → B) (C : Type) (h : B → C) : A → C := h ∘ f - - --Postcomposition of arbitrary functions with f - definition postcompose {A B : Type} (f : A → B) (C : Type) (l : C → A) : C → B := f ∘ l - - --Precomposing with an equivalence is an equivalence - definition arrow_equiv_arrow_of_equiv_dom [instance] {A B : Type} (f : A → B) [F : funext] [Hf : is_equiv f] (C : Type) - : is_equiv (precompose f C) := - adjointify (precompose f C) (λh, h ∘ f⁻¹) - (λh, eq_of_homotopy (λx, ap h (sect f x))) - (λg, eq_of_homotopy (λy, ap g (retr f y))) - - --Postcomposing with an equivalence is an equivalence - definition arrow_equiv_arrow_of_equiv_cod [instance] {A B : Type} (f : A → B) [F : funext] [Hf : is_equiv f] (C : Type) - : is_equiv (postcompose f C) := - adjointify (postcompose f C) (λl, f⁻¹ ∘ l) - (λh, eq_of_homotopy (λx, retr f (h x))) - (λg, eq_of_homotopy (λy, sect f (g y))) - - --Conversely, if pre- or post-composing with a function is always an equivalence, - --then that function is also an equivalence. It's convenient to know - --that we only need to assume the equivalence when the other type is - --the domain or the codomain. - private definition isequiv_precompose_eq {A B : Type} (f : A → B) (C D : Type) - (Ceq : is_equiv (precompose f C)) (Deq : is_equiv (precompose f D)) (k : C → D) (h : A → C) : - k ∘ (precompose f C)⁻¹ h = (precompose f D)⁻¹ (k ∘ h) := - let invD := inv (precompose f D) in - let invC := inv (precompose f C) in - have eq1 : invD (k ∘ h) = k ∘ (invC h), - from calc invD (k ∘ h) = invD (k ∘ (precompose f C (invC h))) : retr (precompose f C) h - ... = k ∘ (invC h) : !sect, - eq1⁻¹ - - definition is_equiv_of_is_equiv_precomp {A B : Type} (f : A → B) (Aeq : is_equiv (precompose f A)) - (Beq : is_equiv (precompose f B)) : (is_equiv f) := - let invA := inv (precompose f A) in - let invB := inv (precompose f B) in - let sect' : f ∘ (invA id) ∼ id := (λx, - calc f (invA id x) = (f ∘ invA id) x : idp - ... = invB (f ∘ id) x : apD10 (!isequiv_precompose_eq) - ... = invB (precompose f B id) x : idp - ... = x : apD10 (sect (precompose f B) id)) - in - let retr' : (invA id) ∘ f ∼ id := (λx, - calc invA id (f x) = precompose f A (invA id) x : idp - ... = x : apD10 (retr (precompose f A) id)) in - adjointify f (invA id) sect' retr' - - end - -end is_equiv - ---Bundled versions of the previous theorems -namespace equiv - - definition arrow_equiv_arrow_of_equiv_dom [F : funext] {A B C : Type} {eqf : A ≃ B} - : (B → C) ≃ (A → C) := - let f := to_fun eqf in - let Hf := to_is_equiv eqf in - equiv.mk (is_equiv.precompose f C) - (@is_equiv.arrow_equiv_arrow_of_equiv_dom A B f F Hf C) - - definition arrow_equiv_arrow_of_equiv_cod [F : funext] {A B C : Type} {eqf : A ≃ B} - : (C → A) ≃ (C → B) := - let f := to_fun eqf in - let Hf := to_is_equiv eqf in - equiv.mk (is_equiv.postcompose f C) - (@is_equiv.arrow_equiv_arrow_of_equiv_cod A B f F Hf C) - -end equiv diff --git a/hott/init/axioms/funext_of_ua.hlean b/hott/init/axioms/funext_of_ua.hlean index 3be24218e..2bc04fa77 100644 --- a/hott/init/axioms/funext_of_ua.hlean +++ b/hott/init/axioms/funext_of_ua.hlean @@ -144,7 +144,11 @@ end funext open funext definition eq_of_homotopy {A : Type} {P : A → Type} {f g : Π x, P x} : f ∼ g → f = g := -is_equiv.inv (@apD10 A P f g) +(@apD10 A P f g)⁻¹ + +definition eq_of_homotopy_id {A : Type} {P : A → Type} (f : Π x, P x) + : eq_of_homotopy (λx : A, idpath (f x)) = idpath f := +is_equiv.sect apD10 idp definition eq_of_homotopy2 {A B : Type} {P : A → B → Type} (f g : Πx y, P x y) : (Πx y, f x y = g x y) → f = g := @@ -152,5 +156,3 @@ definition eq_of_homotopy2 {A B : Type} {P : A → B → Type} definition naive_funext_of_ua : naive_funext := λ A P f g h, eq_of_homotopy h - -exit diff --git a/hott/truncation.hlean b/hott/truncation.hlean deleted file mode 100644 index 7dbafdd5c..000000000 --- a/hott/truncation.hlean +++ /dev/null @@ -1,23 +0,0 @@ -/- -Copyright (c) 2014 Jakob von Raumer. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Module: truncation -Authors: Jakob von Raumer --/ - -open is_trunc - --- Axiomatize the truncation operator as long as we do not have --- Higher inductive types - -axiom truncate (A : Type) (n : trunc_index) : Type - -axiom truncate.mk {A : Type} (n : trunc_index) (a : A) : truncate A n - -axiom truncate.is_trunc (A : Type) (n : trunc_index) : is_trunc n (truncate A n) - -axiom truncate.rec_on {A : Type} {n : trunc_index} {C : truncate A n → Type} - (ta : truncate A n) - [H : Π (ta : truncate A n), is_trunc n (C ta)] - (CC : Π (a : A), C (truncate.mk n a)) : C ta diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index a4d7248e8..42e0d75d5 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -17,24 +17,24 @@ namespace is_pointed variables {A B : Type} (f : A → B) -- Any contractible type is pointed - protected definition contr [instance] [H : is_contr A] : is_pointed A := + definition is_pointed_of_is_contr [instance] [H : is_contr A] : is_pointed A := is_pointed.mk !center -- A pi type with a pointed target is pointed - protected definition pi [instance] {P : A → Type} [H : Πx, is_pointed (P x)] + definition is_pointed_pi [instance] {P : A → Type} [H : Πx, is_pointed (P x)] : is_pointed (Πx, P x) := is_pointed.mk (λx, point (P x)) -- A sigma type of pointed components is pointed - protected definition sigma [instance] {P : A → Type} [G : is_pointed A] + definition is_pointed_sigma [instance] {P : A → Type} [G : is_pointed A] [H : is_pointed (P !point)] : is_pointed (Σx, P x) := is_pointed.mk ⟨!point,!point⟩ - protected definition prod [H1 : is_pointed A] [H2 : is_pointed B] + definition is_pointed_prod [H1 : is_pointed A] [H2 : is_pointed B] : is_pointed (A × B) := is_pointed.mk (!point,!point) - protected definition loop_space (a : A) : is_pointed (a = a) := + definition is_pointed_loop_space (a : A) : is_pointed (a = a) := is_pointed.mk idp end is_pointed