michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(hott) remove duplicate lemma, make defs private, update book.md

Browse source
This commit is contained in:
Jakob von Raumer 2016-08-04 17:33:25 +02:00 committed by Leonardo de Moura
parent e79063970d
commit c81c86a9b8
3 changed files with 9 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
hott/algebra/category/constructions/functor.hlean
View file

@ -536,9 +536,9 @@ namespace functor
apply concat, apply !hom_inv_respect_comp⁻¹, apply ap (hom_inv H),
apply !assoc⁻¹ }
end
definition G0 [reducible] := λ (b), X.c (X_inh b)
definition k := λ b, X.k (X_inh b)
definition k_coh := λ b, @X.k_coh b (X_inh b)
local abbreviation G0 [reducible] := λ (b), X.c (X_inh b)
private definition k := λ b, X.k (X_inh b)
private definition k_coh := λ b, @X.k_coh b (X_inh b)
private definition X_c_eq_of_eq {b} (t t' : X b) (p : t = t') : X.c t = X.c t' :=
by cases p; reflexivity
@ -738,7 +738,7 @@ namespace functor
end essentially_surjective_precomposition
definition essentially_surjective_precomposition_functor {A B : Precategory}
definition essentially_surjective_precomposition_functor [instance] {A B : Precategory}
(C : Category) (H : A ⇒ B) [He : is_weak_equivalence H] :
essentially_surjective (precomposition_functor C H) :=
begin

24
hott/algebra/category/functor/attributes.hlean
View file

@ -84,36 +84,18 @@ namespace category
[H : fully_faithful F] (c c' : C) : (c ⟶ c') ≃ (F c ⟶ F c') :=
equiv.mk _ !H
definition iso_of_F_iso_F (F : C ⇒ D)
[H : fully_faithful F] (c c' : C) (g : F c ≅ F c') : c ≅ c' :=
begin
induction g with g G, induction G with h p q, fapply iso.MK,
{ rexact (to_fun_hom F)⁻¹ᶠ g},
{ rexact (to_fun_hom F)⁻¹ᶠ h},
{ exact abstract begin
apply eq_of_fn_eq_fn' (to_fun_hom F),
rewrite [respect_comp, respect_id,
right_inv (to_fun_hom F), right_inv (to_fun_hom F), p],
end end},
{ exact abstract begin
apply eq_of_fn_eq_fn' (to_fun_hom F),
rewrite [respect_comp, respect_id,
right_inv (to_fun_hom F), right_inv (@(to_fun_hom F) c' c), q],
end end}
end
definition iso_equiv_F_iso_F [constructor] (F : C ⇒ D)
[H : fully_faithful F] (c c' : C) : (c ≅ c') ≃ (F c ≅ F c') :=
begin
fapply equiv.MK,
{ exact to_fun_iso F},
{ apply iso_of_F_iso_F},
{ apply reflect_iso F},
{ exact abstract begin
intro f, induction f with f F', induction F' with g p q, apply iso_eq,
esimp [iso_of_F_iso_F], apply right_inv end end},
esimp [reflect_iso], apply right_inv end end},
{ exact abstract begin
intro f, induction f with f F', induction F' with g p q, apply iso_eq,
esimp [iso_of_F_iso_F], apply right_inv end end},
esimp [reflect_iso], apply right_inv end end},
end
definition full_of_fully_faithful [instance] (F : C ⇒ D) [H : fully_faithful F] : full F :=

4
hott/book.md
View file

@ -23,7 +23,7 @@ The rows indicate the chapters, the columns the sections.
| Ch 6 | . | + | + | + | + | + | + | + | ¾ | ¼ | ¾ | + | . | | |
| Ch 7 | + | + | + | - | ¾ | - | - | | | | | | | | |
| Ch 8 | + | + | + | + | + | ¾ | + | + | + | ¼ | | | | | |
| Ch 9 | ¾ | + | + | ½ | ¾ | ½ | - | - | ¾ | | | | | | |
| Ch 9 | ¾ | + | + | ½ | ¾ | ½ | - | - | + | | | | | | |
| Ch 10 | ¼ | - | - | - | - | | | | | | | | | | |
| Ch 11 | - | - | - | - | - | - | | | | | | | | | |
@ -169,7 +169,7 @@ Every file is in the folder [algebra.category](algebra/category/category.md)
- 9.6 (Strict categories): [strict](algebra/category/strict.hlean) (only definition)
- 9.7 (†-categories): not formalized
- 9.8 (The structure identity principle): not formalized
- 9.9 (The Rezk completion): [constructions.rezk](algebra/category/constructions/rezk.hlean), 9.9.1 and 9.9.2 in [constructions.functor](algebra/category/constructions/functor.hlean)
- 9.9 (The Rezk completion): [constructions.rezk](algebra/category/constructions/rezk.hlean), 9.9.1 to 9.9.4 in [constructions.functor](algebra/category/constructions/functor.hlean)
Chapter 10: Set theory
----------