From 227de07758d3530f41853fdff57de6f9648ccfd4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 23 Mar 2015 11:32:20 -0700 Subject: [PATCH] fix(hott/algebra/category/constructions): avoid type class resolution loop --- hott/algebra/category/constructions.hlean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/hott/algebra/category/constructions.hlean b/hott/algebra/category/constructions.hlean index e337ab414b..7cbf702315 100644 --- a/hott/algebra/category/constructions.hlean +++ b/hott/algebra/category/constructions.hlean @@ -90,7 +90,7 @@ namespace category definition eq_of_iso_functor_ob (η : F ≅ G) (c : C) : F c = G c := by apply eq_of_iso; apply componentwise_iso; exact η - + local attribute functor.to_fun_hom [quasireducible] definition eq_of_iso_functor (η : F ≅ G) : F = G := begin fapply functor_eq,