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

fix(hott/algebra) comment unfinished proofs out for later completion

Browse source
This commit is contained in:
Jakob von Raumer 2015-01-03 15:17:18 -05:00 committed by Leonardo de Moura
parent 4de1a07324
commit e11c401d79
1 changed files with 4 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
hott/algebra/category/set.hlean
View file

@ -31,7 +31,6 @@ namespace category
universe variable l universe variable l
instance precategory.set_precategory.{l+1 l} instance precategory.set_precategory.{l+1 l}
check @equiv
definition set_category_equiv_iso (a b : (Σ (A : Type.{l}), is_hset A)) definition set_category_equiv_iso (a b : (Σ (A : Type.{l}), is_hset A))
: (a ≅ b) = (a.1 ≃ b.1) := : (a ≅ b) = (a.1 ≃ b.1) :=
/-begin /-begin
@ -48,12 +47,12 @@ namespace category
end-/ sorry end-/ sorry
definition set_category : category.{l+1 l} (Σ (A : Type.{l}), is_hset A) := definition set_category : category.{l+1 l} (Σ (A : Type.{l}), is_hset A) :=
begin /-begin
assert (C : precategory.{l+1 l} (Σ (A : Type.{l}), is_hset A)), assert (C : precategory.{l+1 l} (Σ (A : Type.{l}), is_hset A)),
apply precategory.set_precategory, apply precategory.set_precategory,
apply category.mk, apply category.mk,
assert (p : (λ A B p, (set_category_equiv_iso A B) ▹ iso_of_path p) = (λ A B p, @equiv_path A.1 B.1 p)), assert (p : (λ A B p, (set_category_equiv_iso A B) ▹ iso_of_path p) = (λ A B p, @equiv_path A.1 B.1 p)),
/-apply is_equiv.adjointify, apply is_equiv.adjointify,
intros, intros,
apply (isomorphic.rec_on a_1), intros (iso', is_iso'), apply (isomorphic.rec_on a_1), intros (iso', is_iso'),
apply (is_iso.rec_on is_iso'), intros (f', f'sect, f'retr), apply (is_iso.rec_on is_iso'), intros (f', f'sect, f'retr),
@ -65,7 +64,7 @@ namespace category
intros, apply (f'sect ▹ _), intros, apply (f'sect ▹ _),
apply (@is_hprop.elim), apply (@is_hprop.elim),
apply is_trunc_is_hprop, apply is_trunc_is_hprop,
intros, -/ intros,
end end -/ sorry
end category end category