From 23e6a3131d1c49cfa55bd3a3fccfe7c32d917322 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 24 Apr 2015 23:04:24 -0400 Subject: [PATCH] feat(precategory): add two redundant fields to precategory. Also some cleanup. In particular, all instances of "set_option apply.class_instance false" are removed --- hott/algebra/category/basic.hlean | 5 -- hott/algebra/groupoid.hlean | 34 ++++----- hott/algebra/precategory/basic.hlean | 75 +++++++++++++------- hott/algebra/precategory/constructions.hlean | 39 ++++------ hott/algebra/precategory/functor.hlean | 20 ++---- hott/algebra/precategory/nat_trans.hlean | 12 +--- hott/algebra/precategory/strict.hlean | 11 ++- hott/algebra/precategory/yoneda.hlean | 4 +- hott/arity.hlean | 12 +++- hott/init/trunc.hlean | 19 ++--- hott/types/equiv.hlean | 4 +- hott/types/pi.hlean | 8 +-- hott/types/sigma.hlean | 4 +- 13 files changed, 123 insertions(+), 124 deletions(-) diff --git a/hott/algebra/category/basic.hlean b/hott/algebra/category/basic.hlean index 85ffbbe85b..0d58a25b91 100644 --- a/hott/algebra/category/basic.hlean +++ b/hott/algebra/category/basic.hlean @@ -39,15 +39,12 @@ namespace category definition eq_of_iso [reducible] {a b : ob} : a ≅ b → a = b := iso_of_eq⁻¹ᵉ - set_option apply.class_instance false -- disable class instance resolution in the apply tactic - definition is_trunc_1_ob : is_trunc 1 ob := begin apply is_trunc_succ_intro, intros [a, b], fapply is_trunc_is_equiv_closed, exact (@eq_of_iso _ _ a b), apply is_equiv_inv, - apply is_hset_iso, end end basic @@ -58,8 +55,6 @@ namespace category (struct : category carrier) attribute Category.struct [instance] [coercion] - -- definition objects [reducible] := Category.objects - -- definition category_instance [instance] [coercion] [reducible] := Category.category_instance definition Category.to_Precategory [coercion] [reducible] (C : Category) : Precategory := Precategory.mk (Category.carrier C) C diff --git a/hott/algebra/groupoid.hlean b/hott/algebra/groupoid.hlean index 3cea3268a3..c22b1b77fc 100644 --- a/hott/algebra/groupoid.hlean +++ b/hott/algebra/groupoid.hlean @@ -15,27 +15,29 @@ open eq is_trunc iso category path_algebra nat unit namespace category structure groupoid [class] (ob : Type) extends parent : precategory ob := - (all_iso : Π ⦃a b : ob⦄ (f : hom a b), @is_iso ob parent a b f) + mk' :: (all_iso : Π ⦃a b : ob⦄ (f : hom a b), @is_iso ob parent a b f) abbreviation all_iso := @groupoid.all_iso attribute groupoid.all_iso [instance] [priority 100000] - definition groupoid.mk' [reducible] (ob : Type) (C : precategory ob) + definition groupoid.mk [reducible] {ob : Type} (C : precategory ob) (H : Π (a b : ob) (f : a ⟶ b), is_iso f) : groupoid ob := - precategory.rec_on C groupoid.mk H + precategory.rec_on C groupoid.mk' H - definition groupoid_of_1_type.{l} (A : Type.{l}) - [H : is_trunc 1 A] : groupoid.{l l} A := - groupoid.mk + definition precategory_of_1_type.{l} (A : Type.{l}) + [H : is_trunc 1 A] : precategory.{l l} A := + precategory.mk (λ (a b : A), a = b) - (λ (a b : A), have ish : is_hset (a = b), from is_trunc_eq nat.zero a b, ish) (λ (a b c : A) (p : b = c) (q : a = b), q ⬝ p) (λ (a : A), refl a) (λ (a b c d : A) (p : c = d) (q : b = c) (r : a = b), con.assoc r q p) (λ (a b : A) (p : a = b), con_idp p) (λ (a b : A) (p : a = b), idp_con p) - (λ (a b : A) (p : a = b), @is_iso.mk A _ a b p p⁻¹ - !con.right_inv !con.left_inv) + + definition groupoid_of_1_type.{l} (A : Type.{l}) + [H : is_trunc 1 A] : groupoid.{l l} A := + groupoid.mk !precategory_of_1_type + (λ (a b : A) (p : a = b), is_iso.mk !con.right_inv !con.left_inv) -- A groupoid with a contractible carrier is a group definition group_of_is_contr_groupoid {ob : Type} [H : is_contr ob] @@ -43,7 +45,7 @@ namespace category begin fapply group.mk, intros [f, g], apply (comp f g), - apply homH, + apply is_hset_hom, intros [f, g, h], apply (assoc f g h)⁻¹, apply (ID (center ob)), intro f, apply id_left, @@ -56,7 +58,7 @@ namespace category begin fapply group.mk, intros [f, g], apply (comp f g), - apply homH, + apply is_hset_hom, intros [f, g, h], apply (assoc f g h)⁻¹, apply (ID ⋆), intro f, apply id_left, @@ -68,7 +70,7 @@ namespace category -- Conversely we can turn each group into a groupoid on the unit type definition groupoid_of_group.{l} (A : Type.{l}) [G : group A] : groupoid.{l l} unit := begin - fapply groupoid.mk, + fapply groupoid.mk, fapply precategory.mk, intros, exact A, intros, apply (@group.carrier_hset A G), intros [a, b, c, g, h], exact (@group.mul A G g h), @@ -76,7 +78,7 @@ namespace category intros, exact (@group.mul_assoc A G h g f)⁻¹, intros, exact (@group.one_mul A G f), intros, exact (@group.mul_one A G f), - intros, apply is_iso.mk, + intros, esimp [precategory.mk], apply is_iso.mk, apply mul_left_inv, apply mul_right_inv, end @@ -86,7 +88,7 @@ namespace category begin fapply group.mk, intros [f, g], apply (comp f g), - apply homH, + apply is_hset_hom, intros [f, g, h], apply (assoc f g h)⁻¹, apply (ID a), intro f, apply id_left, @@ -102,8 +104,6 @@ namespace category (struct : groupoid carrier) attribute Groupoid.struct [instance] [coercion] - -- definition objects [reducible] := Category.objects - -- definition category_instance [instance] [coercion] [reducible] := Category.category_instance definition Groupoid.to_Precategory [coercion] [reducible] (C : Groupoid) : Precategory := Precategory.mk (Groupoid.carrier C) C @@ -111,7 +111,7 @@ namespace category definition groupoid.Mk [reducible] := Groupoid.mk definition groupoid.MK [reducible] (C : Precategory) (H : Π (a b : C) (f : a ⟶ b), is_iso f) : Groupoid := - Groupoid.mk C (groupoid.mk' C C H) + Groupoid.mk C (groupoid.mk C H) definition Groupoid.eta (C : Groupoid) : Groupoid.mk C C = C := Groupoid.rec (λob c, idp) C diff --git a/hott/algebra/precategory/basic.hlean b/hott/algebra/precategory/basic.hlean index be31104200..f66f36d7f5 100644 --- a/hott/algebra/precategory/basic.hlean +++ b/hott/algebra/precategory/basic.hlean @@ -11,18 +11,29 @@ open eq is_trunc pi namespace category +/- + Just as in Coq-HoTT we add two redundant fields to precategories: assoc' and id_id. + The first is to make (Cᵒᵖ)ᵒᵖ = C definitionally when C is a constructor. + The second is to ensure that the functor from the terminal category 1 ⇒ Cᵒᵖ is + opposite to the functor 1 ⇒ C. +-/ + structure precategory [class] (ob : Type) : Type := + mk' :: (hom : ob → ob → Type) - (homH : Π(a b : ob), is_hset (hom a b)) (comp : Π⦃a b c : ob⦄, hom b c → hom a b → hom a c) (ID : Π (a : ob), hom a a) - (assoc : Π ⦃a b c d : ob⦄ (h : hom c d) (g : hom b c) (f : hom a b), + (assoc : Π ⦃a b c d : ob⦄ (h : hom c d) (g : hom b c) (f : hom a b), comp h (comp g f) = comp (comp h g) f) + (assoc' : Π ⦃a b c d : ob⦄ (h : hom c d) (g : hom b c) (f : hom a b), + comp (comp h g) f = comp h (comp g f)) (id_left : Π ⦃a b : ob⦄ (f : hom a b), comp !ID f = f) (id_right : Π ⦃a b : ob⦄ (f : hom a b), comp f !ID = f) + (id_id : Π (a : ob), comp !ID !ID = ID a) + (is_hset_hom : Π(a b : ob), is_hset (hom a b)) attribute precategory [multiple-instances] - attribute precategory.homH [instance] + attribute precategory.is_hset_hom [instance] infixr `∘` := precategory.comp -- input ⟶ using \--> (this is a different arrow than \-> (→)) @@ -31,13 +42,25 @@ namespace category infixl `⟶`:25 := precategory.hom -- if you open this namespace, hom a b is printed as a ⟶ b end hom - abbreviation hom := @precategory.hom - abbreviation homH := @precategory.homH - abbreviation comp := @precategory.comp - abbreviation ID := @precategory.ID - abbreviation assoc := @precategory.assoc - abbreviation id_left := @precategory.id_left - abbreviation id_right := @precategory.id_right + abbreviation hom := @precategory.hom + abbreviation comp := @precategory.comp + abbreviation ID := @precategory.ID + abbreviation assoc := @precategory.assoc + abbreviation assoc' := @precategory.assoc' + abbreviation id_left := @precategory.id_left + abbreviation id_right := @precategory.id_right + abbreviation id_id := @precategory.id_id + abbreviation is_hset_hom := @precategory.is_hset_hom + + -- the constructor you want to use in practice + protected definition precategory.mk {ob : Type} (hom : ob → ob → Type) + [hset : Π (a b : ob), is_hset (hom a b)] + (comp : Π ⦃a b c : ob⦄, hom b c → hom a b → hom a c) (ID : Π (a : ob), hom a a) + (ass : Π ⦃a b c d : ob⦄ (h : hom c d) (g : hom b c) (f : hom a b), + comp h (comp g f) = comp (comp h g) f) + (idl : Π ⦃a b : ob⦄ (f : hom a b), comp (ID b) f = f) + (idr : Π ⦃a b : ob⦄ (f : hom a b), comp f (ID a) = f) : precategory ob := + precategory.mk' hom comp ID ass (λa b c d h g f, !ass⁻¹) idl idr (λa, !idl) hset section basic_lemmas variables {ob : Type} [C : precategory ob] @@ -62,8 +85,8 @@ namespace category 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 is_hprop_eq_hom [instance] : is_hprop (f = f') := + -- !is_trunc_eq end basic_lemmas section squares @@ -124,7 +147,7 @@ namespace category definition precategory.Mk [reducible] {ob} (C) : Precategory := Precategory.mk ob C definition precategory.MK [reducible] (a b c d e f g h) : Precategory := - Precategory.mk a (precategory.mk b c d e f g h) + Precategory.mk a (@precategory.mk _ b c d e f g h) abbreviation carrier := @Precategory.carrier @@ -159,25 +182,25 @@ namespace category comp1 h (comp1 g f) = comp1 (comp1 h g) f) (assoc2 : Π ⦃a b c d : ob⦄ (h : hom2 c d) (g : hom2 b c) (f : hom2 a b), comp2 h (comp2 g f) = comp2 (comp2 h g) f) + (assoc1' : Π ⦃a b c d : ob⦄ (h : hom1 c d) (g : hom1 b c) (f : hom1 a b), + comp1 (comp1 h g) f = comp1 h (comp1 g f)) + (assoc2' : Π ⦃a b c d : ob⦄ (h : hom2 c d) (g : hom2 b c) (f : hom2 a b), + comp2 (comp2 h g) f = comp2 h (comp2 g f)) (id_left1 : Π ⦃a b : ob⦄ (f : hom1 a b), comp1 !ID1 f = f) (id_left2 : Π ⦃a b : ob⦄ (f : hom2 a b), comp2 !ID2 f = f) (id_right1 : Π ⦃a b : ob⦄ (f : hom1 a b), comp1 f !ID1 = f) (id_right2 : Π ⦃a b : ob⦄ (f : hom2 a b), comp2 f !ID2 = f) + (id_id1 : Π (a : ob), comp1 !ID1 !ID1 = ID1 a) + (id_id2 : Π (a : ob), comp2 !ID2 !ID2 = ID2 a) (p : hom1 = hom2) (q : p ▹ comp1 = comp2) (r : p ▹ ID1 = ID2) : - precategory.mk hom1 homH1 comp1 ID1 assoc1 id_left1 id_right1 - = precategory.mk hom2 homH2 comp2 ID2 assoc2 id_left2 id_right2 := + precategory.mk' hom1 comp1 ID1 assoc1 assoc1' id_left1 id_right1 id_id1 homH1 + = precategory.mk' hom2 comp2 ID2 assoc2 assoc2' id_left2 id_right2 id_id2 homH2 := begin cases p, cases q, cases r, - assert PhomH : homH1 = homH2, - apply is_hprop.elim, - cases PhomH, - apply (ap0111 (precategory.mk hom2 homH1 comp2 ID2)), - repeat - (apply @is_hprop.elim; - repeat (apply is_hprop_pi; intros); - apply is_trunc_eq) + apply (ap0111111 (precategory.mk' hom2 comp2 ID2)), + repeat (apply is_hprop.elim), end definition precategory_eq_mk' (ob : Type) @@ -214,8 +237,8 @@ namespace category (r : transport (λ x, Π a, x a a) (eq_of_homotopy (λ (x : ob), eq_of_homotopy (λ (x_1 : ob), p x x_1))) ID1 = ID2) : - precategory.mk hom1 homH1 comp1 ID1 assoc1 id_left1 id_right1 - = precategory.mk hom2 homH2 comp2 ID2 assoc2 id_left2 id_right2 := + precategory.mk hom1 comp1 ID1 assoc1 id_left1 id_right1 + = precategory.mk hom2 comp2 ID2 assoc2 id_left2 id_right2 := begin fapply precategory_eq_mk, apply eq_of_homotopy, intros, @@ -227,7 +250,7 @@ namespace category definition Precategory_eq_mk (C D : Precategory) (p : carrier C = carrier D) - (q : p ▹ (Precategory.struct C) = Precategory.struct D) : C = D := + (q : p ▹ (Precategory.struct C) = Precategory.struct D) : C = D := begin cases C, cases D, cases p, cases q, diff --git a/hott/algebra/precategory/constructions.hlean b/hott/algebra/precategory/constructions.hlean index e0ffa12dbf..94efd9b3d0 100644 --- a/hott/algebra/precategory/constructions.hlean +++ b/hott/algebra/precategory/constructions.hlean @@ -17,13 +17,15 @@ namespace category namespace opposite definition opposite [reducible] {ob : Type} (C : precategory ob) : precategory ob := - precategory.mk (λ a b, hom b a) - (λ a b, !homH) - (λ a b c f g, g ∘ f) - (λ a, id) - (λ a b c d f g h, !assoc⁻¹) - (λ a b f, !id_right) - (λ a b f, !id_left) + precategory.mk' (λ a b, hom b a) + (λ a b c f g, g ∘ f) + (λ a, id) + (λ a b c d f g h, !assoc') + (λ a b c d f g h, !assoc) + (λ a b f, !id_right) + (λ a b f, !id_left) + (λ a, !id_id) + (λ a b, !is_hset_hom) definition Opposite [reducible] (C : Precategory) : Precategory := precategory.Mk (opposite C) @@ -31,22 +33,10 @@ namespace category variables {C : Precategory} {a b c : C} - set_option apply.class_instance false -- disable class instance resolution in the apply tactic - definition compose_op {f : hom a b} {g : hom b c} : f ∘op g = g ∘ f := idp - -- TODO: Decide whether just to use funext for this theorem or - -- take the trick they use in Coq-HoTT, and introduce a further - -- axiom in the definition of precategories that provides thee - -- symmetric associativity proof. definition opposite_opposite' {ob : Type} (C : precategory ob) : opposite (opposite C) = C := - begin - apply (precategory.rec_on C), intros [hom', homH', comp', ID', assoc', id_left', id_right'], - apply (ap (λassoc'', precategory.mk hom' @homH' comp' ID' assoc'' id_left' id_right')), - repeat (apply eq_of_homotopy ; intros ), - apply ap, - apply (@is_hset.elim), apply !homH', - end + by cases C; apply idp definition opposite_opposite : Opposite (Opposite C) = C := (ap (Precategory.mk C) (opposite_opposite' C)) ⬝ !Precategory.eta @@ -94,7 +84,6 @@ namespace category definition precategory_prod [reducible] {obC obD : Type} (C : precategory obC) (D : precategory obD) : 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, (id, id)) (λ a b c d h g f, pair_eq !assoc !assoc ) @@ -141,7 +130,6 @@ namespace category definition precategory_hset [reducible] : precategory hset := precategory.mk (λx y : hset, x → y) - _ (λx y z g f a, g (f a)) (λx a, a) (λx y z w h g f, eq_of_homotopy (λa, idp)) @@ -156,7 +144,6 @@ namespace category definition precategory_functor [instance] [reducible] (D C : Precategory) : precategory (functor C D) := precategory.mk (λa b, nat_trans 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) @@ -228,12 +215,12 @@ namespace category definition naturality_iso {c c' : C} (f : c ⟶ c') : G f = η c' ∘ F f ∘ (η c)⁻¹ := calc G f = (G f ∘ η c) ∘ (η c)⁻¹ : comp_inverse_cancel_right - ... = (η c' ∘ F f) ∘ (η c)⁻¹ : {naturality η f} + ... = (η c' ∘ F f) ∘ (η c)⁻¹ : by rewrite naturality ... = η c' ∘ F f ∘ (η c)⁻¹ : assoc definition naturality_iso' {c c' : C} (f : c ⟶ c') : (η c')⁻¹ ∘ G f ∘ η c = F f := calc - (η c')⁻¹ ∘ G f ∘ η c = (η c')⁻¹ ∘ η c' ∘ F f : {naturality η f} + (η c')⁻¹ ∘ G f ∘ η c = (η c')⁻¹ ∘ η c' ∘ F f : by rewrite naturality ... = F f : inverse_comp_cancel_left omit isoη @@ -243,7 +230,7 @@ namespace category (@componentwise_is_iso _ _ _ _ (to_hom η) (struct η) c) definition componentwise_iso_id (c : C) : componentwise_iso (iso.refl F) c = iso.refl (F c) := - iso.eq_mk (idpath id) + iso.eq_mk (idpath (ID (F c))) definition componentwise_iso_iso_of_eq (p : F = G) (c : C) : componentwise_iso (iso_of_eq p) c = iso_of_eq (ap010 to_fun_ob p c) := diff --git a/hott/algebra/precategory/functor.hlean b/hott/algebra/precategory/functor.hlean index 3b8c06335f..d7de408976 100644 --- a/hott/algebra/precategory/functor.hlean +++ b/hott/algebra/precategory/functor.hlean @@ -149,21 +149,11 @@ namespace functor apply idp}, end - set_option apply.class_instance false - protected definition is_hset_functor - [HD : is_hset D] : is_hset (functor C D) := - begin - apply is_trunc_is_equiv_closed, apply equiv.to_is_equiv, - apply sigma_char, - apply is_trunc_sigma, apply is_trunc_pi, intros, exact HD, intro F, - apply is_trunc_sigma, apply is_trunc_pi, intro a, - {apply is_trunc_pi, intro b, - apply is_trunc_pi, intro c, apply !homH}, - intro H, apply is_trunc_prod, - {apply is_trunc_pi, intro a, - apply is_trunc_eq, apply is_trunc_succ, apply !homH}, - {repeat (apply is_trunc_pi; intros), - apply is_trunc_eq, apply is_trunc_succ, apply !homH}, + section + local attribute precategory.is_hset_hom [priority 1001] + protected theorem is_hset_functor [instance] + [HD : is_hset D] : is_hset (functor C D) := + by apply is_trunc_equiv_closed; apply sigma_char end definition functor_mk_eq'_idp (F : C → D) (H : Π(a b : C), hom a b → hom (F a) (F b)) diff --git a/hott/algebra/precategory/nat_trans.hlean b/hott/algebra/precategory/nat_trans.hlean index 11320a338a..ada3767ec3 100644 --- a/hott/algebra/precategory/nat_trans.hlean +++ b/hott/algebra/precategory/nat_trans.hlean @@ -77,16 +77,8 @@ namespace nat_trans apply is_hprop.elim, end - set_option apply.class_instance false - 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, - apply is_trunc_pi, intro a, exact (@homH (Precategory.carrier D) _ (F a) (G a)), - intro η, apply is_trunc_pi, intro a, - apply is_trunc_pi, intro b, apply is_trunc_pi, intro f, - apply is_trunc_eq, apply is_trunc_succ, exact (@homH (Precategory.carrier D) _ (F a) (G b)), - end + definition is_hset_nat_trans [instance] : is_hset (F ⟹ G) := + by apply is_trunc_is_equiv_closed; apply (equiv.to_is_equiv !sigma_char) definition nat_trans_functor_compose [reducible] (η : G ⟹ H) (F : E ⇒ C) : G ∘f F ⟹ H ∘f F := nat_trans.mk diff --git a/hott/algebra/precategory/strict.hlean b/hott/algebra/precategory/strict.hlean index 4e75752c8b..9b734f2322 100644 --- a/hott/algebra/precategory/strict.hlean +++ b/hott/algebra/precategory/strict.hlean @@ -34,12 +34,11 @@ namespace category definition precat_strict_precat : precategory Strict_precategory := precategory.mk (λ a b, functor a b) - (λ a b, @functor.is_hset_functor a b _) - (λ a b c g f, functor.compose g f) - (λ a, functor.id) - (λ a b c d h g f, !functor.assoc) - (λ a b f, !functor.id_left) - (λ a b f, !functor.id_right) + (λ a b c g f, functor.compose g f) + (λ a, functor.id) + (λ a b c d h g f, !functor.assoc) + (λ a b f, !functor.id_left) + (λ a b f, !functor.id_right) definition Precat_of_strict_precats := precategory.Mk precat_strict_precat diff --git a/hott/algebra/precategory/yoneda.hlean b/hott/algebra/precategory/yoneda.hlean index 071c39631d..562acab04b 100644 --- a/hott/algebra/precategory/yoneda.hlean +++ b/hott/algebra/precategory/yoneda.hlean @@ -150,8 +150,8 @@ namespace functor from calc to_fun_hom (functor_curry (functor_uncurry G) c) g = to_fun_hom (G c) g ∘ natural_map (to_fun_hom G (ID c)) d : by esimp - ... = to_fun_hom (G c) g ∘ natural_map (ID (G c)) d - : by rewrite respect_id + ... = to_fun_hom (G c) g ∘ natural_map (ID (G c)) d : by rewrite respect_id + ... = to_fun_hom (G c) g ∘ id : idp ... = to_fun_hom (G c) g : id_right} end diff --git a/hott/arity.hlean b/hott/arity.hlean index 55f226ee62..b317cc1fd8 100644 --- a/hott/arity.hlean +++ b/hott/arity.hlean @@ -10,7 +10,7 @@ Theorems about functions with multiple arguments variables {A U V W X Y Z : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type} {E : Πa b c, D a b c → Type} -variables {a a' : A} {u u' : U} {v v' : V} {w w' : W} {x x' x'' : X} {y y' : Y} +variables {a a' : A} {u u' : U} {v v' : V} {w w' : W} {x x' x'' : X} {y y' : Y} {z z' : Z} {b : B a} {b' : B a'} {c : C a b} {c' : C a' b'} {d : D a b c} {d' : D a' b' c'} @@ -59,6 +59,16 @@ namespace eq : f u v w x = f u' v' w' x' := eq.rec_on Hu (ap0111 (f u) Hv Hw Hx) + definition ap011111 (f : U → V → W → X → Y → Z) + (Hu : u = u') (Hv : v = v') (Hw : w = w') (Hx : x = x') (Hy : y = y') + : f u v w x y = f u' v' w' x' y' := + eq.rec_on Hu (ap01111 (f u) Hv Hw Hx Hy) + + definition ap0111111 (f : U → V → W → X → Y → Z → A) + (Hu : u = u') (Hv : v = v') (Hw : w = w') (Hx : x = x') (Hy : y = y') (Hz : z = z') + : f u v w x y z = f u' v' w' x' y' z' := + eq.rec_on Hu (ap011111 (f u) Hv Hw Hx Hy Hz) + definition ap010 (f : X → Πa, B a) (Hx : x = x') : f x ∼ f x' := λa, eq.rec_on Hx idp diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index 87c9fd9cd7..be277d7856 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -5,11 +5,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Module: init.trunc Authors: Jeremy Avigad, Floris van Doorn -Ported from Coq HoTT. +Definition of is_trunc (n-truncatedness) -TODO: can we replace some definitions with a hprop as codomain by theorems? +Ported from Coq HoTT. -/ +--TODO: can we replace some definitions with a hprop as codomain by theorems? + prelude import .logic .equiv .types open eq nat sigma unit @@ -87,7 +89,8 @@ namespace is_trunc : is_trunc n.+1 A := is_trunc.mk (λ x y, !is_trunc.to_internal) - definition is_trunc_eq (n : trunc_index) [H : is_trunc (n.+1) A] (x y : A) : is_trunc n (x = y) := + definition is_trunc_eq [instance] [priority 1200] + (n : trunc_index) [H : is_trunc (n.+1) A] (x y : A) : is_trunc n (x = y) := is_trunc.mk (!is_trunc.to_internal x y) /- contractibility -/ @@ -119,7 +122,7 @@ namespace is_trunc [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)) + (λ n IH A (H : is_trunc (n.+1) A), @is_trunc_succ_intro _ _ (λ x y, IH _ _)) A H --in the proof the type of H is given explicitly to make it available for class inference @@ -136,7 +139,7 @@ namespace is_trunc λm IHm n, trunc_index.rec_on n (λA Hnm Hn, @is_trunc_succ A m (IHm -2 A star Hn)) (λn IHn A Hnm (Hn : is_trunc n.+1 A), - @is_trunc_succ_intro A m (λx y, IHm n (x = y) (trunc_index.le_of_succ_le_succ Hnm) !is_trunc_eq)), + @is_trunc_succ_intro A m (λx y, IHm n (x = y) (trunc_index.le_of_succ_le_succ Hnm) _)), trunc_index.rec_on m base step n A Hnm Hn -- the following cannot be instances in their current form, because they are looping @@ -154,7 +157,7 @@ namespace is_trunc /- hprops -/ definition is_hprop.elim [H : is_hprop A] (x y : A) : x = y := - @center _ !is_trunc_eq + !center definition is_contr_of_inhabited_hprop {A : Type} [H : is_hprop A] (x : A) : is_contr A := is_contr.mk x (λy, !is_hprop.elim) @@ -175,7 +178,7 @@ namespace is_trunc @is_trunc_succ_intro _ _ (λ x y, is_hprop.mk (H x y)) definition is_hset.elim [H : is_hset A] ⦃x y : A⦄ (p q : x = y) : p = q := - @is_hprop.elim _ !is_trunc_eq p q + !is_hprop.elim /- instances -/ @@ -226,7 +229,7 @@ namespace is_trunc trunc_index.rec_on n (λA (HA : is_contr A) B f (H : is_equiv f), !is_contr_is_equiv_closed) (λn IH A (HA : is_trunc n.+1 A) B f (H : is_equiv f), @is_trunc_succ_intro _ _ (λ x y : B, - IH (f⁻¹ x = f⁻¹ y) !is_trunc_eq (x = y) (ap f⁻¹)⁻¹ !is_equiv_inv)) + IH (f⁻¹ x = f⁻¹ y) _ (x = y) (ap f⁻¹)⁻¹ !is_equiv_inv)) A HA B f H definition is_trunc_equiv_closed (n : trunc_index) (f : A ≃ B) [HA : is_trunc n A] diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean index 92fa528fd0..806216d0b3 100644 --- a/hott/types/equiv.hlean +++ b/hott/types/equiv.hlean @@ -78,8 +78,8 @@ namespace is_equiv ... ≃ (Σ(u : Σ(g : B → A), f ∘ g ∼ id), Σ(η : u.1 ∘ f ∼ id), Π(a : A), u.2 (f a) = ap f (η a)) : {sigma_assoc_equiv (λu, Σ(η : u.1 ∘ f ∼ id), Π(a : A), u.2 (f a) = ap f (η a))} - local attribute is_contr_right_inverse [instance] - local attribute is_contr_right_coherence [instance] + local attribute is_contr_right_inverse [instance] [priority 1600] + local attribute is_contr_right_coherence [instance] [priority 1600] theorem is_hprop_is_equiv [instance] : is_hprop (is_equiv f) := is_hprop_of_imp_is_contr (λ(H : is_equiv f), is_trunc_equiv_closed -2 (equiv.symm !sigma_char')) diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean index 0db46e6191..4617637df4 100644 --- a/hott/types/pi.hlean +++ b/hott/types/pi.hlean @@ -154,7 +154,7 @@ namespace pi /- Truncatedness: any dependent product of n-types is an n-type -/ open is_trunc - definition is_trunc_pi [instance] (B : A → Type) (n : trunc_index) + definition is_trunc_pi (B : A → Type) (n : trunc_index) [H : ∀a, is_trunc n (B a)] : is_trunc n (Πa, B a) := begin reverts [B, H], @@ -173,8 +173,8 @@ namespace pi show is_trunc n (f a = g a), from is_trunc_eq n (f a) (g a)} end - - definition is_trunc_eq_pi [instance] (n : trunc_index) (f g : Πa, B a) + local attribute is_trunc_pi [instance] + definition is_trunc_eq_pi [instance] [priority 500] (n : trunc_index) (f g : Πa, B a) [H : ∀a, is_trunc n (f a = g a)] : is_trunc n (f = g) := begin apply is_trunc_equiv_closed, apply equiv.symm, @@ -195,4 +195,4 @@ namespace pi end pi -attribute pi.is_trunc_pi [instance] +attribute pi.is_trunc_pi [instance] [priority 1510] diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index a516a9d472..3cf7e7db7f 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -383,10 +383,10 @@ namespace sigma end sigma -attribute sigma.is_trunc_sigma [instance] +attribute sigma.is_trunc_sigma [instance] [priority 1505] open is_trunc sigma prod /- truncatedness -/ -definition prod.is_trunc_prod [instance] (A B : Type) (n : trunc_index) +definition prod.is_trunc_prod [instance] [priority 1510] (A B : Type) (n : trunc_index) [HA : is_trunc n A] [HB : is_trunc n B] : is_trunc n (A × B) := is_trunc.is_trunc_equiv_closed n !equiv_prod