diff --git a/hott/algebra/category/adjoint.hlean b/hott/algebra/category/adjoint.hlean index 9af235cf0..73f4a1724 100644 --- a/hott/algebra/category/adjoint.hlean +++ b/hott/algebra/category/adjoint.hlean @@ -2,92 +2,111 @@ Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Module: algebra.category.adjoint +Module: algebra.precategory.adjoint Authors: Floris van Doorn -/ -import .constructions.functor +import algebra.category.constructions .constructions types.function arity -open category functor nat_trans eq is_trunc iso equiv prod - -variables {C D : Precategory} {F : C ⇒ D} - --- structure adjoint (F : C ⇒ D) (G : D ⇒ C) := --- (unit : functor.id ⟹ G ∘f F) -- η --- (counit : F ∘f G ⟹ functor.id) -- ε --- (H : (counit ∘nf F) ∘n (nat_trans_of_eq !functor.assoc) ∘n (F ∘fn unit) --- = nat_trans_of_eq !functor.comp_id_eq_id_comp) --- (K : (G ∘fn counit) ∘n (nat_trans_of_eq !functor.assoc⁻¹) ∘n (unit ∘nf G) --- = nat_trans_of_eq !functor.comp_id_eq_id_comp⁻¹) - --- structure is_left_adjoint (F : C ⇒ D) := --- (right_adjoint : D ⇒ C) -- G --- (is_adjoint : adjoint F right_adjoint) - -structure is_left_adjoint (F : C ⇒ D) := - (right_adjoint : D ⇒ C) -- G - (unit : functor.id ⟹ right_adjoint ∘f F) -- η - (counit : F ∘f right_adjoint ⟹ functor.id) -- ε - (H : (counit ∘nf F) ∘n (nat_trans_of_eq !functor.assoc) ∘n (F ∘fn unit) - = nat_trans_of_eq !functor.comp_id_eq_id_comp) - (K : (right_adjoint ∘fn counit) ∘n (nat_trans_of_eq !functor.assoc⁻¹) ∘n (unit ∘nf right_adjoint) - = nat_trans_of_eq !functor.comp_id_eq_id_comp⁻¹) - -structure is_equivalence (F : C ⇒ D) extends is_left_adjoint F := - mk' :: - (is_iso_unit : is_iso unit) - (is_iso_counit : is_iso counit) - -structure equivalence (C D : Precategory) := - (to_functor : C ⇒ D) - (struct : is_equivalence to_functor) - ---TODO: review and change ---TODO: make some or all of these structures? -definition faithful (F : C ⇒ D) := -Π⦃c c' : C⦄, (Π(f f' : c ⟶ c'), to_fun_hom F f = to_fun_hom F f' → f = f') - -definition full (F : C ⇒ D) := Π⦃c c' : C⦄ (g : F c ⟶ F c'), Σ(f : c ⟶ c'), F f = g --merely - -definition fully_faithful (F : C ⇒ D) := Π⦃c c' : C⦄, is_equiv (@to_fun_hom _ _ F c c') - -definition split_essentially_surjective (F : C ⇒ D) := -Π⦃d : D⦄, Σ(c : C), F c ≅ d - -definition essentially_surjective (F : C ⇒ D) := -Π⦃d : D⦄, Σ(c : C), F c ≅ d --merely - -definition is_weak_equivalence (F : C ⇒ D) := -fully_faithful F × essentially_surjective F - -definition is_isomorphism (F : C ⇒ D) := -fully_faithful F × is_equiv (to_fun_ob F) - -structure isomorphism (C D : Precategory) := - (to_functor : C ⇒ D) - (struct : is_isomorphism to_functor) +open category functor nat_trans eq is_trunc iso equiv prod trunc function namespace category + variables {C D : Precategory} {F : C ⇒ D} + -- do we want to have a structure "is_adjoint" and define + -- structure is_left_adjoint (F : C ⇒ D) := + -- (right_adjoint : D ⇒ C) -- G + -- (is_adjoint : adjoint F right_adjoint) + + structure is_left_adjoint [class] (F : C ⇒ D) := + (G : D ⇒ C) + (η : functor.id ⟹ G ∘f F) + (ε : F ∘f G ⟹ functor.id) + (H : Π(c : C), (ε (F c)) ∘ (F (η c)) = ID (F c)) + (K : Π(d : D), (G (ε d)) ∘ (η (G d)) = ID (G d)) + + abbreviation right_adjoint := @is_left_adjoint.G + abbreviation unit := @is_left_adjoint.η + abbreviation counit := @is_left_adjoint.ε + + -- structure is_left_adjoint [class] (F : C ⇒ D) := + -- (right_adjoint : D ⇒ C) -- G + -- (unit : functor.id ⟹ right_adjoint ∘f F) -- η + -- (counit : F ∘f right_adjoint ⟹ functor.id) -- ε + -- (H : Π(c : C), (counit (F c)) ∘ (F (unit c)) = ID (F c)) + -- (K : Π(d : D), (right_adjoint (counit d)) ∘ (unit (right_adjoint d)) = ID (right_adjoint d)) + + structure is_equivalence [class] (F : C ⇒ D) extends is_left_adjoint F := + mk' :: + (is_iso_unit : is_iso η) + (is_iso_counit : is_iso ε) + + structure equivalence (C D : Precategory) := + (to_functor : C ⇒ D) + (struct : is_equivalence to_functor) + + --TODO: review and change + --TODO: make some or all of these structures? + definition faithful (F : C ⇒ D) := + Π⦃c c' : C⦄ (f f' : c ⟶ c'), F f = F f' → f = f' + + definition full (F : C ⇒ D) := Π⦃c c' : C⦄ (g : F c ⟶ F c'), ∃(f : c ⟶ c'), F f = g + + definition fully_faithful [reducible] (F : C ⇒ D) := Π⦃c c' : C⦄, is_equiv (@to_fun_hom _ _ F c c') + + definition split_essentially_surjective (F : C ⇒ D) := + Π⦃d : D⦄, Σ(c : C), F c ≅ d + + definition essentially_surjective (F : C ⇒ D) := + Π⦃d : D⦄, ∃(c : C), F c ≅ d + + definition is_weak_equivalence (F : C ⇒ D) := + fully_faithful F × essentially_surjective F + + definition is_isomorphism (F : C ⇒ D) := + fully_faithful F × is_equiv (to_fun_ob F) + + structure isomorphism (C D : Precategory) := + (to_functor : C ⇒ D) + (struct : is_isomorphism to_functor) -- infix `⊣`:55 := adjoint - infix `⋍`:25 := equivalence -- \backsimeq - infix `≌`:25 := isomorphism -- \backcong - --TODO: add shortcuts for Σ⋍≌▹ + infix `⋍`:25 := equivalence -- \backsimeq or \equiv + infix `≌`:25 := isomorphism -- \backcong or \iso definition is_hprop_is_left_adjoint {C : Category} {D : Precategory} (F : C ⇒ D) : is_hprop (is_left_adjoint F) := - sorry + begin + apply is_hprop.mk, + intros [G, G'], cases G with [G, η, ε, H, K], cases G' with [G', η', ε', H', K'], + fapply (apd011111 is_left_adjoint.mk), + { fapply functor_eq, + { intro d, apply eq_of_iso, fapply iso.MK, + { exact (G' (ε d) ∘ η' (G d))}, + { exact (G (ε' d) ∘ η (G' d))}, + { apply sorry /-rewrite [assoc, -{((G (ε' d)) ∘ (η (G' d))) ∘ (G' (ε d))}(assoc)],-/ +-- apply concat, apply (ap (λc, c ∘ η' _)), rewrite -assoc, apply idp +}, +--/-rewrite [-nat_trans.assoc]-/apply sorry +---assoc (G (ε' d)) (η (G' d)) (G' (ε d)) + { apply sorry}}, + { apply sorry}, +}, + { apply sorry}, + { apply sorry}, + { apply is_hprop.elim}, + { apply is_hprop.elim}, + end definition is_equivalence.mk (F : C ⇒ D) (G : D ⇒ C) (η : G ∘f F ≅ functor.id) (ε : F ∘f G ≅ functor.id) : is_equivalence F := sorry definition full_of_fully_faithful (H : fully_faithful F) : full F := - sorry + sorry --λc c' g, trunc.elim _ _ definition faithful_of_fully_faithful (H : fully_faithful F) : faithful F := - sorry + λc c' f f' p, is_injective_of_is_embedding p definition fully_faithful_of_full_of_faithful (H : faithful F) (K : full F) : fully_faithful F := sorry @@ -118,7 +137,7 @@ namespace category sorry definition is_isomorphism_equiv2 (F : C ⇒ D) : is_equivalence F - ≃ Σ/-MERELY-/(G : D ⇒ C), functor.id = G ∘f F × F ∘f G = functor.id := + ≃ ∃(G : D ⇒ C), functor.id = G ∘f F × F ∘f G = functor.id := sorry definition is_equivalence_of_isomorphism (H : is_isomorphism F) : is_equivalence F := diff --git a/hott/algebra/category/constructions/functor.hlean b/hott/algebra/category/constructions/functor.hlean index 0ecfecc7b..660c3377d 100644 --- a/hott/algebra/category/constructions/functor.hlean +++ b/hott/algebra/category/constructions/functor.hlean @@ -159,14 +159,20 @@ namespace category end functor - definition Category_functor_of_precategory (D : Category) (C : Precategory) : Category := - category.MK (D ^c C) (functor.is_univalent D C) + definition category_functor [instance] (D : Category) (C : Precategory) + : category (D ^c C) := + category.mk (D ^c C) (functor.is_univalent D C) - definition Category_functor (D : Category) (C : Category) : Category := - Category_functor_of_precategory D C + definition Category_functor (D : Category) (C : Precategory) : Category := + category.Mk (D ^c C) !category_functor + + --this definition is only useful if the exponent is a category, + -- and the elaborator has trouble with inserting the coercion + definition Category_functor' (D C : Category) : Category := + Category_functor D C namespace ops - infixr `^c2`:35 := Category_functor_of_precategory + infixr `^c2`:35 := Category_functor end ops diff --git a/hott/algebra/category/default.hlean b/hott/algebra/category/default.hlean new file mode 100644 index 000000000..9db29ece4 --- /dev/null +++ b/hott/algebra/category/default.hlean @@ -0,0 +1,9 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: algebra.category.default +Authors: Floris van Doorn +-/ + +import .category .strict .groupoid .constructions diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean index bf7965446..20fe815ea 100644 --- a/hott/algebra/category/iso.hlean +++ b/hott/algebra/category/iso.hlean @@ -230,11 +230,11 @@ namespace iso 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) + 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) := diff --git a/hott/algebra/category/nat_trans.hlean b/hott/algebra/category/nat_trans.hlean index b703e93af..49bf05c74 100644 --- a/hott/algebra/category/nat_trans.hlean +++ b/hott/algebra/category/nat_trans.hlean @@ -93,12 +93,16 @@ namespace nat_trans ... = F (η b ∘ G f) : by rewrite (naturality η f) ... = F (η b) ∘ F (G f) : by rewrite respect_comp) - infixr `∘nf`:60 := nat_trans_functor_compose - infixr `∘fn`:60 := functor_nat_trans_compose + infixr `∘nf`:62 := nat_trans_functor_compose + infixr `∘fn`:62 := functor_nat_trans_compose - definition functor_nat_trans_compose_commute (η : F ⟹ G) (θ : F' ⟹ G') + definition nf_fn_eq_fn_nf_pt (η : F ⟹ G) (θ : F' ⟹ G') (c : C) + : (θ (G c)) ∘ (F' (η c)) = (G' (η c)) ∘ (θ (F c)) := + (naturality θ (η c))⁻¹ + + definition nf_fn_eq_fn_nf (η : F ⟹ G) (θ : F' ⟹ G') : (θ ∘nf G) ∘n (F' ∘fn η) = (G' ∘fn η) ∘n (θ ∘nf F) := - nat_trans_eq (λc, (naturality θ (η c))⁻¹) + nat_trans_eq (λc, !nf_fn_eq_fn_nf_pt) definition fn_n_distrib (F' : D ⇒ E) (η : G ⟹ H) (θ : F ⟹ G) : F' ∘fn (η ∘n θ) = (F' ∘fn η) ∘n (F' ∘fn θ) := diff --git a/hott/arity.hlean b/hott/arity.hlean index 965115872..552ea33ab 100644 --- a/hott/arity.hlean +++ b/hott/arity.hlean @@ -14,6 +14,7 @@ variables {a a' : A} {u u' : U} {v v' : V} {w w' : W} {x x' x'' : X} {y y' : Y} {b : B a} {b' : B a'} {c : C a b} {c' : C a' b'} {d : D a b c} {d' : D a' b' c'} + {e : E a b c d} {e' : E a' b' c' d'} namespace eq /- @@ -49,48 +50,54 @@ namespace eq notation f `∼3`:50 g := homotopy3 f g definition ap011 (f : U → V → W) (Hu : u = u') (Hv : v = v') : f u v = f u' v' := - eq.rec_on Hu (ap (f u) Hv) + by cases Hu; exact (ap (f u) Hv) definition ap0111 (f : U → V → W → X) (Hu : u = u') (Hv : v = v') (Hw : w = w') : f u v w = f u' v' w' := - eq.rec_on Hu (ap011 (f u) Hv Hw) + by cases Hu; exact (ap011 (f u) Hv Hw) definition ap01111 (f : U → V → W → X → Y) (Hu : u = u') (Hv : v = v') (Hw : w = w') (Hx : x = x') : f u v w x = f u' v' w' x' := - eq.rec_on Hu (ap0111 (f u) Hv Hw Hx) + by cases Hu; exact (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) + by cases Hu; exact (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) + by cases Hu; exact (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 + λa, by cases Hx; exact idp definition ap0100 (f : X → Πa b, C a b) (Hx : x = x') : f x ∼2 f x' := - λa b, eq.rec_on Hx idp + λa b, by cases Hx; exact idp definition ap01000 (f : X → Πa b c, D a b c) (Hx : x = x') : f x ∼3 f x' := - λa b c, eq.rec_on Hx idp + λa b c, by cases Hx; exact idp definition apd011 (f : Πa, B a → Z) (Ha : a = a') (Hb : (Ha ▹ b) = b') : f a b = f a' b' := - eq.rec_on Hb (eq.rec_on Ha idp) + by cases Ha; cases Hb; exact idp definition apd0111 (f : Πa b, C a b → Z) (Ha : a = a') (Hb : (Ha ▹ b) = b') (Hc : apd011 C Ha Hb ▹ c = c') : f a b c = f a' b' c' := - eq.rec_on Hc (eq.rec_on Hb (eq.rec_on Ha idp)) + by cases Ha; cases Hb; cases Hc; exact idp definition apd01111 (f : Πa b c, D a b c → Z) (Ha : a = a') (Hb : (Ha ▹ b) = b') (Hc : apd011 C Ha Hb ▹ c = c') (Hd : apd0111 D Ha Hb Hc ▹ d = d') : f a b c d = f a' b' c' d' := - eq.rec_on Hd (eq.rec_on Hc (eq.rec_on Hb (eq.rec_on Ha idp))) + by cases Ha; cases Hb; cases Hc; cases Hd; exact idp + + definition apd011111 (f : Πa b c d, E a b c d → Z) (Ha : a = a') (Hb : (Ha ▹ b) = b') + (Hc : apd011 C Ha Hb ▹ c = c') (Hd : apd0111 D Ha Hb Hc ▹ d = d') + (He : apd01111 E Ha Hb Hc Hd ▹ e = e') + : f a b c d e = f a' b' c' d' e' := + by cases Ha; cases Hb; cases Hc; cases Hd; cases He; exact idp definition apd100 {f g : Πa b, C a b} (p : f = g) : f ∼2 g := λa b, apd10 (apd10 p a) b diff --git a/hott/hit/circle.hlean b/hott/hit/circle.hlean index c7ed9ef23..b51938a1c 100644 --- a/hott/hit/circle.hlean +++ b/hott/hit/circle.hlean @@ -91,10 +91,13 @@ namespace circle eq_inv_tr_of_tr_eq (tr_eq_of_eq_inv_tr q) = q := by cases p; exact idp + definition con_refl {A : Type} {x y : A} (p : x = y) : p ⬝ refl _ = p := + eq.rec_on p idp + theorem rec_loop {P : circle → Type} (Pbase : P base) (Ploop : loop ▹ Pbase = Pbase) : apd (rec Pbase Ploop) loop = Ploop := begin - rewrite [↑loop,apd_con,↑rec,↑rec2_on,↑base,rec2_seg1,apd_inv,rec2_seg2], + rewrite [↑loop,apd_con,↑rec,↑rec2_on,↑base,rec2_seg1,apd_inv,rec2_seg2,↑ap], --con_idp should work here apply concat, apply (ap (λx, x ⬝ _)), apply con_idp, esimp, rewrite [rec_loop_helper,inv_con_inv_left], apply con_inv_cancel_left diff --git a/hott/hit/trunc.hlean b/hott/hit/trunc.hlean index d1935e79e..ffca2a768 100644 --- a/hott/hit/trunc.hlean +++ b/hott/hit/trunc.hlean @@ -31,4 +31,106 @@ namespace trunc because the universe is generally not a set -/ + --export is_trunc + + variables {X Y Z : Type} {P : X → Type} (A B : Type) (n : trunc_index) + + local attribute is_trunc_eq [instance] + + definition is_equiv_tr [instance] [H : is_trunc n A] : is_equiv (@tr n A) := + adjointify _ + (trunc.rec id) + (λaa, trunc.rec_on aa (λa, idp)) + (λa, idp) + + definition equiv_trunc [H : is_trunc n A] : A ≃ trunc n A := + equiv.mk tr _ + + definition is_trunc_of_is_equiv_tr [H : is_equiv (@tr n A)] : is_trunc n A := + is_trunc_is_equiv_closed n tr⁻¹ + + definition untrunc_of_is_trunc [reducible] [H : is_trunc n A] : trunc n A → A := + tr⁻¹ + + /- Functoriality -/ + definition trunc_functor (f : X → Y) : trunc n X → trunc n Y := + λxx, trunc.rec_on xx (λx, tr (f x)) +-- by intro xx; apply (trunc.rec_on xx); intro x; exact (tr (f x)) +-- by intro xx; fapply (trunc.rec_on xx); intro x; exact (tr (f x)) +-- by intro xx; exact (trunc.rec_on xx (λx, (tr (f x)))) + + definition trunc_functor_compose (f : X → Y) (g : Y → Z) + : trunc_functor n (g ∘ f) ∼ trunc_functor n g ∘ trunc_functor n f := + λxx, trunc.rec_on xx (λx, idp) + + definition trunc_functor_id : trunc_functor n (@id A) ∼ id := + λxx, trunc.rec_on xx (λx, idp) + + definition is_equiv_trunc_functor (f : X → Y) [H : is_equiv f] : is_equiv (trunc_functor n f) := + adjointify _ + (trunc_functor n f⁻¹) + (λyy, trunc.rec_on yy (λy, ap tr !right_inv)) + (λxx, trunc.rec_on xx (λx, ap tr !left_inv)) + + section + open prod.ops + definition trunc_prod_equiv : trunc n (X × Y) ≃ trunc n X × trunc n Y := + sorry + -- equiv.MK (λpp, trunc.rec_on pp (λp, (tr p.1, tr p.2))) + -- (λp, trunc.rec_on p.1 (λx, trunc.rec_on p.2 (λy, tr (x,y)))) + -- sorry --(λp, trunc.rec_on p.1 (λx, trunc.rec_on p.2 (λy, idp))) + -- (λpp, trunc.rec_on pp (λp, prod.rec_on p (λx y, idp))) + + -- begin + -- fapply equiv.MK, + -- apply sorry, --{exact (λpp, trunc.rec_on pp (λp, (tr p.1, tr p.2)))}, + -- apply sorry, /-{intro p, cases p with (xx, yy), + -- apply (trunc.rec_on xx), intro x, + -- apply (trunc.rec_on yy), intro y, exact (tr (x,y))},-/ + -- apply sorry, /-{intro p, cases p with (xx, yy), + -- apply (trunc.rec_on xx), intro x, + -- apply (trunc.rec_on yy), intro y, apply idp},-/ + -- apply sorry --{intro pp, apply (trunc.rec_on pp), intro p, cases p, apply idp}, + -- end + end + + /- Propositional truncation -/ + + -- should this live in hprop? + definition merely [reducible] (A : Type) : Type := trunc -1 A + + notation `||`:max A `||`:0 := merely A + notation `∥`:max A `∥`:0 := merely A + + definition Exists [reducible] (P : X → Type) : Type := ∥ sigma P ∥ + definition or [reducible] (A B : Type) : Type := ∥ A ⊎ B ∥ + + notation `exists` binders `,` r:(scoped P, Exists P) := r + notation `∃` binders `,` r:(scoped P, Exists P) := r + notation A `\/` B := or A B + notation A ∨ B := or A B + + definition merely.intro [reducible] (a : A) : ∥ A ∥ := tr a + definition exists.intro [reducible] (x : X) (p : P x) : ∃x, P x := tr ⟨x, p⟩ + definition or.intro_left [reducible] (x : X) : X ∨ Y := tr (inl x) + definition or.intro_right [reducible] (y : Y) : X ∨ Y := tr (inr y) + + definition is_contr_of_merely_hprop [H : is_hprop A] (aa : merely A) : is_contr A := + is_contr_of_inhabited_hprop (trunc.rec_on aa id) + + section + open sigma.ops + definition trunc_sigma_equiv : trunc n (Σ x, P x) ≃ trunc n (Σ x, trunc n (P x)) := + equiv.MK (λpp, trunc.rec_on pp (λp, tr ⟨p.1, tr p.2⟩)) + (λpp, trunc.rec_on pp (λp, trunc.rec_on p.2 (λb, tr ⟨p.1, b⟩))) + (λpp, trunc.rec_on pp (λp, sigma.rec_on p (λa bb, trunc.rec_on bb (λb, by esimp)))) + (λpp, trunc.rec_on pp (λp, sigma.rec_on p (λa b, by esimp))) + + definition trunc_sigma_equiv_of_is_trunc [H : is_trunc n X] + : trunc n (Σ x, P x) ≃ Σ x, trunc n (P x) := + calc + trunc n (Σ x, P x) ≃ trunc n (Σ x, trunc n (P x)) : trunc_sigma_equiv + ... ≃ Σ x, trunc n (P x) : equiv.symm !equiv_trunc + end + end trunc diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index e049c4ccb..d440312a7 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -218,7 +218,6 @@ namespace is_equiv definition is_equiv_tr [instance] {A : Type} (P : A → Type) {x y : A} (p : x = y) : (is_equiv (transport P p)) := is_equiv.mk _ (transport P p⁻¹) (tr_inv_tr p) (inv_tr_tr p) (tr_inv_tr_lemma p) - end is_equiv open is_equiv diff --git a/hott/init/function.hlean b/hott/init/function.hlean index 7675901cf..f8562d30a 100644 --- a/hott/init/function.hlean +++ b/hott/init/function.hlean @@ -50,8 +50,6 @@ infixr ∘' := dcompose infixl on := on_fun infixr $ := app notation f `-[` op `]-` g := combine f op g --- Trick for using any binary function as infix operator -notation a `⟨` f `⟩` b := f a b end function diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index 450030aac..65a76a027 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -127,7 +127,7 @@ namespace is_trunc A H --in the proof the type of H is given explicitly to make it available for class inference - definition is_trunc_of_leq (A : Type) (n m : trunc_index) (Hnm : n ≤ m) + definition is_trunc_of_leq.{l} (A : Type.{l}) {n m : trunc_index} (Hnm : n ≤ m) [Hn : is_trunc n A] : is_trunc m A := have base : ∀k A, k ≤ -2 → is_trunc k A → (is_trunc -2 A), from λ k A, trunc_index.cases_on k @@ -149,11 +149,11 @@ namespace is_trunc definition is_trunc_succ_of_is_hprop (A : Type) (n : trunc_index) [H : is_hprop A] : is_trunc (n.+1) A := - is_trunc_of_leq A -1 (n.+1) star + is_trunc_of_leq A star definition is_trunc_succ_succ_of_is_hset (A : Type) (n : trunc_index) [H : is_hset A] : is_trunc (n.+2) A := - is_trunc_of_leq A nat.zero (n.+2) star + is_trunc_of_leq A star /- hprops -/ @@ -204,8 +204,12 @@ namespace is_trunc abbreviation hprop := -1-Type abbreviation hset := 0-Type - protected definition hprop.mk := @trunctype.mk -1 - protected definition hset.mk := @trunctype.mk (-1.+1) + protected abbreviation hprop.mk := @trunctype.mk -1 + protected abbreviation hset.mk := @trunctype.mk (-1.+1) + + protected abbreviation trunctype.mk' [parsing-only] (n : trunc_index) (A : Type) + [H : is_trunc n A] : n-Type := + trunctype.mk A H /- interaction with equivalences -/ @@ -234,10 +238,18 @@ namespace is_trunc IH (f⁻¹ x = f⁻¹ y) _ (x = y) (ap f⁻¹)⁻¹ !is_equiv_inv)) A HA B f H + definition is_trunc_is_equiv_closed_rev (n : trunc_index) (f : A → B) [H : is_equiv f] + [HA : is_trunc n B] : is_trunc n A := + is_trunc_is_equiv_closed n f⁻¹ + definition is_trunc_equiv_closed (n : trunc_index) (f : A ≃ B) [HA : is_trunc n A] : is_trunc n B := is_trunc_is_equiv_closed n (to_fun f) + definition is_trunc_equiv_closed_rev (n : trunc_index) (f : A ≃ B) [HA : is_trunc n B] + : is_trunc n A := + is_trunc_is_equiv_closed n (to_inv f) + definition is_equiv_of_is_hprop [HA : is_hprop A] [HB : is_hprop B] (f : A → B) (g : B → A) : is_equiv f := is_equiv.mk f g (λb, !is_hprop.elim) (λa, !is_hprop.elim) (λa, !is_hset.elim) diff --git a/hott/types/default.hlean b/hott/types/default.hlean index d4947f6d3..670e2106f 100644 --- a/hott/types/default.hlean +++ b/hott/types/default.hlean @@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Module: types.default Authors: Floris van Doorn - -The core of the HoTT library -/ import .sigma .prod .pi .equiv .fiber .eq .trunc .arrow .pointed diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean index c324d2daa..65a476910 100644 --- a/hott/types/equiv.hlean +++ b/hott/types/equiv.hlean @@ -9,53 +9,47 @@ Ported from Coq HoTT Theorems about the types equiv and is_equiv -/ -import types.fiber types.arrow arity +import .fiber .arrow arity .hprop_trunc -open eq is_trunc sigma sigma.ops arrow pi +open eq is_trunc sigma sigma.ops arrow pi fiber function equiv namespace is_equiv - open equiv function - section - open fiber - variables {A B : Type} (f : A → B) [H : is_equiv f] - include H - definition is_contr_fiber_of_is_equiv (b : B) : is_contr (fiber f b) := - is_contr.mk - (fiber.mk (f⁻¹ b) (right_inv f b)) - (λz, fiber.rec_on z (λa p, fiber_eq ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) (calc - right_inv f b = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ((ap (f ∘ f⁻¹) p) ⬝ right_inv f b) : by rewrite inv_con_cancel_left - ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (right_inv f (f a) ⬝ p) : by rewrite ap_con_eq_con - ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (ap f (left_inv f a) ⬝ p) : by rewrite adj - ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite con.assoc - ... = (ap f (ap f⁻¹ p))⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite ap_compose - ... = ap f (ap f⁻¹ p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite ap_inv - ... = ap f ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) ⬝ p : by rewrite ap_con))) - - definition is_contr_right_inverse : is_contr (Σ(g : B → A), f ∘ g ∼ id) := - begin - fapply is_trunc_equiv_closed, - {apply sigma_equiv_sigma_id, intro g, apply eq_equiv_homotopy}, - fapply is_trunc_equiv_closed, - {apply fiber.sigma_char}, - fapply is_contr_fiber_of_is_equiv, - apply (to_is_equiv (arrow_equiv_arrow_right (equiv.mk f H))), - end - - definition is_contr_right_coherence (u : Σ(g : B → A), f ∘ g ∼ id) - : is_contr (Σ(η : u.1 ∘ f ∼ id), Π(a : A), u.2 (f a) = ap f (η a)) := - begin - fapply is_trunc_equiv_closed, - {apply equiv.symm, apply sigma_pi_equiv_pi_sigma}, - fapply is_trunc_equiv_closed, - {apply pi_equiv_pi_id, intro a, - apply (fiber_eq_equiv (fiber.mk (u.1 (f a)) (u.2 (f a))) (fiber.mk a idp))}, - fapply is_trunc_pi, - intro a, fapply @is_contr_eq, - apply is_contr_fiber_of_is_equiv - end + variables {A B : Type} (f : A → B) [H : is_equiv f] + include H + /- is_equiv f is a mere proposition -/ + definition is_contr_fiber_of_is_equiv [instance] (b : B) : is_contr (fiber f b) := + is_contr.mk + (fiber.mk (f⁻¹ b) (right_inv f b)) + (λz, fiber.rec_on z (λa p, fiber_eq ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) (calc + right_inv f b = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ((ap (f ∘ f⁻¹) p) ⬝ right_inv f b) : by rewrite inv_con_cancel_left + ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (right_inv f (f a) ⬝ p) : by rewrite ap_con_eq_con + ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (ap f (left_inv f a) ⬝ p) : by rewrite adj + ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite con.assoc + ... = (ap f (ap f⁻¹ p))⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite ap_compose + ... = ap f (ap f⁻¹ p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite ap_inv + ... = ap f ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) ⬝ p : by rewrite ap_con))) + definition is_contr_right_inverse : is_contr (Σ(g : B → A), f ∘ g ∼ id) := + begin + fapply is_trunc_equiv_closed, + {apply sigma_equiv_sigma_id, intro g, apply eq_equiv_homotopy}, + fapply is_trunc_equiv_closed, + {apply fiber.sigma_char}, + fapply is_contr_fiber_of_is_equiv, + apply (to_is_equiv (arrow_equiv_arrow_right (equiv.mk f H))), end - variables {A B : Type} (f : A → B) + + definition is_contr_right_coherence (u : Σ(g : B → A), f ∘ g ∼ id) + : is_contr (Σ(η : u.1 ∘ f ∼ id), Π(a : A), u.2 (f a) = ap f (η a)) := + begin + fapply is_trunc_equiv_closed, + {apply equiv.symm, apply sigma_pi_equiv_pi_sigma}, + fapply is_trunc_equiv_closed, + {apply pi_equiv_pi_id, intro a, + apply (fiber_eq_equiv (fiber.mk (u.1 (f a)) (u.2 (f a))) (fiber.mk a idp))}, + end + + omit H protected definition sigma_char : (is_equiv f) ≃ (Σ(g : B → A) (ε : f ∘ g ∼ id) (η : g ∘ f ∼ id), Π(a : A), ε (f a) = ap f (η a)) := @@ -80,21 +74,32 @@ namespace is_equiv 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')) - /- contractible fibers -/ -- TODO: uncomment this (needs to import instance is_hprop_is_trunc) - -- definition is_contr_fun [reducible] {A B : Type} (f : A → B) := Π(b : B), is_contr (fiber f b) + /- contractible fibers -/ + definition is_contr_fun [reducible] (f : A → B) := Π(b : B), is_contr (fiber f b) - -- definition is_hprop_is_contr_fun (f : A → B) : is_hprop (is_contr_fun f) := _ + definition is_contr_fun_of_is_equiv [H : is_equiv f] : is_contr_fun f := + is_contr_fiber_of_is_equiv f - -- definition is_equiv_of_is_contr_fun [instance] [H : is_contr_fun f] : is_equiv f := - -- adjointify _ (λb, point (center (fiber f b))) - -- (λb, point_eq (center (fiber f b))) - -- (λa, ap point (contr (fiber.mk a idp))) + definition is_hprop_is_contr_fun (f : A → B) : is_hprop (is_contr_fun f) := _ - -- definition is_equiv_of_imp_is_equiv (H : B → is_equiv f) : is_equiv f := - -- @is_equiv_of_is_contr_fun _ _ f (is_contr_fun.mk (λb, @is_contr_fiber_of_is_equiv _ _ _ (H b) _)) + /- + we cannot make the next theorem an instance, because it loops together with + is_contr_fiber_of_is_equiv + -/ + definition is_equiv_of_is_contr_fun [H : is_contr_fun f] : is_equiv f := + adjointify _ (λb, point (center (fiber f b))) + (λb, point_eq (center (fiber f b))) + (λa, ap point (center_eq (fiber.mk a idp))) + + definition is_equiv_of_imp_is_equiv (H : B → is_equiv f) : is_equiv f := + @is_equiv_of_is_contr_fun _ _ f (λb, @is_contr_fiber_of_is_equiv _ _ _ (H b) _) + + definition is_equiv_equiv_is_contr_fun : is_equiv f ≃ is_contr_fun f := + equiv_of_is_hprop _ (λH, !is_equiv_of_is_contr_fun) end is_equiv @@ -108,4 +113,32 @@ namespace equiv definition equiv_eq {f f' : A ≃ B} (p : to_fun f = to_fun f') : f = f' := by (cases f; cases f'; apply (equiv_mk_eq p)) + + protected definition equiv.sigma_char (A B : Type) : (A ≃ B) ≃ Σ(f : A → B), is_equiv f := + begin + fapply equiv.MK, + {intro F, exact ⟨to_fun F, to_is_equiv F⟩}, + {intro p, cases p with [f, H], exact (equiv.mk f H)}, + {intro p, cases p with [f, H], exact idp}, + {intro F, cases F with [f, H], exact idp}, + end + + definition equiv_eq_char (f f' : A ≃ B) : (f = f') ≃ (to_fun f = to_fun f') := + calc + (f = f') ≃ (to_fun !equiv.sigma_char f = to_fun !equiv.sigma_char f') + : eq_equiv_fn_eq (to_fun !equiv.sigma_char) + ... ≃ ((to_fun !equiv.sigma_char f).1 = (to_fun !equiv.sigma_char f').1 ) : equiv_subtype + ... ≃ (to_fun f = to_fun f') : equiv.refl + + definition is_equiv_ap_to_fun (f f' : A ≃ B) + : is_equiv (ap to_fun : f = f' → to_fun f = to_fun f') := + begin + fapply adjointify, + {intro p, cases f with [f, H], cases f' with [f', H'], cases p, apply (ap (mk f')), apply is_hprop.elim}, + {intro p, cases f with [f, H], cases f' with [f', H'], cases p, + apply (@concat _ _ (ap to_fun (ap (equiv.mk f') (is_hprop.elim H H')))), {apply idp}, + generalize (is_hprop.elim H H'), intro q, cases q, apply idp}, + {intro p, cases p, cases f with [f, H], apply (ap (ap (equiv.mk f))), apply is_hset.elim} + end + end equiv diff --git a/hott/types/function.hlean b/hott/types/function.hlean new file mode 100644 index 000000000..2c982a5dd --- /dev/null +++ b/hott/types/function.hlean @@ -0,0 +1,98 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: types.function +Author: Floris van Doorn + +Ported from Coq HoTT +Theorems about embeddings and surjections +-/ + +import hit.trunc .pi .fiber .equiv + +open equiv sigma sigma.ops eq trunc is_trunc pi is_equiv fiber prod + +variables {A B : Type} {f : A → B} {b : B} + +structure is_embedding [class] (f : A → B) := +(elim : Π(a a' : A), is_equiv (@ap A B f a a')) + +structure is_surjective [class] (f : A → B) := +(elim : Π(b : B), ∥ fiber f b ∥) + +structure is_split_surjective [class] (f : A → B) := +(elim : Π(b : B), fiber f b) + +structure is_retraction [class] (f : A → B) := + (sect : B → A) + (right_inverse : Π(b : B), f (sect b) = b) + +namespace function + + attribute is_embedding.elim [instance] + + definition is_surjective_rec_on {P : Type} (H : is_surjective f) (b : B) [Pt : is_hprop P] + (IH : fiber f b → P) : P := + trunc.rec_on (is_surjective.elim f b) IH + + definition is_surjective_of_is_split_surjective [instance] [H : is_split_surjective f] + : is_surjective f := + is_surjective.mk (λb, tr (is_split_surjective.elim f b)) + + definition is_injective_of_is_embedding [reducible] [H : is_embedding f] {a a' : A} + : f a = f a' → a = a' := + (ap f)⁻¹ + + definition is_embedding_of_is_injective [HA : is_hset A] [HB : is_hset B] + (H : Π(a a' : A), f a = f a' → a = a') : is_embedding f := + begin + fapply is_embedding.mk, + intros [a, a'], + fapply adjointify, + {exact (H a a')}, + {intro p, apply is_hset.elim}, + {intro p, apply is_hset.elim} + end + + definition is_hprop_is_embedding [instance] (f : A → B) : is_hprop (is_embedding f) := + begin + have H : (Π(a a' : A), is_equiv (@ap A B f a a')) ≃ is_embedding f, + begin + fapply equiv.MK, + {exact is_embedding.mk}, + {intro h, cases h, exact elim}, + {intro h, cases h, apply idp}, + {intro p, apply idp}, + end, + apply is_trunc_equiv_closed, + exact H, + end + + definition is_hprop_is_surjective [instance] (f : A → B) : is_hprop (is_surjective f) := + begin + have H : (Π(b : B), merely (fiber f b)) ≃ is_surjective f, + begin + fapply equiv.MK, + {exact is_surjective.mk}, + {intro h, cases h, exact elim}, + {intro h, cases h, apply idp}, + {intro p, apply idp}, + end, + apply is_trunc_equiv_closed, + exact H, + end + + definition is_embedding_of_is_equiv [instance] (f : A → B) [H : is_equiv f] : is_embedding f := + is_embedding.mk _ + + definition is_equiv_of_is_surjective_of_is_embedding (f : A → B) + [H : is_embedding f] [H' : is_surjective f] : is_equiv f := + @is_equiv_of_is_contr_fun _ _ _ + (λb, is_surjective_rec_on H' b + (λa, is_contr.mk a + (λa', + fiber_eq ((ap f)⁻¹ ((point_eq a) ⬝ (point_eq a')⁻¹)) + (by rewrite (right_inv (ap f)); rewrite inv_con_cancel_right)))) + +end function diff --git a/hott/types/hprop_trunc.hlean b/hott/types/hprop_trunc.hlean new file mode 100644 index 000000000..1812b2d08 --- /dev/null +++ b/hott/types/hprop_trunc.hlean @@ -0,0 +1,63 @@ +/- +Copyright (c) 2015 Jakob von Raumer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: types.hprop_trunc +Authors: Jakob von Raumer, Floris van Doorn + +Proof of the theorem that (is_trunc n A) is a mere proposition +We prove this here to avoid circular dependency of files +We want to use this in .equiv; .equiv is imported by .function and .function is imported by .trunc +-/ + +import .pi + +open equiv sigma sigma.ops eq function pi + +namespace is_trunc + definition is_contr.sigma_char (A : Type) : + (Σ (center : A), Π (a : A), center = a) ≃ (is_contr A) := + begin + fapply equiv.MK, + { intro S, exact (is_contr.mk S.1 S.2)}, + { intro H, cases H with [H'], cases H' with [ce, co], exact ⟨ce, co⟩}, + { intro H, cases H with [H'], cases H' with [ce, co], exact idp}, + { intro S, cases S, apply idp} + end + + definition is_trunc.pi_char (n : trunc_index) (A : Type) : + (Π (x y : A), is_trunc n (x = y)) ≃ (is_trunc (n .+1) A) := + begin + fapply equiv.MK, + { intro H, apply is_trunc_succ_intro}, + { intros [H, x, y], apply is_trunc_eq}, + { intro H, cases H, apply idp}, + { intro P, apply eq_of_homotopy, intro a, apply eq_of_homotopy, intro b, + esimp [function.id,compose,is_trunc_succ_intro,is_trunc_eq], + generalize (P a b), intro H, cases H, apply idp}, + end + + definition is_hprop_is_trunc [instance] (n : trunc_index) : + Π (A : Type), is_hprop (is_trunc n A) := + begin + apply (trunc_index.rec_on n), + { intro A, + apply is_trunc_is_equiv_closed, + { apply equiv.to_is_equiv, apply is_contr.sigma_char}, + apply (@is_hprop.mk), intros, + fapply sigma_eq, {apply x.2}, + apply (@is_hprop.elim), + apply is_trunc_pi, intro a, + apply is_hprop.mk, intros [w, z], + have H : is_hset A, + begin + apply is_trunc_succ, apply is_trunc_succ, + apply is_contr.mk, exact y.2 + end, + fapply (@is_hset.elim A _ _ _ w z)}, + { intros [n', IH, A], + apply is_trunc_is_equiv_closed, + apply equiv.to_is_equiv, + apply is_trunc.pi_char}, + end +end is_trunc diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index c2494a11c..af16d8055 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -3,75 +3,99 @@ Copyright (c) 2015 Jakob von Raumer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Module: types.trunc -Authors: Jakob von Raumer, Floris van Doorn +Authors: Floris van Doorn -Properties of is_trunc +Properties of is_trunc and trunctype -/ -import types.pi types.eq +--NOTE: the fact that (is_trunc n A) is a mere proposition is proved in .hprop_trunc + +import types.pi types.eq types.equiv .function + +open eq sigma sigma.ops pi function equiv is_trunc.trunctype is_equiv prod -open sigma sigma.ops pi function eq equiv eq funext namespace is_trunc + variables {A B : Type} {n : trunc_index} - definition is_contr.sigma_char (A : Type) : - (Σ (center : A), Π (a : A), center = a) ≃ (is_contr A) := - begin - fapply equiv.mk, - {intro S, apply is_contr.mk, exact S.2}, - {fapply is_equiv.adjointify, - {intro H, apply sigma.mk, exact (@center_eq A H)}, - {intro H, apply (is_trunc.rec_on H), intro Hint, - apply (contr_internal.rec_on Hint), intros [H1, H2], - apply idp}, - {intro S, cases S, apply idp}} - end - - definition is_trunc.pi_char (n : trunc_index) (A : Type) : - (Π (x y : A), is_trunc n (x = y)) ≃ (is_trunc (n .+1) A) := - begin - fapply equiv.MK, - {intro H, apply is_trunc_succ_intro}, - {intros [H, x, y], apply is_trunc_eq}, - {intro H, apply (is_trunc.rec_on H), intro Hint, apply idp}, - {intro P, apply eq_of_homotopy, intro a, apply eq_of_homotopy, intro b, - esimp [function.id,compose,is_trunc_succ_intro,is_trunc_eq], - generalize (P a b), intro H, apply (is_trunc.rec_on H), intro H', apply idp}, - end - - definition is_hprop_is_trunc [instance] (n : trunc_index) : - Π (A : Type), is_hprop (is_trunc n A) := - begin - apply (trunc_index.rec_on n), - {intro A, - apply is_trunc_is_equiv_closed, apply equiv.to_is_equiv, - apply is_contr.sigma_char, - apply (@is_hprop.mk), intros, - fapply sigma_eq, apply x.2, - apply (@is_hprop.elim), - apply is_trunc_pi, intro a, - apply is_hprop.mk, intros [w, z], - have H : is_hset A, - begin - apply is_trunc_succ, apply is_trunc_succ, - apply is_contr.mk, exact y.2 - end, - fapply (@is_hset.elim A _ _ _ w z)}, - {intros [n', IH, A], - apply is_trunc_is_equiv_closed, - apply equiv.to_is_equiv, - apply is_trunc.pi_char}, - end - - definition is_trunc_succ_of_imp_is_trunc_succ {A : Type} {n : trunc_index} (H : A → is_trunc (n.+1) A) - : is_trunc (n.+1) A := + definition is_trunc_succ_of_imp_is_trunc_succ (H : A → is_trunc (n.+1) A) : is_trunc (n.+1) A := @is_trunc_succ_intro _ _ (λx y, @is_trunc_eq _ _ (H x) x y) - definition is_trunc_of_imp_is_trunc_of_leq {A : Type} {n : trunc_index} (Hn : -1 ≤ n) - (H : A → is_trunc n A) : is_trunc n A := + definition is_trunc_of_imp_is_trunc_of_leq (Hn : -1 ≤ n) (H : A → is_trunc n A) : is_trunc n A := trunc_index.rec_on n (λHn H, empty.rec _ Hn) (λn IH Hn, is_trunc_succ_of_imp_is_trunc_succ) Hn H + /- theorems about trunctype -/ + protected definition trunctype.sigma_char.{l} (n : trunc_index) : + (trunctype.{l} n) ≃ (Σ (A : Type.{l}), is_trunc n A) := + begin + fapply equiv.MK, + { 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}, + end + + definition trunctype_eq_equiv (n : trunc_index) (A B : n-Type) : + (A = B) ≃ (carrier A = carrier B) := + calc + (A = B) ≃ (to_fun (trunctype.sigma_char n) A = to_fun (trunctype.sigma_char n) B) + : eq_equiv_fn_eq_of_equiv + ... ≃ ((to_fun (trunctype.sigma_char n) A).1 = (to_fun (trunctype.sigma_char n) B).1) + : equiv.symm (!equiv_subtype) + ... ≃ (carrier A = carrier B) : equiv.refl + + definition is_trunc_is_embedding_closed (f : A → B) [Hf : is_embedding f] [HB : is_trunc n B] + (Hn : -1 ≤ n) : is_trunc n A := + begin + cases n with [n], + {exact (!empty.elim Hn)}, + {apply is_trunc_succ_intro, intros [a, a'], + fapply (@is_trunc_is_equiv_closed_rev _ _ n (ap f))} + end + + definition is_trunc_is_retraction_closed (f : A → B) [Hf : is_retraction f] + (n : trunc_index) [HA : is_trunc n A] : is_trunc n B := + begin + reverts [A, B, f, Hf, HA], + apply (trunc_index.rec_on n), + { clear n, intros [A, B, f, Hf, HA], cases Hf with [g, ε], fapply is_contr.mk, + { exact (f (center A))}, + { intro b, apply concat, + { apply (ap f), exact (center_eq (g b))}, + { apply ε}}}, + { clear n, intros [n, IH, A, B, f, Hf, HA], cases Hf with [g, ε], + apply is_trunc_succ_intro, intros [b, b'], + fapply (IH (g b = g b')), + { intro q, exact ((ε b)⁻¹ ⬝ ap f q ⬝ ε b')}, + { apply (is_retraction.mk (ap g)), + { intro p, cases p, {rewrite [↑ap, con_idp, con.left_inv]}}}, + { apply is_trunc_eq}} + end + + definition is_embedding_to_fun (A B : Type) : is_embedding (@to_fun A B) := + is_embedding.mk (λf f', !is_equiv_ap_to_fun) + + definition is_trunc_trunctype [instance] (n : trunc_index) : is_trunc n.+1 (n-Type) := + begin + apply is_trunc_succ_intro, intros [X, Y], + fapply is_trunc_equiv_closed, + {apply equiv.symm, apply trunctype_eq_equiv}, + fapply is_trunc_equiv_closed, + {apply equiv.symm, apply eq_equiv_equiv}, + cases n, + {apply @is_contr_of_inhabited_hprop, + {apply is_trunc_is_embedding_closed, + {apply is_embedding_to_fun} , + {exact unit.star}}, + {apply equiv_of_is_contr_of_is_contr}}, + {apply is_trunc_is_embedding_closed, + {apply is_embedding_to_fun}, + {exact unit.star}} + end + + + /- theorems about decidable equality and axiom K -/ definition is_hset_of_axiom_K {A : Type} (K : Π{a : A} (p : a = a), p = idp) : is_hset A := is_hset.mk _ (λa b p q, eq.rec_on q K p) @@ -116,24 +140,62 @@ namespace is_trunc (K : Π(a : A), is_trunc n (a = a)) : is_trunc (n.+1) A := @is_trunc_succ_intro _ _ (λa b, is_trunc_of_imp_is_trunc_of_leq H (λp, eq.rec_on p !K)) - open trunctype equiv equiv.ops +end is_trunc open is_trunc - protected definition trunctype.sigma_char.{l} (n : trunc_index) : - (trunctype.{l} n) ≃ (Σ (A : Type.{l}), is_trunc n A) := +namespace trunc + variable {A : Type} + + definition trunc_eq_type (n : trunc_index) (aa aa' : trunc n.+1 A) : n-Type := + trunc.rec_on aa (λa, trunc.rec_on aa' (λa', trunctype.mk' n (trunc n (a = a')))) + + definition trunc_eq_equiv (n : trunc_index) (aa aa' : trunc n.+1 A) + : aa = aa' ≃ trunc_eq_type n aa aa' := begin fapply equiv.MK, - /--/ 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, + { intro p, cases p, apply (trunc.rec_on aa), + intro a, esimp [trunc_eq_type,trunc.rec_on], exact (tr idp)}, + { apply (trunc.rec_on aa'), apply (trunc.rec_on aa), + intros [a, a', x], esimp [trunc_eq_type, trunc.rec_on] at x, + apply (trunc.rec_on x), intro p, exact (ap tr p)}, + { + -- apply (trunc.rec_on aa'), apply (trunc.rec_on aa), + -- intros [a, a', x], esimp [trunc_eq_type, trunc.rec_on] at x, + -- apply (trunc.rec_on x), intro p, + -- cases p, esimp [trunc.rec_on,eq.cases_on,compose,id], -- apply idp --? + apply sorry}, + { intro p, cases p, apply (trunc.rec_on aa), intro a, apply sorry}, end - protected definition trunctype_eq_equiv (n : trunc_index) (A B : n-Type) : - (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) - ... ≃ (carrier A = carrier B) : equiv.refl + definition tr_eq_tr_equiv (n : trunc_index) (a a' : A) + : (tr a = tr a' :> trunc n.+1 A) ≃ trunc n (a = a') := + !trunc_eq_equiv + definition is_trunc_trunc_of_is_trunc [instance] [priority 500] (A : Type) + (n m : trunc_index) [H : is_trunc n A] : is_trunc n (trunc m A) := + begin + reverts [A, m, H], apply (trunc_index.rec_on n), + { clear n, intros [A, m, H], apply is_contr_equiv_closed, + { apply equiv_trunc, apply (@is_trunc_of_leq _ -2), exact unit.star} }, + { clear n, intros [n, IH, A, m, H], cases m with [m], + { apply (@is_trunc_of_leq _ -2), exact unit.star}, + { apply is_trunc_succ_intro, intros [aa, aa'], + apply (@trunc.rec_on _ _ _ aa (λy, !is_trunc_succ_of_is_hprop)), + apply (@trunc.rec_on _ _ _ aa' (λy, !is_trunc_succ_of_is_hprop)), + intros [a, a'], apply (is_trunc_equiv_closed_rev), + { apply tr_eq_tr_equiv}, + { exact (IH _ _ _)}}} + end -end is_trunc +end trunc open trunc + +namespace function + variables {A B : Type} + definition is_surjective_of_is_equiv [instance] (f : A → B) [H : is_equiv f] : is_surjective f := + is_surjective.mk (λb, !center) + + definition is_equiv_equiv_is_embedding_times_is_surjective (f : A → B) + : is_equiv f ≃ (is_embedding f × is_surjective f) := + equiv_of_is_hprop (λH, (_, _)) + (λP, prod.rec_on P (λH₁ H₂, !is_equiv_of_is_surjective_of_is_embedding)) + +end function diff --git a/hott/types/types.md b/hott/types/types.md index 099d84cde..77efad375 100644 --- a/hott/types/types.md +++ b/hott/types/types.md @@ -3,13 +3,16 @@ hott.types Various datatypes. +* [prod](prod.hlean) +* [sigma](sigma.hlean) * [pi](pi.hlean) * [arrow](arrow.hlean) * [eq](eq.hlean) -* [trunc](trunc.hlean) -* [prod](prod.hlean) -* [sigma](sigma.hlean) * [fiber](fiber.hlean) +* [hprop_trunc](hprop_trunc.hlean): in this file we prove that `is_trunc n A` is a mere proposition. We separate this from [trunc](trunc.hlean) to avoid circularity in imports. * [equiv](equiv.hlean) * [pointed](pointed.hlean) + +* [trunc](trunc.hlean) + * [W](W.hlean) (not loaded by default) \ No newline at end of file