From 5e4441cb43702c845df21f1ba417a08eb747daf3 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 27 Oct 2015 23:17:24 -0400 Subject: [PATCH] fix(functor.equivalence): comment out sorry's --- hott/algebra/category/functor/equivalence.hlean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/hott/algebra/category/functor/equivalence.hlean b/hott/algebra/category/functor/equivalence.hlean index dbbf21df03..8b7e520efc 100644 --- a/hott/algebra/category/functor/equivalence.hlean +++ b/hott/algebra/category/functor/equivalence.hlean @@ -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