chore(library/hott): make constructions.lean compile, still lots of work to do

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
 

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
 

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}