From d402b67d252b38cd82b97d8bad8689bc0e984dc2 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 5 Nov 2015 12:51:59 -0500 Subject: [PATCH] feat(hott/function): show that a function is embedding iff it has propositional fibers --- hott/function.hlean | 15 +++++++++++++++ hott/init/pathover.hlean | 10 +++++++++- hott/types/W.hlean | 12 ++++++------ hott/types/equiv.hlean | 4 +--- hott/types/fiber.hlean | 9 ++++++--- hott/types/sigma.hlean | 2 -- 6 files changed, 37 insertions(+), 15 deletions(-) diff --git a/hott/function.hlean b/hott/function.hlean index b1468db29..8c5fb1559 100644 --- a/hott/function.hlean +++ b/hott/function.hlean @@ -61,6 +61,10 @@ namespace function : is_equiv (ap f : a = a' → f a = f a') := H a a' + definition ap_inv_idp {a : A} {H : is_equiv (ap f : a = a → f a = f a)} + : (ap f)⁻¹ᶠ idp = idp :> a = a := + !left_inv + variable {f} definition is_injective_of_is_embedding [reducible] [H : is_embedding f] {a a' : A} : f a = f a' → a = a' := @@ -101,6 +105,17 @@ namespace function { esimp [is_injective_of_is_embedding], symmetry, apply right_inv} end + definition is_hprop_fun_of_is_embedding [H : is_embedding f] : is_trunc_fun -1 f := + is_hprop_fiber_of_is_embedding f + + definition is_embedding_of_is_hprop_fun [constructor] [H : is_trunc_fun -1 f] : is_embedding f := + begin + intro a a', fapply adjointify, + { intro p, exact ap point (@is_hprop.elim (fiber f (f a')) _ (fiber.mk a p) (fiber.mk a' idp))}, + { intro p, rewrite [-ap_compose], esimp, apply ap_con_eq (@point_eq _ _ f (f a'))}, + { intro p, induction p, apply ap (ap point), apply is_hprop_elim_self} + end + variable {f} definition is_surjective_rec_on {P : Type} (H : is_surjective f) (b : B) [Pt : is_hprop P] (IH : fiber f b → P) : P := diff --git a/hott/init/pathover.hlean b/hott/init/pathover.hlean index 59358fc88..4a554ae34 100644 --- a/hott/init/pathover.hlean +++ b/hott/init/pathover.hlean @@ -253,10 +253,18 @@ namespace eq (b : B a) : f b =[apo011 C p !pathover_tr] g (p ▸ b) := by cases r; constructor - definition apo10 {f : B a → B' a} {g : B a₂ → B' a₂} (r : f =[p] g) + definition apo10 [unfold 9] {f : B a → B' a} {g : B a₂ → B' a₂} (r : f =[p] g) (b : B a) : f b =[p] g (p ▸ b) := by cases r; constructor + definition apo10_constant_right [unfold 9] {f : B a → A'} {g : B a₂ → A'} (r : f =[p] g) + (b : B a) : f b = g (p ▸ b) := + by cases r; constructor + + definition apo10_constant_left [unfold 9] {f : A' → B a} {g : A' → B a₂} (r : f =[p] g) + (a' : A') : f a' =[p] g a' := + by cases r; constructor + definition apo11 {f : B a → B' a} {g : B a₂ → B' a₂} (r : f =[p] g) (q : b =[p] b₂) : f b =[p] g b₂ := by induction q; exact apo10 r b diff --git a/hott/types/W.hlean b/hott/types/W.hlean index 51d1f6e67..7ea30fdb7 100644 --- a/hott/types/W.hlean +++ b/hott/types/W.hlean @@ -32,19 +32,19 @@ namespace Wtype end ops open ops - protected definition eta (w : W a, B a) : ⟨w.1 , w.2⟩ = w := + protected definition eta [unfold 3] (w : W a, B a) : ⟨w.1 , w.2⟩ = w := by cases w; exact idp - definition sup_eq_sup (p : a = a') (q : f =[p] f') : ⟨a, f⟩ = ⟨a', f'⟩ := + definition sup_eq_sup [unfold 8] (p : a = a') (q : f =[p] f') : ⟨a, f⟩ = ⟨a', f'⟩ := by cases q; exact idp - definition Wtype_eq (p : w.1 = w'.1) (q : w.2 =[p] w'.2) : w = w' := + definition Wtype_eq [unfold 3 4] (p : w.1 = w'.1) (q : w.2 =[p] w'.2) : w = w' := by cases w; cases w';exact (sup_eq_sup p q) - definition Wtype_eq_pr1 (p : w = w') : w.1 = w'.1 := + definition Wtype_eq_pr1 [unfold 5] (p : w = w') : w.1 = w'.1 := by cases p;exact idp - definition Wtype_eq_pr2 (p : w = w') : w.2 =[Wtype_eq_pr1 p] w'.2 := + definition Wtype_eq_pr2 [unfold 5] (p : w = w') : w.2 =[Wtype_eq_pr1 p] w'.2 := by cases p;exact idpo namespace ops @@ -116,7 +116,7 @@ namespace Wtype /- truncatedness -/ open is_trunc pi - definition trunc_W [instance] (n : trunc_index) + definition is_trunc_W [instance] (n : trunc_index) [HA : is_trunc (n.+1) A] : is_trunc (n.+1) (W a, B a) := begin fapply is_trunc_succ_intro, intro w w', diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean index beec18a3b..03b3bb383 100644 --- a/hott/types/equiv.hlean +++ b/hott/types/equiv.hlean @@ -84,8 +84,6 @@ namespace is_equiv apd011 inv p !is_hprop.elim /- contractible fibers -/ - definition is_contr_fun [reducible] (f : A → B) := Π(b : B), is_contr (fiber f b) - definition is_contr_fun_of_is_equiv [H : is_equiv f] : is_contr_fun f := is_contr_fiber_of_is_equiv f @@ -115,7 +113,7 @@ namespace is_equiv definition is_equiv_total_of_is_fiberwise_equiv [H : is_fiberwise_equiv f] : is_equiv (total f) := is_equiv_sigma_functor id f - definition is_fiberwise_equiv_of_is_equiv_total [H : is_equiv (sigma_functor id f)] + definition is_fiberwise_equiv_of_is_equiv_total [H : is_equiv (total f)] : is_fiberwise_equiv f := begin intro a, diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean index 83f6e1edc..24a9f8e6c 100644 --- a/hott/types/fiber.hlean +++ b/hott/types/fiber.hlean @@ -66,6 +66,10 @@ namespace fiber definition pointed_fiber [constructor] (f : A → B) (a : A) : Type* := Pointed.mk (fiber.mk a (idpath (f a))) + definition is_trunc_fun [reducible] (n : trunc_index) (f : A → B) := + Π(b : B), is_trunc n (fiber f b) + definition is_contr_fun [reducible] (f : A → B) := is_trunc_fun -2 f + end fiber open unit is_trunc @@ -98,11 +102,10 @@ namespace fiber variables {A : Type} {P Q : A → Type} variable (f : Πa, P a → Q a) - /- Note that the map on total spaces/sigmas is just sigma_functor id -/ definition fiber_total_equiv {a : A} (q : Q a) - : fiber (sigma_functor id f) ⟨a , q⟩ ≃ fiber (f a) q := + : fiber (total f) ⟨a , q⟩ ≃ fiber (f a) q := calc - fiber (sigma_functor id f) ⟨a , q⟩ + fiber (total f) ⟨a , q⟩ ≃ Σ(w : Σx, P x), ⟨w.1 , f w.1 w.2 ⟩ = ⟨a , q⟩ : fiber.sigma_char ... ≃ Σ(x : A), Σ(p : P x), ⟨x , f x p⟩ = ⟨a , q⟩ diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index 9c5e836d3..beaa30ea2 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -146,9 +146,7 @@ namespace sigma definition sigma_eq2 {p q : u = v} (r : p..1 = q..1) (s : p..2 =[r] q..2) : p = q := begin - revert q r s, induction p, induction u with u1 u2, - intro q r s, transitivity sigma_eq q..1 q..2, apply sigma_eq_eq_sigma_eq r s, apply sigma_eq_eta,