feat(hott/function): show that a function is embedding iff it has propositional fibers

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 :=

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

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',

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,

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⟩

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,