From 1559e0e58c45f0c87c6b47f1ad74aa4e82105d88 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sat, 28 Feb 2015 01:16:20 -0500 Subject: [PATCH] feat(hott): some more renaming in category library --- hott/algebra/category/basic.hlean | 4 +- hott/algebra/category/constructions.hlean | 44 ++- hott/algebra/groupoid.hlean | 16 +- hott/algebra/precategory/constructions.hlean | 10 +- hott/algebra/precategory/iso.hlean | 342 ++++++++++++++++--- hott/algebra/precategory/morphism.hlean | 42 +-- hott/algebra/precategory/nat_trans.hlean | 3 +- hott/algebra/precategory/yoneda.hlean | 13 +- hott/init/axioms/funext_of_ua.hlean | 6 +- hott/init/axioms/ua.hlean | 2 +- hott/init/equiv.hlean | 6 +- hott/init/trunc.hlean | 12 +- hott/types/trunc.hlean | 6 +- 13 files changed, 391 insertions(+), 115 deletions(-) diff --git a/hott/algebra/category/basic.hlean b/hott/algebra/category/basic.hlean index 657ad5608..1e651688c 100644 --- a/hott/algebra/category/basic.hlean +++ b/hott/algebra/category/basic.hlean @@ -8,7 +8,7 @@ Author: Jakob von Raumer import algebra.precategory.iso -open morphism is_equiv eq is_trunc +open iso is_equiv eq is_trunc -- A category is a precategory extended by a witness -- that the function from paths to isomorphisms, @@ -45,7 +45,7 @@ namespace category fapply is_trunc_is_equiv_closed, exact (@eq_of_iso _ _ a b), apply is_equiv_inv, - apply is_hset_isomorphic, + apply is_hset_iso, end end basic diff --git a/hott/algebra/category/constructions.hlean b/hott/algebra/category/constructions.hlean index 8712f63b8..43c561cd9 100644 --- a/hott/algebra/category/constructions.hlean +++ b/hott/algebra/category/constructions.hlean @@ -8,23 +8,51 @@ Authors: Floris van Doorn import .basic algebra.precategory.constructions -open eq prod eq eq.ops equiv is_trunc funext pi category.ops morphism category +--open eq eq.ops equiv category.ops iso category is_trunc +open eq category equiv iso is_equiv category.ops is_trunc iso.iso + +--TODO: MOVE THIS +namespace equiv + variables {A B : Type} + protected definition eq_mk' {f f' : A → B} [H : is_equiv f] [H' : is_equiv f'] (p : f = f') + : equiv.mk f H = equiv.mk f' H' := + apD011 equiv.mk p sorry --!is_hprop.elim + + protected definition eq_mk {f f' : A ≃ B} (p : to_fun f = to_fun f') : f = f' := + by (cases f; cases f'; apply (equiv.eq_mk' p)) + +end equiv namespace category - section hset - definition is_univalent_hset (a b : Precategory_hset) : is_equiv (@iso_of_eq _ _ a b) := - sorry + namespace set + definition equiv_equiv_iso (A B : Precategory_hset) : (A ≃ B) ≃ (A ≅ B) := + equiv.MK (λf, iso.MK (to_fun f) + (equiv.to_inv f) + (eq_of_homotopy (sect (to_fun f))) + (eq_of_homotopy (retr (to_fun f)))) + (λf, equiv.MK (to_hom f) + (iso.to_inv f) + (ap10 (right_inverse (to_hom f))) + (ap10 (left_inverse (to_hom f)))) + (λf, iso.eq_mk idp) + (λf, equiv.eq_mk idp) + + definition equiv_eq_iso (A B : Precategory_hset) : (A ≃ B) = (A ≅ B) := + ua !equiv_equiv_iso + + definition is_univalent (A B : Precategory_hset) : is_equiv (@iso_of_eq _ _ A B) := + sorry + end set + + definition category_hset [reducible] [instance] : category hset := - category.mk' hset precategory_hset is_univalent_hset + category.mk' hset precategory_hset set.is_univalent definition Category_hset [reducible] : Category := Category.mk hset category_hset - definition isomorphic_hset_eq_equiv (a b : Category_hset) : (a ≅ b) = (a ≃ b) := sorry - - end hset namespace ops abbreviation set := Category_hset end ops diff --git a/hott/algebra/groupoid.hlean b/hott/algebra/groupoid.hlean index 35fbf6e49..eb4260d23 100644 --- a/hott/algebra/groupoid.hlean +++ b/hott/algebra/groupoid.hlean @@ -8,9 +8,9 @@ Author: Jakob von Raumer Ported from Coq HoTT -/ -import .precategory.morphism .group +import .precategory.iso .group -open eq is_trunc morphism category path_algebra nat unit +open eq is_trunc iso category path_algebra nat unit namespace category @@ -48,8 +48,8 @@ namespace category apply (ID (center ob)), intro f, apply id_left, intro f, apply id_right, - intro f, exact (morphism.inverse f), - intro f, exact (morphism.inverse_comp f), + intro f, exact (iso.inverse f), + intro f, exact (iso.left_inverse f), end definition group_of_groupoid_unit [G : groupoid unit] : group (hom ⋆ ⋆) := @@ -61,8 +61,8 @@ namespace category apply (ID ⋆), intro f, apply id_left, intro f, apply id_right, - intro f, exact (morphism.inverse f), - intro f, exact (morphism.inverse_comp f), + intro f, exact (iso.inverse f), + intro f, exact (iso.left_inverse f), end -- Conversely we can turn each group into a groupoid on the unit type @@ -91,8 +91,8 @@ namespace category apply (ID a), intro f, apply id_left, intro f, apply id_right, - intro f, exact (morphism.inverse f), - intro f, exact (morphism.inverse_comp f), + intro f, exact (iso.inverse f), + intro f, exact (iso.left_inverse f), end -- Bundled version of categories diff --git a/hott/algebra/precategory/constructions.hlean b/hott/algebra/precategory/constructions.hlean index c74cbcd96..7f8bcba29 100644 --- a/hott/algebra/precategory/constructions.hlean +++ b/hott/algebra/precategory/constructions.hlean @@ -152,7 +152,7 @@ namespace category Precategory.mk hset precategory_hset section precategory_functor - open morphism functor nat_trans + open iso functor nat_trans definition precategory_functor [instance] [reducible] (D C : Precategory) : precategory (functor C D) := precategory.mk (λa b, nat_trans a b) @@ -177,16 +177,16 @@ namespace category (λc, (η c)⁻¹) (λc d f, begin - apply to_fun.comp_inverse_eq_of_eq_comp, + apply comp_inverse_eq_of_eq_comp, apply concat, rotate_left 1, apply assoc, - apply to_fun.eq_inverse_comp_of_comp_eq, + apply eq_inverse_comp_of_comp_eq, apply inverse, apply naturality, end) definition nat_trans_left_inverse : nat_trans_inverse η ∘n η = nat_trans.id := begin fapply (apD011 nat_trans.mk), - apply eq_of_homotopy, intro c, apply inverse_comp, + apply eq_of_homotopy, intro c, apply left_inverse, apply eq_of_homotopy, intros, apply eq_of_homotopy, intros, apply eq_of_homotopy, intros, apply is_hset.elim end @@ -194,7 +194,7 @@ namespace category definition nat_trans_right_inverse : η ∘n nat_trans_inverse η = nat_trans.id := begin fapply (apD011 nat_trans.mk), - apply eq_of_homotopy, intro c, apply comp_inverse, + apply eq_of_homotopy, intro c, apply right_inverse, apply eq_of_homotopy, intros, apply eq_of_homotopy, intros, apply eq_of_homotopy, intros, apply is_hset.elim end diff --git a/hott/algebra/precategory/iso.hlean b/hott/algebra/precategory/iso.hlean index 0412ae999..563aebf0f 100644 --- a/hott/algebra/precategory/iso.hlean +++ b/hott/algebra/precategory/iso.hlean @@ -1,72 +1,316 @@ /- -Copyright (c) 2014 Jakob von Raumer. All rights reserved. +Copyright (c) 2014 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Module: algebra.precategory.to_fun -Authors: Floris van Doorn, Jakob von Raumer +Module: algebra.category.morphism +Author: Floris van Doorn, Jakob von Raumer -/ -import .basic .morphism types.sigma +import algebra.precategory.basic types.sigma -open eq category sigma sigma.ops equiv is_equiv function is_trunc -open prod +open eq category prod equiv is_equiv sigma sigma.ops is_trunc -namespace morphism - variables {ob : Type} [C : precategory ob] include C +namespace iso + structure split_mono [class] {ob : Type} [C : precategory ob] {a b : ob} (f : a ⟶ b) := + {retraction_of : b ⟶ a} + (retraction_comp : retraction_of ∘ f = id) + structure split_epi [class] {ob : Type} [C : precategory ob] {a b : ob} (f : a ⟶ b) := + {section_of : b ⟶ a} + (comp_section : f ∘ section_of = id) + structure is_iso [class] {ob : Type} [C : precategory ob] {a b : ob} (f : a ⟶ b) := + {inverse : b ⟶ a} + (left_inverse : inverse ∘ f = id) + (right_inverse : f ∘ inverse = id) + + attribute is_iso [multiple-instances] + open split_mono split_epi is_iso + definition retraction_of [reducible] := @split_mono.retraction_of + definition retraction_comp [reducible] := @split_mono.retraction_comp + definition section_of [reducible] := @split_epi.section_of + definition comp_section [reducible] := @split_epi.comp_section + definition inverse [reducible] := @is_iso.inverse + definition left_inverse [reducible] := @is_iso.left_inverse + definition right_inverse [reducible] := @is_iso.right_inverse + postfix `⁻¹` := inverse + --a second notation for the inverse, which is not overloaded + postfix [parsing-only] `⁻¹ʰ`:std.prec.max_plus := inverse + + variables {ob : Type} [C : precategory ob] variables {a b c : ob} {g : b ⟶ c} {f : a ⟶ b} {h : b ⟶ a} + include C + + definition split_mono_of_is_iso [instance] [priority 300] [reducible] + (f : a ⟶ b) [H : is_iso f] : split_mono f := + split_mono.mk !left_inverse + + definition split_epi_of_is_iso [instance] [priority 300] [reducible] + (f : a ⟶ b) [H : is_iso f] : split_epi f := + split_epi.mk !right_inverse + + definition is_iso_id [instance] [priority 500] (a : ob) : is_iso (ID a) := + is_iso.mk !id_comp !id_comp + + definition is_iso_inverse [instance] [priority 200] (f : a ⟶ b) [H : is_iso f] : is_iso f⁻¹ := + is_iso.mk !right_inverse !left_inverse + + definition left_inverse_eq_right_inverse {f : a ⟶ b} {g g' : hom b a} + (Hl : g ∘ f = id) (Hr : f ∘ g' = id) : g = g' := + by rewrite [-(id_right g), -Hr, assoc, Hl, id_left] + + definition retraction_eq [H : split_mono f] (H2 : f ∘ h = id) : retraction_of f = h := + left_inverse_eq_right_inverse !retraction_comp H2 + + definition section_eq [H : split_epi f] (H2 : h ∘ f = id) : section_of f = h := + (left_inverse_eq_right_inverse H2 !comp_section)⁻¹ + + definition inverse_eq_right [H : is_iso f] (H2 : f ∘ h = id) : f⁻¹ = h := + left_inverse_eq_right_inverse !left_inverse H2 + + definition inverse_eq_left [H : is_iso f] (H2 : h ∘ f = id) : f⁻¹ = h := + (left_inverse_eq_right_inverse H2 !right_inverse)⁻¹ + + definition retraction_eq_section (f : a ⟶ b) [Hl : split_mono f] [Hr : split_epi f] : + retraction_of f = section_of f := + retraction_eq !comp_section + + definition is_iso_of_split_epi_of_split_mono (f : a ⟶ b) [Hl : split_mono f] [Hr : split_epi f] + : is_iso f := + is_iso.mk ((retraction_eq_section f) ▹ (retraction_comp f)) (comp_section f) + + definition inverse_unique (H H' : is_iso f) : @inverse _ _ _ _ f H = @inverse _ _ _ _ f H' := + inverse_eq_left !left_inverse + + definition inverse_involutive (f : a ⟶ b) [H : is_iso f] : (f⁻¹)⁻¹ = f := + inverse_eq_right !left_inverse + + definition retraction_id (a : ob) : retraction_of (ID a) = id := + retraction_eq !id_comp + + definition section_id (a : ob) : section_of (ID a) = id := + section_eq !id_comp + + definition id_inverse (a : ob) [H : is_iso (ID a)] : (ID a)⁻¹ = id := + inverse_eq_left !id_comp + + definition split_mono_comp [instance] [priority 150] (g : b ⟶ c) (f : a ⟶ b) + [Hf : split_mono f] [Hg : split_mono g] : split_mono (g ∘ f) := + split_mono.mk + (show (retraction_of f ∘ retraction_of g) ∘ g ∘ f = id, + by rewrite [-assoc, assoc _ g f, retraction_comp, id_left, retraction_comp]) + + definition split_epi_comp [instance] [priority 150] (g : b ⟶ c) (f : a ⟶ b) + [Hf : split_epi f] [Hg : split_epi g] : split_epi (g ∘ f) := + split_epi.mk + (show (g ∘ f) ∘ section_of f ∘ section_of g = id, + by rewrite [-assoc, {f ∘ _}assoc, comp_section, id_left, comp_section]) + + definition is_iso_comp [instance] [priority 150] (g : b ⟶ c) (f : a ⟶ b) + [Hf : is_iso f] [Hg : is_iso g] : is_iso (g ∘ f) := + !is_iso_of_split_epi_of_split_mono -- "is_iso f" is equivalent to a certain sigma type - protected definition sigma_char (f : hom a b) : - (Σ (g : hom b a), (g ∘ f = id) × (f ∘ g = id)) ≃ is_iso f := + -- definition is_iso.sigma_char (f : hom a b) : + -- (Σ (g : hom b a), (g ∘ f = id) × (f ∘ g = id)) ≃ is_iso f := + -- begin + -- fapply equiv.MK, + -- {intro S, apply is_iso.mk, + -- exact (pr₁ S.2), + -- exact (pr₂ S.2)}, + -- {intro H, cases H with (g, η, ε), + -- exact (sigma.mk g (pair η ε))}, + -- {intro H, cases H, apply idp}, + -- {intro S, cases S with (g, ηε), cases ηε, apply idp}, + -- end + + definition is_hprop_is_iso [instance] (f : hom a b) : is_hprop (is_iso f) := begin - fapply (equiv.mk), - {intro S, apply is_iso.mk, - exact (pr₁ S.2), - exact (pr₂ S.2)}, - {fapply adjointify, - {intro H, cases H with (g, η, ε), - exact (sigma.mk g (pair η ε))}, - {intro H, cases H, apply idp}, - {intro S, cases S with (g, ηε), cases ηε, apply idp}}, + apply is_hprop.mk, intros (H, H'), + cases H with (g, li, ri), cases H' with (g', li', ri'), + fapply (apD0111 (@is_iso.mk ob C a b f)), + apply left_inverse_eq_right_inverse, + apply li, + apply ri', + apply is_hprop.elim, + apply is_hprop.elim, end - -- The structure for isomorphism can be characterized up to equivalence - -- by a sigma type. - definition isomorphic.sigma_char ⦃a b : ob⦄ : (Σ (f : hom a b), is_iso f) ≃ (a ≅ b) := - begin - fapply (equiv.mk), - {intro S, apply isomorphic.mk, apply (S.2)}, - {fapply adjointify, - {intro p, cases p with (f, H), exact (sigma.mk f H)}, - {intro p, cases p, apply idp}, - {intro S, cases S, apply idp}}, - end + /- iso objects -/ + structure iso (a b : ob) := + (to_hom : hom a b) + [struct : is_iso to_hom] - set_option apply.class_instance false -- disable class instance resolution in the apply tactic + infix `≅`:50 := iso.iso + attribute iso.struct [instance] [priority 400] - -- The statement "f is an isomorphism" is a mere proposition - definition is_hset_iso : is_hset (is_iso f) := - begin - apply is_trunc_is_equiv_closed, - apply (equiv.to_is_equiv (!sigma_char)), - apply is_trunc_sigma, - apply (!homH), - {intro g, apply is_trunc_prod, - repeat (apply is_trunc_eq; apply is_trunc_succ; apply (!homH))}, - end + namespace iso + attribute to_hom [coercion] + + definition MK (f : a ⟶ b) (g : b ⟶ a) (H1 : g ∘ f = id) (H2 : f ∘ g = id) := + @mk _ _ _ _ f (is_iso.mk H1 H2) + + definition to_inv (f : a ≅ b) : b ⟶ a := + (to_hom f)⁻¹ + + protected definition refl (a : ob) : a ≅ a := + mk (ID a) + + protected definition symm ⦃a b : ob⦄ (H : a ≅ b) : b ≅ a := + mk (to_hom H)⁻¹ + + protected definition trans ⦃a b c : ob⦄ (H1 : a ≅ b) (H2 : b ≅ c) : a ≅ c := + mk (to_hom H2 ∘ to_hom H1) + + protected definition eq_mk' {f f' : a ⟶ b} [H : is_iso f] [H' : is_iso f'] (p : f = f') + : iso.mk f = iso.mk f' := + apD011 iso.mk p !is_hprop.elim + + protected definition eq_mk {f f' : a ≅ b} (p : to_hom f = to_hom f') : f = f' := + by (cases f; cases f'; apply (iso.eq_mk' p)) + + -- The structure for isomorphism can be characterized up to equivalence by a sigma type. + definition sigma_char ⦃a b : ob⦄ : (Σ (f : hom a b), is_iso f) ≃ (a ≅ b) := + begin + fapply (equiv.mk), + {intro S, apply iso.mk, apply (S.2)}, + {fapply adjointify, + {intro p, cases p with (f, H), exact (sigma.mk f H)}, + {intro p, cases p, apply idp}, + {intro S, cases S, apply idp}}, + end + + end iso -- The type of isomorphisms between two objects is a set - definition is_hset_isomorphic : is_hset (a ≅ b) := + definition is_hset_iso [instance] : is_hset (a ≅ b) := begin apply is_trunc_is_equiv_closed, - apply (equiv.to_is_equiv (!isomorphic.sigma_char)), - apply is_trunc_sigma, - apply homH, - {intro f, apply is_hset_iso}, + apply (equiv.to_is_equiv (!iso.sigma_char)), end - -- In a precategory, equal objects are isomorphic definition iso_of_eq (p : a = b) : a ≅ b := - eq.rec_on p (isomorphic.mk id) + eq.rec_on p (iso.mk id) -end morphism + structure mono [class] (f : a ⟶ b) := + (elim : ∀c (g h : hom c a), f ∘ g = f ∘ h → g = h) + structure epi [class] (f : a ⟶ b) := + (elim : ∀c (g h : hom b c), g ∘ f = h ∘ f → g = h) + + definition mono_of_split_mono [instance] (f : a ⟶ b) [H : split_mono f] : mono f := + mono.mk + (λ c g h H, + calc + g = id ∘ g : by rewrite id_left + ... = (retraction_of f ∘ f) ∘ g : by rewrite -retraction_comp + ... = (retraction_of f ∘ f) ∘ h : by rewrite [-assoc, H, -assoc] + ... = id ∘ h : by rewrite retraction_comp + ... = h : by rewrite id_left) + + definition epi_of_split_epi [instance] (f : a ⟶ b) [H : split_epi f] : epi f := + epi.mk + (λ c g h H, + calc + g = g ∘ id : by rewrite id_right + ... = g ∘ f ∘ section_of f : by rewrite -comp_section + ... = h ∘ f ∘ section_of f : by rewrite [assoc, H, -assoc] + ... = h ∘ id : by rewrite comp_section + ... = h : by rewrite id_right) + + definition mono_comp [instance] (g : b ⟶ c) (f : a ⟶ b) [Hf : mono f] [Hg : mono g] + : mono (g ∘ f) := + mono.mk + (λ d h₁ h₂ H, + have H2 : g ∘ (f ∘ h₁) = g ∘ (f ∘ h₂), + begin + rewrite *assoc, exact H + end, + !mono.elim (!mono.elim H2)) + + definition epi_comp [instance] (g : b ⟶ c) (f : a ⟶ b) [Hf : epi f] [Hg : epi g] + : epi (g ∘ f) := + epi.mk + (λ d h₁ h₂ H, + have H2 : (h₁ ∘ g) ∘ f = (h₂ ∘ g) ∘ f, + begin + rewrite -*assoc, exact H + end, + !epi.elim (!epi.elim H2)) + +end iso + +namespace iso + /- + rewrite lemmas for inverses, modified from + https://github.com/JasonGross/HoTT-categories/blob/master/theories/Categories/Category/Morphisms.v + -/ + section + variables {ob : Type} [C : precategory ob] include C + variables {a b c d : ob} (f : b ⟶ a) + (r : c ⟶ d) (q : b ⟶ c) (p : a ⟶ b) + (g : d ⟶ c) + variable [Hq : is_iso q] include Hq + definition comp.right_inverse : q ∘ q⁻¹ = id := !right_inverse + definition comp.left_inverse : q⁻¹ ∘ q = id := !left_inverse + definition inverse_comp_cancel_left : q⁻¹ ∘ (q ∘ p) = p := + by rewrite [assoc, left_inverse, id_left] + definition comp_inverse_cancel_left : q ∘ (q⁻¹ ∘ g) = g := + by rewrite [assoc, right_inverse, id_left] + definition comp_inverse_cancel_right : (r ∘ q) ∘ q⁻¹ = r := + by rewrite [-assoc, right_inverse, id_right] + definition inverse_comp_cancel_right : (f ∘ q⁻¹) ∘ q = f := + by rewrite [-assoc, left_inverse, id_right] + + definition comp_inverse [Hp : is_iso p] [Hpq : is_iso (q ∘ p)] : (q ∘ p)⁻¹ʰ = p⁻¹ʰ ∘ q⁻¹ʰ := + inverse_eq_left + (show (p⁻¹ʰ ∘ q⁻¹ʰ) ∘ q ∘ p = id, from + by rewrite [-assoc, inverse_comp_cancel_left, left_inverse]) + + definition inverse_comp_inverse_left [H' : is_iso g] : (q⁻¹ ∘ g)⁻¹ = g⁻¹ ∘ q := + inverse_involutive q ▹ comp_inverse q⁻¹ g + + definition inverse_comp_inverse_right [H' : is_iso f] : (q ∘ f⁻¹)⁻¹ = f ∘ q⁻¹ := + inverse_involutive f ▹ comp_inverse q f⁻¹ + + definition inverse_comp_inverse_inverse [H' : is_iso r] : (q⁻¹ ∘ r⁻¹)⁻¹ = r ∘ q := + inverse_involutive r ▹ inverse_comp_inverse_left q r⁻¹ + end + + section + variables {ob : Type} {C : precategory ob} include C + variables {d c b a : ob} + {i : b ⟶ c} {f : b ⟶ a} + {r : c ⟶ d} {q : b ⟶ c} {p : a ⟶ b} + {g : d ⟶ c} {h : c ⟶ b} + {x : b ⟶ d} {z : a ⟶ c} + {y : d ⟶ b} {w : c ⟶ a} + variable [Hq : is_iso q] include Hq + + definition comp_eq_of_eq_inverse_comp (H : y = q⁻¹ ∘ g) : q ∘ y = g := + H⁻¹ ▹ comp_inverse_cancel_left q g + definition comp_eq_of_eq_comp_inverse (H : w = f ∘ q⁻¹) : w ∘ q = f := + H⁻¹ ▹ inverse_comp_cancel_right f q + definition inverse_comp_eq_of_eq_comp (H : z = q ∘ p) : q⁻¹ ∘ z = p := + H⁻¹ ▹ inverse_comp_cancel_left q p + definition comp_inverse_eq_of_eq_comp (H : x = r ∘ q) : x ∘ q⁻¹ = r := + H⁻¹ ▹ comp_inverse_cancel_right r q + definition eq_comp_of_inverse_comp_eq (H : q⁻¹ ∘ g = y) : g = q ∘ y := + (comp_eq_of_eq_inverse_comp H⁻¹)⁻¹ + definition eq_comp_of_comp_inverse_eq (H : f ∘ q⁻¹ = w) : f = w ∘ q := + (comp_eq_of_eq_comp_inverse H⁻¹)⁻¹ + definition eq_inverse_comp_of_comp_eq (H : q ∘ p = z) : p = q⁻¹ ∘ z := + (inverse_comp_eq_of_eq_comp H⁻¹)⁻¹ + definition eq_comp_inverse_of_comp_eq (H : r ∘ q = x) : r = x ∘ q⁻¹ := + (comp_inverse_eq_of_eq_comp H⁻¹)⁻¹ + definition eq_inverse_of_comp_eq_id' (H : h ∘ q = id) : h = q⁻¹ := (inverse_eq_left H)⁻¹ + definition eq_inverse_of_comp_eq_id (H : q ∘ h = id) : h = q⁻¹ := (inverse_eq_right H)⁻¹ + definition eq_of_comp_inverse_eq_id (H : i ∘ q⁻¹ = id) : i = q := + eq_inverse_of_comp_eq_id' H ⬝ inverse_involutive q + definition eq_of_inverse_comp_eq_id (H : q⁻¹ ∘ i = id) : i = q := + eq_inverse_of_comp_eq_id H ⬝ inverse_involutive q + definition eq_of_id_eq_comp_inverse (H : id = i ∘ q⁻¹) : q = i := (eq_of_comp_inverse_eq_id H⁻¹)⁻¹ + definition eq_of_id_eq_inverse_comp (H : id = q⁻¹ ∘ i) : q = i := (eq_of_inverse_comp_eq_id H⁻¹)⁻¹ + definition inverse_eq_of_id_eq_comp (H : id = h ∘ q) : q⁻¹ = h := + (eq_inverse_of_comp_eq_id' H⁻¹)⁻¹ + definition inverse_eq_of_id_eq_comp' (H : id = q ∘ h) : q⁻¹ = h := + (eq_inverse_of_comp_eq_id H⁻¹)⁻¹ + end +end iso diff --git a/hott/algebra/precategory/morphism.hlean b/hott/algebra/precategory/morphism.hlean index c53dcf275..766c3990e 100644 --- a/hott/algebra/precategory/morphism.hlean +++ b/hott/algebra/precategory/morphism.hlean @@ -19,8 +19,8 @@ namespace morphism (comp_section : f ∘ section_of = id) structure is_iso [class] {ob : Type} [C : precategory ob] {a b : ob} (f : a ⟶ b) := {inverse : b ⟶ a} - (inverse_comp : inverse ∘ f = id) - (comp_inverse : f ∘ inverse = id) + (left_inverse : inverse ∘ f = id) + (right_inverse : f ∘ inverse = id) attribute is_iso [multiple-instances] open split_mono split_epi is_iso @@ -29,8 +29,8 @@ namespace morphism definition section_of [reducible] := @split_epi.section_of definition comp_section [reducible] := @split_epi.comp_section definition inverse [reducible] := @is_iso.inverse - definition inverse_comp [reducible] := @is_iso.inverse_comp - definition comp_inverse [reducible] := @is_iso.comp_inverse + definition left_inverse [reducible] := @is_iso.left_inverse + definition right_inverse [reducible] := @is_iso.right_inverse postfix `⁻¹` := inverse --a second notation for the inverse, which is not overloaded postfix [parsing-only] `⁻¹ʰ`:std.prec.max_plus := inverse @@ -41,17 +41,17 @@ namespace morphism definition iso_imp_retraction [instance] [priority 300] [reducible] (f : a ⟶ b) [H : is_iso f] : split_mono f := - split_mono.mk !inverse_comp + split_mono.mk !left_inverse definition iso_imp_section [instance] [priority 300] [reducible] (f : a ⟶ b) [H : is_iso f] : split_epi f := - split_epi.mk !comp_inverse + split_epi.mk !right_inverse definition is_iso_id [instance] [priority 500] (a : ob) : is_iso (ID a) := is_iso.mk !id_comp !id_comp definition is_iso_inverse [instance] [priority 200] (f : a ⟶ b) [H : is_iso f] : is_iso f⁻¹ := - is_iso.mk !comp_inverse !inverse_comp + is_iso.mk !right_inverse !left_inverse definition left_inverse_eq_right_inverse {f : a ⟶ b} {g g' : hom b a} (Hl : g ∘ f = id) (Hr : f ∘ g' = id) : g = g' := @@ -64,10 +64,10 @@ namespace morphism (left_inverse_eq_right_inverse H2 !comp_section)⁻¹ definition inverse_eq_right [H : is_iso f] (H2 : f ∘ h = id) : f⁻¹ = h := - left_inverse_eq_right_inverse !inverse_comp H2 + left_inverse_eq_right_inverse !left_inverse H2 definition inverse_eq_left [H : is_iso f] (H2 : h ∘ f = id) : f⁻¹ = h := - (left_inverse_eq_right_inverse H2 !comp_inverse)⁻¹ + (left_inverse_eq_right_inverse H2 !right_inverse)⁻¹ definition retraction_eq_section (f : a ⟶ b) [Hl : split_mono f] [Hr : split_epi f] : retraction_of f = section_of f := @@ -78,10 +78,10 @@ namespace morphism is_iso.mk ((retraction_eq_section f) ▹ (retraction_comp f)) (comp_section f) definition inverse_unique (H H' : is_iso f) : @inverse _ _ _ _ f H = @inverse _ _ _ _ f H' := - inverse_eq_left !inverse_comp + inverse_eq_left !left_inverse definition inverse_involutive (f : a ⟶ b) [H : is_iso f] : (f⁻¹)⁻¹ = f := - inverse_eq_right !inverse_comp + inverse_eq_right !left_inverse definition retraction_id (a : ob) : retraction_of (ID a) = id := retraction_eq !id_comp @@ -188,27 +188,27 @@ namespace morphism (r : c ⟶ d) (q : b ⟶ c) (p : a ⟶ b) (g : d ⟶ c) variable [Hq : is_iso q] include Hq - definition comp.right_inverse : q ∘ q⁻¹ = id := !comp_inverse - definition comp.left_inverse : q⁻¹ ∘ q = id := !inverse_comp + definition comp.right_inverse : q ∘ q⁻¹ = id := !right_inverse + definition comp.left_inverse : q⁻¹ ∘ q = id := !left_inverse definition inverse_comp_cancel_left : q⁻¹ ∘ (q ∘ p) = p := - by rewrite [assoc, inverse_comp, id_left] + by rewrite [assoc, left_inverse, id_left] definition comp_inverse_cancel_left : q ∘ (q⁻¹ ∘ g) = g := - by rewrite [assoc, comp_inverse, id_left] + by rewrite [assoc, right_inverse, id_left] definition comp_inverse_cancel_right : (r ∘ q) ∘ q⁻¹ = r := - by rewrite [-assoc, comp_inverse, id_right] + by rewrite [-assoc, right_inverse, id_right] definition inverse_comp_cancel_right : (f ∘ q⁻¹) ∘ q = f := - by rewrite [-assoc, inverse_comp, id_right] + by rewrite [-assoc, left_inverse, id_right] - definition comp_inverse [Hp : is_iso p] [Hpq : is_iso (q ∘ p)] : (q ∘ p)⁻¹ʰ = p⁻¹ʰ ∘ q⁻¹ʰ := + definition right_inverse [Hp : is_iso p] [Hpq : is_iso (q ∘ p)] : (q ∘ p)⁻¹ʰ = p⁻¹ʰ ∘ q⁻¹ʰ := inverse_eq_left (show (p⁻¹ʰ ∘ q⁻¹ʰ) ∘ q ∘ p = id, from - by rewrite [-assoc, inverse_comp_cancel_left, inverse_comp]) + by rewrite [-assoc, inverse_comp_cancel_left, left_inverse]) definition inverse_comp_inverse_left [H' : is_iso g] : (q⁻¹ ∘ g)⁻¹ = g⁻¹ ∘ q := - inverse_involutive q ▹ comp_inverse q⁻¹ g + inverse_involutive q ▹ right_inverse q⁻¹ g definition inverse_comp_inverse_right [H' : is_iso f] : (q ∘ f⁻¹)⁻¹ = f ∘ q⁻¹ := - inverse_involutive f ▹ comp_inverse q f⁻¹ + inverse_involutive f ▹ right_inverse q f⁻¹ definition inverse_comp_inverse_inverse [H' : is_iso r] : (q⁻¹ ∘ r⁻¹)⁻¹ = r ∘ q := inverse_involutive r ▹ inverse_comp_inverse_left q r⁻¹ diff --git a/hott/algebra/precategory/nat_trans.hlean b/hott/algebra/precategory/nat_trans.hlean index 863e709c6..527ad731e 100644 --- a/hott/algebra/precategory/nat_trans.hlean +++ b/hott/algebra/precategory/nat_trans.hlean @@ -6,7 +6,7 @@ Module: algebra.precategory.nat_trans Author: Floris van Doorn, Jakob von Raumer -/ -import .functor .morphism +import .functor .iso open eq category functor is_trunc equiv sigma.ops sigma is_equiv function pi funext structure nat_trans {C D : Precategory} (F G : C ⇒ D) := @@ -39,7 +39,6 @@ namespace nat_trans 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) (nat₂ : Π (a b : C) (f : hom a b), G f ∘ η₂ a = η₂ b ∘ F f) diff --git a/hott/algebra/precategory/yoneda.hlean b/hott/algebra/precategory/yoneda.hlean index 24c4bf23f..edf5367fc 100644 --- a/hott/algebra/precategory/yoneda.hlean +++ b/hott/algebra/precategory/yoneda.hlean @@ -29,8 +29,9 @@ namespace yoneda definition hom_functor (C : Precategory) : Cᵒᵖ ×c C ⇒ set := functor.mk (λ(x : Cᵒᵖ ×c C), homset x.1 x.2) (λ(x y : Cᵒᵖ ×c C) (f : _) (h : homset x.1 x.2), f.2 ∘⁅ C ⁆ (h ∘⁅ C ⁆ f.1)) - proof (λ(x : Cᵒᵖ ×c C), eq_of_homotopy (λ(h : homset x.1 x.2), !id_left ⬝ !id_right)) qed - -- (λ(x y z : Cᵒᵖ ×c C) (g : y ⟶ z) (f : x ⟶ y), eq_of_homotopy (λ(h : hom x.1 x.2), representable_functor_assoc g.2 f.2 h f.1 g.1)) + proof + (λ(x : Cᵒᵖ ×c C), eq_of_homotopy (λ(h : homset x.1 x.2), !id_left ⬝ !id_right)) + qed begin intros (x, y, z, g, f), apply eq_of_homotopy, intro h, exact (representable_functor_assoc g.2 f.2 h f.1 g.1), @@ -68,10 +69,10 @@ namespace functor definition functor_curry_hom_def ⦃c c' : C⦄ (f : c ⟶ c') (d : D) : (Fhom F f) d = to_fun_hom F (f, id) := idp - definition functor_curry_id (c : C) : Fhom F (ID c) = nat_trans.id := + theorem functor_curry_id (c : C) : Fhom F (ID c) = nat_trans.id := nat_trans_eq_mk (λd, respect_id F _) - definition functor_curry_comp ⦃c c' c'' : C⦄ (f' : c' ⟶ c'') (f : c ⟶ c') + theorem 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 (Fhom F (f' ∘ f)) d = F (f' ∘ f, id) : functor_curry_hom_def @@ -94,14 +95,14 @@ namespace functor to_fun_hom (to_fun_ob G p'.1) f.2 ∘ natural_map (to_fun_hom G f.1) p.2 local abbreviation Ghom := @functor_uncurry_hom - definition functor_uncurry_id (p : C ×c D) : Ghom G (ID p) = id := + theorem functor_uncurry_id (p : C ×c D) : Ghom G (ID p) = id := calc Ghom G (ID p) = to_fun_hom (to_fun_ob G p.1) id ∘ natural_map (to_fun_hom G id) p.2 : idp ... = id ∘ natural_map (to_fun_hom G id) p.2 : ap (λx, x ∘ _) (respect_id (to_fun_ob G p.1) p.2) ... = id ∘ natural_map nat_trans.id p.2 : {respect_id G p.1} ... = id : id_comp - definition functor_uncurry_comp ⦃p p' p'' : C ×c D⦄ (f' : p' ⟶ p'') (f : p ⟶ p') + theorem 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) diff --git a/hott/init/axioms/funext_of_ua.hlean b/hott/init/axioms/funext_of_ua.hlean index 94e1de7d7..468440b04 100644 --- a/hott/init/axioms/funext_of_ua.hlean +++ b/hott/init/axioms/funext_of_ua.hlean @@ -136,9 +136,9 @@ definition funext_of_ua : funext := funext_of_weak_funext (@weak_funext_of_ua) namespace funext -definition is_equiv_apD [instance] {A : Type} {P : A → Type} (f g : Π x, P x) - : is_equiv (@apD10 A P f g) := -funext_of_ua f g + definition is_equiv_apD [instance] {A : Type} {P : A → Type} (f g : Π x, P x) + : is_equiv (@apD10 A P f g) := + funext_of_ua f g end funext open funext diff --git a/hott/init/axioms/ua.hlean b/hott/init/axioms/ua.hlean index 5c4dca18f..e3626c3d6 100644 --- a/hott/init/axioms/ua.hlean +++ b/hott/init/axioms/ua.hlean @@ -30,7 +30,7 @@ axiom univalence (A B : Type) : is_equiv (@equiv_of_eq A B) attribute univalence [instance] -- This is the version of univalence axiom we will probably use most often -definition ua {A B : Type} : A ≃ B → A = B := +definition ua {A B : Type} : A ≃ B → A = B := (@equiv_of_eq A B)⁻¹ -- One consequence of UA is that we can transport along equivalencies of types diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index ee37eb065..a053ede24 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -228,9 +228,11 @@ namespace equiv variables {A B C : Type} - protected definition MK (f : A → B) (g : B → A) (retr : f ∘ g ∼ id) (sect : g ∘ f ∼ id) : A ≃ B := + protected definition MK [reducible] (f : A → B) (g : B → A) + (retr : f ∘ g ∼ id) (sect : g ∘ f ∼ id) : A ≃ B := equiv.mk f (adjointify f g retr sect) - definition to_inv (f : A ≃ B) : B → A := + + definition to_inv [reducible] (f : A ≃ B) : B → A := f⁻¹ protected definition refl : A ≃ A := diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index 297d15d9f..6c5aae39a 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -108,14 +108,16 @@ namespace is_trunc have K : ∀ (r : x = y), center_eq x y = r, from (λ r, eq.rec_on r !con.left_inv), (K p)⁻¹ ⬝ K q - definition is_contr_eq [instance] {A : Type} [H : is_contr A] (x y : A) : is_contr (x = y) + definition is_contr_eq {A : Type} [H : is_contr A] (x y : A) : is_contr (x = y) := is_contr.mk !center_eq (λ p, !hprop_eq) + local attribute is_contr_eq [instance] /- truncation is upward close -/ -- n-types are also (n+1)-types - definition is_trunc_succ [instance] (A : Type) (n : trunc_index) [H : is_trunc n A] : is_trunc (n.+1) A := + definition is_trunc_succ [instance] [priority 100] (A : Type) (n : trunc_index) + [H : is_trunc n A] : is_trunc (n.+1) A := trunc_index.rec_on n (λ A (H : is_contr A), !is_trunc_succ_intro) (λ n IH A (H : is_trunc (n.+1) A), @is_trunc_succ_intro _ _ (λ x y, IH _ !is_trunc_eq)) @@ -190,9 +192,9 @@ namespace is_trunc /- truncated universe -/ structure trunctype (n : trunc_index) := - (trunctype_type : Type) (is_trunc_trunctype_type : is_trunc n trunctype_type) - attribute trunctype.trunctype_type [coercion] - attribute trunctype.is_trunc_trunctype_type [instance] + (carrier : Type) (struct : is_trunc n carrier) + attribute trunctype.carrier [coercion] + attribute trunctype.struct [instance] notation n `-Type` := trunctype n abbreviation hprop := -1-Type diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index c52fd85ec..dd6a3f77e 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -122,7 +122,7 @@ namespace is_trunc (trunctype.{l} n) ≃ (Σ (A : Type.{l}), is_trunc n A) := begin fapply equiv.MK, - /--/ intro A, exact (⟨trunctype_type A, is_trunc_trunctype_type A⟩), + /--/ intro A, exact (⟨carrier A, struct A⟩), /--/ intro S, exact (trunctype.mk S.1 S.2), /--/ intro S, apply (sigma.rec_on S), intros (S1, S2), apply idp, intro A, apply (trunctype.rec_on A), intros (A1, A2), apply idp, @@ -130,11 +130,11 @@ namespace is_trunc -- set_option pp.notation false protected definition trunctype.eq (n : trunc_index) (A B : n-Type) : - (A = B) ≃ (trunctype_type A = trunctype_type B) := + (A = B) ≃ (carrier A = carrier B) := calc (A = B) ≃ (trunctype.sigma_char n A = trunctype.sigma_char n B) : eq_equiv_fn_eq_of_equiv ... ≃ ((trunctype.sigma_char n A).1 = (trunctype.sigma_char n B).1) : equiv.symm (!equiv_subtype) - ... ≃ (trunctype_type A = trunctype_type B) : equiv.refl + ... ≃ (carrier A = carrier B) : equiv.refl end is_trunc