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

fix(functor.equivalence): comment out sorry's

Browse source
This commit is contained in:
Floris van Doorn 2015-10-27 23:17:24 -04:00 committed by Leonardo de Moura
parent 49cb516c71
commit 5e4441cb43
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/algebra/category/functor/equivalence.hlean
View file

@ -367,6 +367,7 @@ namespace category
: c ⟶ c' ≃ H c ⟶ H c' :=
equiv.mk (to_fun_hom (isomorphism.to_functor H)) _
/- TODO
definition is_equiv_isomorphism_of_eq [constructor] (C D : Precategory)
: is_equiv (@isomorphism_of_eq C D) :=
begin
@ -391,7 +392,6 @@ namespace category
definition eq_equiv_equivalence [constructor] (C D : Category) : (C = D) ≃ (C ≃c D) :=
!eq_equiv_isomorphism ⬝e !isomorphism_equiv_equivalence
/- TODO
definition is_equivalence_equiv [constructor] (F : C ⇒ D)
: is_equivalence F ≃ (fully_faithful F × split_essentially_surjective F) :=
sorry