diff --git a/library/hott/algebra/precategory/basic.lean b/library/hott/algebra/precategory/basic.lean
index 6b4aea2d7..60be71305 100644
--- a/library/hott/algebra/precategory/basic.lean
+++ b/library/hott/algebra/precategory/basic.lean
@@ -20,6 +20,7 @@ namespace precategory
   variables {ob : Type} [C : precategory ob]
   variables {a b c d : ob}
   include C
+  instance [persistent] homH
 
   definition compose := comp
 
diff --git a/library/hott/algebra/precategory/constructions.lean b/library/hott/algebra/precategory/constructions.lean
index 0ab7762cd..96c021ab8 100644
--- a/library/hott/algebra/precategory/constructions.lean
+++ b/library/hott/algebra/precategory/constructions.lean
@@ -127,12 +127,15 @@ namespace precategory
   namespace opposite
   section
   open ops functor
+  set_option pp.universes true
+
   definition opposite_functor {C D : Precategory} (F : C ⇒ D) : Cᵒᵖ ⇒ Dᵒᵖ :=
-  @functor.mk (Cᵒᵖ) (Dᵒᵖ)
-              (λ a, F a)
-              (λ a b f, F f)
-              (λ a, !respect_id)
-              (λ a b c g f, !respect_comp)
+  /-begin
+    apply (@functor.mk (Cᵒᵖ) (Dᵒᵖ)),
+      intro a, apply (respect_id F),
+      intros, apply (@respect_comp C D)
+  end-/ sorry
+
   end
   end opposite
 
diff --git a/library/hott/algebra/precategory/functor.lean b/library/hott/algebra/precategory/functor.lean
index 6da585f85..b717b04c1 100644
--- a/library/hott/algebra/precategory/functor.lean
+++ b/library/hott/algebra/precategory/functor.lean
@@ -15,7 +15,7 @@ mk : Π (obF : C → D) (homF : Π(a b : C), hom a b → hom (obF a) (obF b)),
 
 infixl `⇒`:25 := functor
 
--- I think we only have a precategory of stict catetories.
+-- I think we only have a precategory of stict categories.
 -- Maybe better implement this using univalence.
 namespace functor
   variables {C D E : Precategory}