feat(category.adjoint): prove more about functors
This commit is contained in:
Floris van Doorn
Leonardo de Moura
parent
18ec5f8b85
commit
3f0d8c0a8c
3 changed files with 201 additions and 98 deletions
|
|
@ -43,7 +43,6 @@ namespace category
|
|||
--a second notation for the inverse, which is not overloaded (there is no unicode superscript F)
|
||||
postfix [parsing_only] `⁻¹F`:std.prec.max_plus := inverse
|
||||
|
||||
--TODO: review and change
|
||||
definition faithful [class] (F : C ⇒ D) := Π⦃c c' : C⦄ ⦃f f' : c ⟶ c'⦄, F f = F f' → f = f'
|
||||
definition full [class] (F : C ⇒ D) := Π⦃c c' : C⦄, is_surjective (@(to_fun_hom F) c c')
|
||||
definition fully_faithful [class] (F : C ⇒ D) := Π(c c' : C), is_equiv (@(to_fun_hom F) c c')
|
||||
|
|
@ -114,75 +113,11 @@ namespace category
|
|||
definition is_iso_counit [instance] (F : C ⇒ D) [H : is_equivalence F] : is_iso (counit F) :=
|
||||
!is_equivalence.is_iso_counit
|
||||
|
||||
theorem is_hprop_is_left_adjoint {C : Category} {D : Precategory} (F : C ⇒ D)
|
||||
: is_hprop (is_left_adjoint F) :=
|
||||
begin
|
||||
apply is_hprop.mk,
|
||||
intro G G', cases G with G η ε H K, cases G' with G' η' ε' H' K',
|
||||
assert lem₁ : Π(p : G = G'), p ▸ η = η' → p ▸ ε = ε'
|
||||
→ is_left_adjoint.mk G η ε H K = is_left_adjoint.mk G' η' ε' H' K',
|
||||
{ intros p q r, induction p, induction q, induction r, esimp,
|
||||
apply apd011 (is_left_adjoint.mk G η ε) !is_hprop.elim !is_hprop.elim},
|
||||
assert lem₂ : Π (d : carrier D),
|
||||
(to_fun_hom G (natural_map ε' d) ∘
|
||||
natural_map η (to_fun_ob G' d)) ∘
|
||||
to_fun_hom G' (natural_map ε d) ∘
|
||||
natural_map η' (to_fun_ob G d) = id,
|
||||
{ intro d, esimp,
|
||||
rewrite [assoc],
|
||||
rewrite [-assoc (G (ε' d))],
|
||||
esimp, rewrite [nf_fn_eq_fn_nf_pt' G' ε η d],
|
||||
esimp, rewrite [assoc],
|
||||
esimp, rewrite [-assoc],
|
||||
rewrite [↑functor.compose, -respect_comp G],
|
||||
rewrite [nf_fn_eq_fn_nf_pt ε ε' d,nf_fn_eq_fn_nf_pt η' η (G d),▸*],
|
||||
rewrite [respect_comp G],
|
||||
rewrite [assoc,▸*,-assoc (G (ε d))],
|
||||
rewrite [↑functor.compose, -respect_comp G],
|
||||
rewrite [H' (G d)],
|
||||
rewrite [respect_id,▸*,id_right],
|
||||
apply K},
|
||||
assert lem₃ : Π (d : carrier D),
|
||||
(to_fun_hom G' (natural_map ε d) ∘
|
||||
natural_map η' (to_fun_ob G d)) ∘
|
||||
to_fun_hom G (natural_map ε' d) ∘
|
||||
natural_map η (to_fun_ob G' d) = id,
|
||||
{ intro d, esimp,
|
||||
rewrite [assoc, -assoc (G' (ε d))],
|
||||
esimp, rewrite [nf_fn_eq_fn_nf_pt' G ε' η' d],
|
||||
esimp, rewrite [assoc], esimp, rewrite [-assoc],
|
||||
rewrite [↑functor.compose, -respect_comp G'],
|
||||
rewrite [nf_fn_eq_fn_nf_pt ε' ε d,nf_fn_eq_fn_nf_pt η η' (G' d)],
|
||||
esimp,
|
||||
rewrite [respect_comp G'],
|
||||
rewrite [assoc,▸*,-assoc (G' (ε' d))],
|
||||
rewrite [↑functor.compose, -respect_comp G'],
|
||||
rewrite [H (G' d)],
|
||||
rewrite [respect_id,▸*,id_right],
|
||||
apply K'},
|
||||
fapply lem₁,
|
||||
{ fapply functor.eq_of_pointwise_iso,
|
||||
{ fapply change_natural_map,
|
||||
{ exact (G' ∘fn1 ε) ∘n !assoc_natural_rev ∘n (η' ∘1nf G)},
|
||||
{ intro d, exact (G' (ε d) ∘ η' (G d))},
|
||||
{ intro d, exact ap (λx, _ ∘ x) !id_left}},
|
||||
{ intro d, fconstructor,
|
||||
{ exact (G (ε' d) ∘ η (G' d))},
|
||||
{ exact lem₂ d },
|
||||
{ exact lem₃ d }}},
|
||||
{ clear lem₁, refine transport_hom_of_eq_right _ η ⬝ _,
|
||||
krewrite hom_of_eq_compose_right,
|
||||
rewrite functor.hom_of_eq_eq_of_pointwise_iso,
|
||||
apply nat_trans_eq, intro c, esimp,
|
||||
refine !assoc⁻¹ ⬝ ap (λx, _ ∘ x) (nf_fn_eq_fn_nf_pt η η' c) ⬝ !assoc ⬝ _,
|
||||
esimp, rewrite [-respect_comp G',H c,respect_id G',▸*,id_left]},
|
||||
{ clear lem₁, refine transport_hom_of_eq_left _ ε ⬝ _,
|
||||
krewrite inv_of_eq_compose_left,
|
||||
rewrite functor.inv_of_eq_eq_of_pointwise_iso,
|
||||
apply nat_trans_eq, intro d, esimp,
|
||||
krewrite [respect_comp],
|
||||
rewrite [assoc,nf_fn_eq_fn_nf_pt ε' ε d,-assoc,▸*,H (G' d),id_right]}
|
||||
end
|
||||
definition iso_unit (F : C ⇒ D) [H : is_equivalence F] : F ⁻¹F ∘f F ≅ 1 :=
|
||||
(@(iso.mk _) !is_iso_unit)⁻¹ⁱ
|
||||
|
||||
definition iso_counit (F : C ⇒ D) [H : is_equivalence F] : F ∘f F ⁻¹F ≅ 1 :=
|
||||
@(iso.mk _) !is_iso_counit
|
||||
|
||||
definition full_of_fully_faithful (H : fully_faithful F) : full F :=
|
||||
λc c' g, tr (fiber.mk ((@(to_fun_hom F) c c')⁻¹ᶠ g) !right_inv)
|
||||
|
|
@ -287,7 +222,7 @@ namespace category
|
|||
exact naturality (to_hom η) (G (to_hom (εi d))),
|
||||
end
|
||||
|
||||
parameters (F G)
|
||||
parameter (G)
|
||||
include η ε
|
||||
definition is_equivalence.mk : is_equivalence F :=
|
||||
begin
|
||||
|
|
@ -307,7 +242,7 @@ namespace category
|
|||
equivalence.mk F is_equivalence.mk
|
||||
end
|
||||
|
||||
variables {C D : Precategory} {F : C ⇒ D} {G : D ⇒ C}
|
||||
variables {C D E : Precategory} {F : C ⇒ D}
|
||||
|
||||
--TODO: add variants
|
||||
definition unit_eq_counit_inv (F : C ⇒ D) [H : is_equivalence F] (c : C) :
|
||||
|
|
@ -324,12 +259,12 @@ namespace category
|
|||
fapply adjointify,
|
||||
{ intro g, exact natural_map (@(iso.inverse (unit F)) !is_iso_unit) c' ∘ F⁻¹ g ∘ unit F c},
|
||||
{ intro g, rewrite [+respect_comp,▸*],
|
||||
krewrite [natural_map_inverse], xrewrite [respect_inv'],
|
||||
xrewrite [natural_map_inverse (unit F) c', respect_inv'],
|
||||
apply inverse_comp_eq_of_eq_comp,
|
||||
let H := @(naturality (F ∘fn (unit F))),
|
||||
rewrite [+unit_eq_counit_inv], exact sorry},
|
||||
/-this is basically the naturality of the counit-/
|
||||
{ exact sorry},
|
||||
rewrite [+unit_eq_counit_inv],
|
||||
esimp, exact naturality (counit F)⁻¹ _},
|
||||
{ intro f, xrewrite [▸*,natural_map_inverse (unit F) c'], apply inverse_comp_eq_of_eq_comp,
|
||||
apply naturality (unit F)},
|
||||
end
|
||||
|
||||
definition is_isomorphism.mk {F : C ⇒ D} (G : D ⇒ C) (p : G ∘f F = 1) (q : F ∘f G = 1)
|
||||
|
|
@ -368,7 +303,9 @@ namespace category
|
|||
exact !right_inverse⁻¹},
|
||||
end
|
||||
|
||||
definition strict_right_inverse (F : C ⇒ D) [H : is_isomorphism F] : F ∘f strict_inverse F = 1 :=
|
||||
postfix /-[parsing-only]-/ `⁻¹ˢ`:std.prec.max_plus := strict_inverse
|
||||
|
||||
definition strict_right_inverse (F : C ⇒ D) [H : is_isomorphism F] : F ∘f F⁻¹ˢ = 1 :=
|
||||
begin
|
||||
fapply functor_eq,
|
||||
{ intro d, esimp, apply right_inv},
|
||||
|
|
@ -378,7 +315,7 @@ namespace category
|
|||
rewrite [id_left], apply comp_inverse_cancel_right},
|
||||
end
|
||||
|
||||
definition strict_left_inverse (F : C ⇒ D) [H : is_isomorphism F] : strict_inverse F ∘f F = 1 :=
|
||||
definition strict_left_inverse (F : C ⇒ D) [H : is_isomorphism F] : F⁻¹ˢ ∘f F = 1 :=
|
||||
begin
|
||||
fapply functor_eq,
|
||||
{ intro d, esimp, apply left_inv},
|
||||
|
|
@ -392,31 +329,180 @@ namespace category
|
|||
: is_equivalence F :=
|
||||
begin
|
||||
fapply is_equivalence.mk,
|
||||
{ apply strict_inverse F},
|
||||
{ apply F⁻¹ˢ},
|
||||
{ apply iso_of_eq !strict_left_inverse},
|
||||
{ apply iso_of_eq !strict_right_inverse},
|
||||
end
|
||||
|
||||
theorem is_hprop_is_left_adjoint [instance] {C : Category} {D : Precategory} (F : C ⇒ D)
|
||||
: is_hprop (is_left_adjoint F) :=
|
||||
begin
|
||||
apply is_hprop.mk,
|
||||
intro G G', cases G with G η ε H K, cases G' with G' η' ε' H' K',
|
||||
assert lem₁ : Π(p : G = G'), p ▸ η = η' → p ▸ ε = ε'
|
||||
→ is_left_adjoint.mk G η ε H K = is_left_adjoint.mk G' η' ε' H' K',
|
||||
{ intros p q r, induction p, induction q, induction r, esimp,
|
||||
apply apd011 (is_left_adjoint.mk G η ε) !is_hprop.elim !is_hprop.elim},
|
||||
assert lem₂ : Π (d : carrier D),
|
||||
(to_fun_hom G (natural_map ε' d) ∘
|
||||
natural_map η (to_fun_ob G' d)) ∘
|
||||
to_fun_hom G' (natural_map ε d) ∘
|
||||
natural_map η' (to_fun_ob G d) = id,
|
||||
{ intro d, esimp,
|
||||
rewrite [assoc],
|
||||
rewrite [-assoc (G (ε' d))],
|
||||
esimp, rewrite [nf_fn_eq_fn_nf_pt' G' ε η d],
|
||||
esimp, rewrite [assoc],
|
||||
esimp, rewrite [-assoc],
|
||||
rewrite [↑functor.compose, -respect_comp G],
|
||||
rewrite [nf_fn_eq_fn_nf_pt ε ε' d,nf_fn_eq_fn_nf_pt η' η (G d),▸*],
|
||||
rewrite [respect_comp G],
|
||||
rewrite [assoc,▸*,-assoc (G (ε d))],
|
||||
rewrite [↑functor.compose, -respect_comp G],
|
||||
rewrite [H' (G d)],
|
||||
rewrite [respect_id,▸*,id_right],
|
||||
apply K},
|
||||
assert lem₃ : Π (d : carrier D),
|
||||
(to_fun_hom G' (natural_map ε d) ∘
|
||||
natural_map η' (to_fun_ob G d)) ∘
|
||||
to_fun_hom G (natural_map ε' d) ∘
|
||||
natural_map η (to_fun_ob G' d) = id,
|
||||
{ intro d, esimp,
|
||||
rewrite [assoc, -assoc (G' (ε d))],
|
||||
esimp, rewrite [nf_fn_eq_fn_nf_pt' G ε' η' d],
|
||||
esimp, rewrite [assoc], esimp, rewrite [-assoc],
|
||||
rewrite [↑functor.compose, -respect_comp G'],
|
||||
rewrite [nf_fn_eq_fn_nf_pt ε' ε d,nf_fn_eq_fn_nf_pt η η' (G' d)],
|
||||
esimp,
|
||||
rewrite [respect_comp G'],
|
||||
rewrite [assoc,▸*,-assoc (G' (ε' d))],
|
||||
rewrite [↑functor.compose, -respect_comp G'],
|
||||
rewrite [H (G' d)],
|
||||
rewrite [respect_id,▸*,id_right],
|
||||
apply K'},
|
||||
fapply lem₁,
|
||||
{ fapply functor.eq_of_pointwise_iso,
|
||||
{ fapply change_natural_map,
|
||||
{ exact (G' ∘fn1 ε) ∘n !assoc_natural_rev ∘n (η' ∘1nf G)},
|
||||
{ intro d, exact (G' (ε d) ∘ η' (G d))},
|
||||
{ intro d, exact ap (λx, _ ∘ x) !id_left}},
|
||||
{ intro d, fconstructor,
|
||||
{ exact (G (ε' d) ∘ η (G' d))},
|
||||
{ exact lem₂ d },
|
||||
{ exact lem₃ d }}},
|
||||
{ clear lem₁, refine transport_hom_of_eq_right _ η ⬝ _,
|
||||
krewrite hom_of_eq_compose_right,
|
||||
rewrite functor.hom_of_eq_eq_of_pointwise_iso,
|
||||
apply nat_trans_eq, intro c, esimp,
|
||||
refine !assoc⁻¹ ⬝ ap (λx, _ ∘ x) (nf_fn_eq_fn_nf_pt η η' c) ⬝ !assoc ⬝ _,
|
||||
esimp, rewrite [-respect_comp G',H c,respect_id G',▸*,id_left]},
|
||||
{ clear lem₁, refine transport_hom_of_eq_left _ ε ⬝ _,
|
||||
krewrite inv_of_eq_compose_left,
|
||||
rewrite functor.inv_of_eq_eq_of_pointwise_iso,
|
||||
apply nat_trans_eq, intro d, esimp,
|
||||
krewrite [respect_comp],
|
||||
rewrite [assoc,nf_fn_eq_fn_nf_pt ε' ε d,-assoc,▸*,H (G' d),id_right]}
|
||||
end
|
||||
|
||||
theorem is_hprop_is_equivalence [instance] {C : Category} {D : Precategory} (F : C ⇒ D) : is_hprop (is_equivalence F) :=
|
||||
begin
|
||||
assert f : is_equivalence F ≃ Σ(H : is_left_adjoint F), is_iso (unit F) × is_iso (counit F),
|
||||
{ fapply equiv.MK,
|
||||
{ intro H, induction H, fconstructor: constructor, repeat (esimp;assumption) },
|
||||
{ intro H, induction H with H1 H2, induction H1, induction H2, constructor,
|
||||
repeat (esimp at *;assumption)},
|
||||
{ intro H, induction H with H1 H2, induction H1, induction H2, reflexivity},
|
||||
{ intro H, induction H, reflexivity}},
|
||||
apply is_trunc_equiv_closed_rev, exact f,
|
||||
end
|
||||
|
||||
theorem is_hprop_fully_faithful [instance] (F : C ⇒ D) : is_hprop (fully_faithful F) :=
|
||||
by unfold fully_faithful; exact _
|
||||
|
||||
theorem is_hprop_full [instance] (F : C ⇒ D) : is_hprop (full F) :=
|
||||
by unfold full; exact _
|
||||
|
||||
theorem is_hprop_faithful [instance] (F : C ⇒ D) : is_hprop (faithful F) :=
|
||||
by unfold faithful; exact _
|
||||
|
||||
theorem is_hprop_essentially_surjective [instance] (F : C ⇒ D)
|
||||
: is_hprop (essentially_surjective F) :=
|
||||
by unfold essentially_surjective; exact _
|
||||
|
||||
theorem is_hprop_is_weak_equivalence [instance] (F : C ⇒ D) : is_hprop (is_weak_equivalence F) :=
|
||||
by unfold is_weak_equivalence; exact _
|
||||
|
||||
theorem is_hprop_is_isomorphism [instance] (F : C ⇒ D) : is_hprop (is_isomorphism F) :=
|
||||
by unfold is_isomorphism; exact _
|
||||
|
||||
definition fully_faithful_equiv (F : C ⇒ D) : fully_faithful F ≃ (faithful F × full F) :=
|
||||
sorry
|
||||
equiv_of_is_hprop (λH, (faithful_of_fully_faithful H, full_of_fully_faithful H))
|
||||
(λH, fully_faithful_of_full_of_faithful (pr1 H) (pr2 H))
|
||||
|
||||
/- alternative proof using direct calculation with equivalences
|
||||
|
||||
definition fully_faithful_equiv (F : C ⇒ D) : fully_faithful F ≃ (faithful F × full F) :=
|
||||
calc
|
||||
fully_faithful F
|
||||
≃ (Π(c c' : C), is_embedding (to_fun_hom F) × is_surjective (to_fun_hom F))
|
||||
: pi_equiv_pi_id (λc, pi_equiv_pi_id
|
||||
(λc', !is_equiv_equiv_is_embedding_times_is_surjective))
|
||||
... ≃ (Π(c : C), (Π(c' : C), is_embedding (to_fun_hom F)) ×
|
||||
(Π(c' : C), is_surjective (to_fun_hom F)))
|
||||
: pi_equiv_pi_id (λc, !equiv_prod_corec)
|
||||
... ≃ (Π(c c' : C), is_embedding (to_fun_hom F)) × full F
|
||||
: equiv_prod_corec
|
||||
... ≃ faithful F × full F
|
||||
: prod_equiv_prod_right (pi_equiv_pi_id (λc, pi_equiv_pi_id
|
||||
(λc', !is_embedding_equiv_is_injective)))
|
||||
-/
|
||||
|
||||
/- closure properties -/
|
||||
|
||||
definition is_isomorphism_id [instance] (C : Precategory) : is_isomorphism (1 : C ⇒ C) :=
|
||||
is_isomorphism.mk 1 !functor.id_right !functor.id_right
|
||||
|
||||
definition is_isomorphism_strict_inverse (F : C ⇒ D) [K : is_isomorphism F]
|
||||
: is_isomorphism F⁻¹ˢ :=
|
||||
is_isomorphism.mk F !strict_right_inverse !strict_left_inverse
|
||||
|
||||
definition is_isomorphism_compose (G : D ⇒ E) (F : C ⇒ D)
|
||||
[H : is_isomorphism G] [K : is_isomorphism F] : is_isomorphism (G ∘f F) :=
|
||||
is_isomorphism.mk
|
||||
(F⁻¹ˢ ∘f G⁻¹ˢ)
|
||||
abstract begin
|
||||
rewrite [functor.assoc,-functor.assoc F⁻¹ˢ,strict_left_inverse,functor.id_right,
|
||||
strict_left_inverse]
|
||||
end end
|
||||
abstract begin
|
||||
rewrite [functor.assoc,-functor.assoc G,strict_right_inverse,functor.id_right,
|
||||
strict_right_inverse]
|
||||
end end
|
||||
|
||||
definition is_equivalence_id (C : Precategory) : is_equivalence (1 : C ⇒ C) := _
|
||||
|
||||
definition is_equivalence_strict_inverse (F : C ⇒ D) [K : is_equivalence F]
|
||||
: is_equivalence F ⁻¹F :=
|
||||
is_equivalence.mk F (iso_counit F) (iso_unit F)
|
||||
|
||||
/-
|
||||
definition is_equivalence_compose (G : D ⇒ E) (F : C ⇒ D)
|
||||
[H : is_equivalence G] [K : is_equivalence F] : is_equivalence (G ∘f F) :=
|
||||
is_equivalence.mk
|
||||
(F ⁻¹F ∘f G ⁻¹F)
|
||||
abstract begin
|
||||
rewrite [functor.assoc,-functor.assoc F ⁻¹F],
|
||||
-- refine ((_ ∘fi _) ∘if _) ⬝i _,
|
||||
end end
|
||||
abstract begin
|
||||
rewrite [functor.assoc,-functor.assoc G,strict_right_inverse,functor.id_right,
|
||||
strict_right_inverse]
|
||||
end end
|
||||
|
||||
definition is_equivalence_equiv (F : C ⇒ D)
|
||||
: is_equivalence F ≃ (fully_faithful F × split_essentially_surjective F) :=
|
||||
sorry
|
||||
|
||||
definition is_hprop_is_weak_equivalence (F : C ⇒ D) : is_hprop (is_weak_equivalence F) :=
|
||||
sorry
|
||||
|
||||
definition is_hprop_is_equivalence {C D : Category} (F : C ⇒ D) : is_hprop (is_equivalence F) :=
|
||||
sorry
|
||||
|
||||
definition is_equivalence_equiv_is_weak_equivalence {C D : Category} (F : C ⇒ D)
|
||||
: is_equivalence F ≃ is_weak_equivalence F :=
|
||||
sorry
|
||||
|
||||
definition is_hprop_is_isomorphism (F : C ⇒ D) : is_hprop (is_isomorphism F) :=
|
||||
sorry
|
||||
|
||||
definition is_isomorphism_equiv1 (F : C ⇒ D) : is_equivalence F
|
||||
≃ Σ(G : D ⇒ C) (η : 1 = G ∘f F) (ε : F ∘f G = 1),
|
||||
sorry ▸ ap (λ(H : C ⇒ C), F ∘f H) η = ap (λ(H : D ⇒ D), H ∘f F) ε⁻¹ :=
|
||||
|
|
@ -426,10 +512,6 @@ namespace category
|
|||
≃ ∃(G : D ⇒ C), 1 = G ∘f F × F ∘f G = 1 :=
|
||||
sorry
|
||||
|
||||
definition is_isomorphism_of_is_equivalence {C D : Category} {F : C ⇒ D} (H : is_equivalence F)
|
||||
: is_isomorphism F :=
|
||||
sorry
|
||||
|
||||
definition isomorphism_of_eq {C D : Precategory} (p : C = D) : C ≅c D :=
|
||||
sorry
|
||||
|
||||
|
|
@ -439,7 +521,16 @@ namespace category
|
|||
definition equivalence_of_eq {C D : Precategory} (p : C = D) : C ≃c D :=
|
||||
sorry
|
||||
|
||||
definition is_isomorphism_of_is_equivalence {C D : Category} {F : C ⇒ D} (H : is_equivalence F)
|
||||
: is_isomorphism F :=
|
||||
sorry
|
||||
|
||||
definition is_equivalence_equiv_is_weak_equivalence {C D : Category} (F : C ⇒ D)
|
||||
: is_equivalence F ≃ is_weak_equivalence F :=
|
||||
sorry
|
||||
|
||||
definition is_equiv_equivalence_of_eq (C D : Category) : is_equiv (@equivalence_of_eq C D) :=
|
||||
sorry
|
||||
|
||||
-/
|
||||
end category
|
||||
|
|
|
|||
|
|
@ -75,11 +75,22 @@ namespace function
|
|||
{intro p, apply is_hset.elim},
|
||||
{intro p, apply is_hset.elim}
|
||||
end
|
||||
|
||||
variable (f)
|
||||
|
||||
definition is_hprop_is_embedding [instance] : is_hprop (is_embedding f) :=
|
||||
by unfold is_embedding; exact _
|
||||
|
||||
definition is_embedding_equiv_is_injective [HA : is_hset A] [HB : is_hset B]
|
||||
: is_embedding f ≃ (Π(a a' : A), f a = f a' → a = a') :=
|
||||
begin
|
||||
fapply equiv.MK,
|
||||
{ apply @is_injective_of_is_embedding},
|
||||
{ apply is_embedding_of_is_injective},
|
||||
{ intro H, apply is_hprop.elim},
|
||||
{ intro H, apply is_hprop.elim, }
|
||||
end
|
||||
|
||||
definition is_hprop_fiber_of_is_embedding [H : is_embedding f] (b : B) :
|
||||
is_hprop (fiber f b) :=
|
||||
begin
|
||||
|
|
|
|||
|
|
@ -346,6 +346,7 @@ order for the change to take effect."
|
|||
("-1o" . ("⁻¹ᵒ"))
|
||||
("-1r" . ("⁻¹ʳ"))
|
||||
("-1p" . ("⁻¹ᵖ"))
|
||||
("-1s" . ("⁻¹ˢ"))
|
||||
("-1v" . ("⁻¹ᵛ"))
|
||||
("-2" . ("⁻²"))
|
||||
("-2o" . ("⁻²ᵒ"))
|
||||
|
|
|
|||
Loading…
Reference in a new issue