diff --git a/theories/Algebra/AbGroups/AbelianGroup.v b/theories/Algebra/AbGroups/AbelianGroup.v
index ebfaa94ce21..3cc11246bed 100644
--- a/theories/Algebra/AbGroups/AbelianGroup.v
+++ b/theories/Algebra/AbGroups/AbelianGroup.v
@@ -94,26 +94,29 @@ Defined.
 (** ** The wild category of abelian groups *)
 
 Global Instance isgraph_abgroup : IsGraph AbGroup
-  := induced_graph abgroup_group.
+  := isgraph_induced abgroup_group.
 
-Global Instance is01cat_AbGroup : Is01Cat AbGroup
-  := induced_01cat abgroup_group.
+Global Instance is01cat_abgroup : Is01Cat AbGroup
+  := is01cat_induced abgroup_group.
 
-Global Instance is01cat_GroupHomomorphism {A B : AbGroup} : Is01Cat (A $-> B)
-  := induced_01cat (@grp_homo_map A B).
+Global Instance is01cat_grouphomomorphism {A B : AbGroup} : Is01Cat (A $-> B)
+  := is01cat_induced (@grp_homo_map A B).
 
-Global Instance is0gpd_GroupHomomorphism {A B : AbGroup}: Is0Gpd (A $-> B)
-  := induced_0gpd (@grp_homo_map A B).
+Global Instance is0gpd_grouphomomorphism {A B : AbGroup} : Is0Gpd (A $-> B)
+  := is0gpd_induced (@grp_homo_map A B).
+
+Global Instance is2graph_abgroup : Is2Graph AbGroup
+  := is2graph_induced abgroup_group.
 
 (** AbGroup forms a 1Cat *)
 Global Instance is1cat_abgroup : Is1Cat AbGroup
-  := induced_1cat _.
+  := is1cat_induced _.
 
 Global Instance hasmorext_abgroup `{Funext} : HasMorExt AbGroup
-  := induced_hasmorext _.
+  := hasmorext_induced _.
 
 Global Instance hasequivs_abgroup : HasEquivs AbGroup
-  := induced_hasequivs _.
+  := hasequivs_induced _.
 
 (** Zero object of AbGroup *)
 
diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v
index e6171c68b4e..721c3df3e4c 100644
--- a/theories/Algebra/Groups/Group.v
+++ b/theories/Algebra/Groups/Group.v
@@ -468,14 +468,17 @@ Global Instance isgraph_group : IsGraph Group
 Global Instance is01cat_group : Is01Cat Group :=
   (Build_Is01Cat Group _ (@grp_homo_id) (@grp_homo_compose)).
 
+Global Instance is2graph_group : Is2Graph Group
+  := fun A B => isgraph_induced (@grp_homo_map A B).
+
 Global Instance isgraph_grouphomomorphism {A B : Group} : IsGraph (A $-> B)
-  := induced_graph (@grp_homo_map A B).
+  := isgraph_induced (@grp_homo_map A B).
 
 Global Instance is01cat_grouphomomorphism {A B : Group} : Is01Cat (A $-> B)
-  := induced_01cat (@grp_homo_map A B).
+  := is01cat_induced (@grp_homo_map A B).
 
 Global Instance is0gpd_grouphomomorphism {A B : Group}: Is0Gpd (A $-> B)
-  := induced_0gpd (@grp_homo_map A B).
+  := is0gpd_induced (@grp_homo_map A B).
 
 Global Instance is0functor_postcomp_grouphomomorphism {A B C : Group} (h : B $-> C)
   : Is0Functor (@cat_postcomp Group _ _ A B C h).
diff --git a/theories/Algebra/Rings/CRing.v b/theories/Algebra/Rings/CRing.v
index fbca8dc9ed5..a750aad3beb 100644
--- a/theories/Algebra/Rings/CRing.v
+++ b/theories/Algebra/Rings/CRing.v
@@ -235,14 +235,14 @@ Global Instance isgraph_cring : IsGraph CRing
 Global Instance is01cat_cring : Is01Cat CRing
   := Build_Is01Cat _ _ rng_homo_id (@rng_homo_compose).
 
-Global Instance isgraph_cringhomomorphism {A B : CRing} : IsGraph (A $-> B)
-  := induced_graph (@rng_homo_map A B).
+Global Instance is2graph_cring : Is2Graph CRing
+  := fun A B => isgraph_induced (@rng_homo_map A B).
 
 Global Instance is01cat_cringhomomorphism {A B : CRing} : Is01Cat (A $-> B)
-  := induced_01cat (@rng_homo_map A B).
+  := is01cat_induced (@rng_homo_map A B).
 
-Global Instance is0gpd_cringhomomorphism {A B : CRing}: Is0Gpd (A $-> B)
-  := induced_0gpd (@rng_homo_map A B).
+Global Instance is0gpd_cringhomomorphism {A B : CRing} : Is0Gpd (A $-> B)
+  := is0gpd_induced (@rng_homo_map A B).
 
 Global Instance is0functor_postcomp_cringhomomorphism {A B C : CRing} (h : B $-> C)
   : Is0Functor (@cat_postcomp CRing _ _ A B C h).
diff --git a/theories/Algebra/Universal/Homomorphism.v b/theories/Algebra/Universal/Homomorphism.v
index 631ddbaa056..e43941c5040 100644
--- a/theories/Algebra/Universal/Homomorphism.v
+++ b/theories/Algebra/Universal/Homomorphism.v
@@ -145,9 +145,9 @@ Proof.
   by apply path_homomorphism.
 Defined.
 
-Global Instance isgraph_homomorphism {σ} (A B : Algebra σ)
-  : IsGraph (A $-> B)
-  := Build_IsGraph _ (fun (f g : A $-> B) => forall s, f s == g s).
+Global Instance is2graph_algebra {σ} : Is2Graph (Algebra σ)
+  := fun A B
+    => Build_IsGraph _ (fun (f g : A $-> B) => forall s, f s == g s).
 
 Global Instance is01cat_homomorphism {σ} (A B : Algebra σ)
   : Is01Cat (A $-> B).
diff --git a/theories/Algebra/ooGroup.v b/theories/Algebra/ooGroup.v
index 25ac54e18f2..14c1ed85d6e 100644
--- a/theories/Algebra/ooGroup.v
+++ b/theories/Algebra/ooGroup.v
@@ -289,9 +289,14 @@ End Subgroups.
 
 (** The wild category of oo-groups is induced by the wild category of pTypes *)
 
-Global Instance isgraph_oogroup : IsGraph ooGroup := Build_IsGraph _ ooGroupHom.
-Global Instance is01cat_oogroup : Is01Cat ooGroup := Build_Is01Cat _ _ grouphom_idmap (@grouphom_compose).
-Global Instance is1cat_oogroup : Is1Cat ooGroup := induced_1cat classifying_space.
+Global Instance isgraph_oogroup : IsGraph ooGroup
+  := Build_IsGraph _ ooGroupHom.
+Global Instance is01cat_oogroup : Is01Cat ooGroup
+  := Build_Is01Cat _ _ grouphom_idmap (@grouphom_compose).
+Global Instance is2graph_oogroup : Is2Graph ooGroup
+  := is2graph_induced classifying_space.
+Global Instance is1cat_oogroup : Is1Cat ooGroup
+  := is1cat_induced classifying_space.
 
 (** ** 1-groups as oo-groups *)
 
diff --git a/theories/Homotopy/ExactSequence.v b/theories/Homotopy/ExactSequence.v
index 5b715330abb..2c88fc374df 100644
--- a/theories/Homotopy/ExactSequence.v
+++ b/theories/Homotopy/ExactSequence.v
@@ -90,7 +90,7 @@ Definition iscomplex_cancelR {F X Y Y' : pType}
            (i : F ->* X) (f : X ->* Y) (e : Y <~>* Y') (cx : IsComplex i (e o* f))
   : IsComplex i f :=
   (compose_V_hh e (f o* i))^$ $@ 
-    cat_postwhisker _ ((cat_assoc _ _ _)^$ $@ cx) $@ precompose_pconst _.
+    cat_postwhisker _ ((cat_assoc i _ _)^$ $@ cx) $@ precompose_pconst _.
 
 (** And likewise passage across squares with equivalences *)
 Definition iscomplex_equiv_i {F F' X X' Y : pType}
@@ -211,8 +211,10 @@ Proof.
   pose (I := isexact_equiv_i n i i' g h p f).
   pose (I2 := isexact_homotopic_f n i' q).
   exists (iscomplex_cancelR i' f' k cx_isexact).
-  pose (e := (pequiv_pfiber (id_cate _) k (cat_idr _)^$ : pfiber f' <~>* pfiber (k o* f'))).
-  nrefine (cancelR_isequiv_conn_map n _ e). 1: apply pointed_isequiv.
+  epose (e := (pequiv_pfiber (id_cate _) k (cat_idr (k o* f'))^$
+    : pfiber f' <~>* pfiber (k o* f'))).
+  nrefine (cancelR_isequiv_conn_map n _ e).
+  1: apply pointed_isequiv.
   refine (conn_map_homotopic n (cxfib (cx_isexact)) _ _ _).
   intro u. srapply path_hfiber.
   { reflexivity. }
diff --git a/theories/Pointed/Core.v b/theories/Pointed/Core.v
index 406aad6cd02..6678f626462 100644
--- a/theories/Pointed/Core.v
+++ b/theories/Pointed/Core.v
@@ -590,9 +590,16 @@ Global Instance is01cat_ptype : Is01Cat pType
   := Build_Is01Cat pType _ (@pmap_idmap) (@pmap_compose).
 
 (** pForall is a graph *)
-Global Instance isgraph_pforall (A : pType) (P : pFam A) : IsGraph (pForall A P)
+Global Instance isgraph_pforall (A : pType) (P : pFam A)
+  : IsGraph (pForall A P)
   := Build_IsGraph _ pHomotopy.
 
+Global Instance is2graph_ptype : Is2Graph pType := fun f g => _.
+
+Global Instance is2graph_pforall (A : pType) (P : pFam A)
+  : Is2Graph (pForall A P)
+  := fun f g => _.
+
 (** pForall is a 0-coherent 1-category *)
 Global Instance is01cat_pforall (A : pType) (P : pFam A) : Is01Cat (pForall A P).
 Proof.
@@ -633,8 +640,9 @@ Defined.
 (** pType has equivalences *)
 Global Instance hasequivs_ptype : HasEquivs pType.
 Proof.
-  srapply (Build_HasEquivs _ _ _ _ pEquiv (fun A B f => IsEquiv f));
-    intros A B f; cbn; intros.
+  srapply (
+    Build_HasEquivs _ _ _ _ _ pEquiv (fun A B f => IsEquiv f));
+  intros A B f; cbn; intros.
   - exact f.
   - exact _.
   - exact (Build_pEquiv _ _ f _).
diff --git a/theories/Pointed/pEquiv.v b/theories/Pointed/pEquiv.v
index 1a17220fa2e..b56529c42d4 100644
--- a/theories/Pointed/pEquiv.v
+++ b/theories/Pointed/pEquiv.v
@@ -16,7 +16,7 @@ Proof.
 Defined.
 
 (* We can probably get rid of the following notation, and use ^-1$ instead. *)
-Notation "f ^-1*" := (@cate_inv pType _ _ _ hasequivs_ptype _ _ f) : pointed_scope.
+Notation "f ^-1*" := (@cate_inv pType _ _ _ _ hasequivs_ptype _ _ f) : pointed_scope.
 
 (* pointed equivalence is a symmetric relation *)
 Global Instance pequiv_symmetric : Symmetric pEquiv.
diff --git a/theories/WildCat/Core.v b/theories/WildCat/Core.v
index eba5b380c88..0bda1a7ebd9 100644
--- a/theories/WildCat/Core.v
+++ b/theories/WildCat/Core.v
@@ -71,13 +71,16 @@ Class Is0Functor {A B : Type} `{IsGraph A} `{IsGraph B} (F : A -> B)
 
 Arguments fmap {_ _ _ _} F {_ _ _} f.
 
+Class Is2Graph (A : Type) `{IsGraph A}
+  := isgraph_hom : forall (a b : A), IsGraph (a $-> b).
+Global Existing Instance isgraph_hom | 20.
+Typeclasses Transparent Is2Graph.
 
 (** ** Wild 1-categorical structures *)
-Class Is1Cat (A : Type) `{!IsGraph A, !Is01Cat A} :=
+Class Is1Cat (A : Type) `{!IsGraph A, !Is2Graph A, !Is01Cat A} :=
 {
-  isgraph_hom : forall (a b : A), IsGraph (a $-> b) ;
   is01cat_hom : forall (a b : A), Is01Cat (a $-> b) ;
-  isgpd_hom : forall (a b : A), Is0Gpd (a $-> b) ;
+  is0gpd_hom : forall (a b : A), Is0Gpd (a $-> b) ;
   is0functor_postcomp : forall (a b c : A) (g : b $-> c), Is0Functor (cat_postcomp a g) ;
   is0functor_precomp : forall (a b c : A) (f : a $-> b), Is0Functor (cat_precomp c f) ;
   cat_assoc : forall (a b c d : A) (f : a $-> b) (g : b $-> c) (h : c $-> d),
@@ -86,14 +89,13 @@ Class Is1Cat (A : Type) `{!IsGraph A, !Is01Cat A} :=
   cat_idr : forall (a b : A) (f : a $-> b), f $o Id a $== f;
 }.
 
-Global Existing Instance isgraph_hom.
 Global Existing Instance is01cat_hom.
-Global Existing Instance isgpd_hom.
+Global Existing Instance is0gpd_hom.
 Global Existing Instance is0functor_postcomp.
 Global Existing Instance is0functor_precomp.
-Arguments cat_assoc {_ _ _ _ _ _ _ _} f g h.
-Arguments cat_idl {_ _ _ _ _ _} f.
-Arguments cat_idr {_ _ _ _ _ _} f.
+Arguments cat_assoc {_ _ _ _ _ _ _ _ _} f g h.
+Arguments cat_idl {_ _ _ _ _ _ _} f.
+Arguments cat_idr {_ _ _ _ _ _ _} f.
 
 Definition cat_assoc_opp {A : Type} `{Is1Cat A}
            {a b c d : A} (f : a $-> b) (g : b $-> c) (h : c $-> d)
@@ -123,23 +125,24 @@ Definition cat_prewhisker {A} `{Is1Cat A} {a b c : A}
 Notation "p $@R h" := (cat_prewhisker p h).
 
 (** Often, the coherences are actually equalities rather than homotopies. *)
-Class Is1Cat_Strong (A : Type) `{Is01Cat A} := 
+Class Is1Cat_Strong (A : Type)`{!IsGraph A, !Is2Graph A, !Is01Cat A} := 
 {
-  isgraph_hom_strong : forall (a b : A), IsGraph (a $-> b) ;
   is01cat_hom_strong : forall (a b : A), Is01Cat (a $-> b) ;
-  isgpd_hom_strong : forall (a b : A), Is0Gpd (a $-> b) ;
-  is0functor_postcomp_strong : forall (a b c : A) (g : b $-> c), Is0Functor (cat_postcomp a g) ;
-  is0functor_precomp_strong : forall (a b c : A) (f : a $-> b), Is0Functor (cat_precomp c f) ;
+  is0gpd_hom_strong : forall (a b : A), Is0Gpd (a $-> b) ;
+  is0functor_postcomp_strong : forall (a b c : A) (g : b $-> c),
+    Is0Functor (cat_postcomp a g) ;
+  is0functor_precomp_strong : forall (a b c : A) (f : a $-> b),
+    Is0Functor (cat_precomp c f) ;
   cat_assoc_strong : forall (a b c d : A)
     (f : a $-> b) (g : b $-> c) (h : c $-> d),
-    (h $o g) $o f = h $o (g $o f);
-  cat_idl_strong : forall (a b : A) (f : a $-> b), Id b $o f = f;
-  cat_idr_strong : forall (a b : A) (f : a $-> b), f $o Id a = f;
+    (h $o g) $o f = h $o (g $o f) ;
+  cat_idl_strong : forall (a b : A) (f : a $-> b), Id b $o f = f ;
+  cat_idr_strong : forall (a b : A) (f : a $-> b), f $o Id a = f ;
 }.
 
-Arguments cat_assoc_strong {_ _ _ _ _ _ _ _} f g h.
-Arguments cat_idl_strong {_ _ _ _ _ _} f.
-Arguments cat_idr_strong {_ _ _ _ _ _} f.
+Arguments cat_assoc_strong {_ _ _ _ _ _ _ _ _} f g h.
+Arguments cat_idl_strong {_ _ _ _ _ _ _} f.
+Arguments cat_idr_strong {_ _ _ _ _ _ _} f.
 
 Definition cat_assoc_opp_strong {A : Type} `{Is1Cat_Strong A}
            {a b c d : A} (f : a $-> b) (g : b $-> c) (h : c $-> d)
@@ -151,9 +154,8 @@ Global Instance is1cat_is1cat_strong (A : Type) `{Is1Cat_Strong A}
 Proof.
   srapply Build_Is1Cat.
   all: intros a b.
-  - apply isgraph_hom_strong.
   - apply is01cat_hom_strong.
-  - apply isgpd_hom_strong.
+  - apply is0gpd_hom_strong.
   - apply is0functor_postcomp_strong.
   - apply is0functor_precomp_strong.
   - intros; apply GpdHom_path, cat_assoc_strong.
@@ -203,9 +205,9 @@ Class Is1Functor {A B : Type} `{Is1Cat A} `{Is1Cat B}
     fmap F (g $o f) $== fmap F g $o fmap F f;
 }.
 
-Arguments fmap2 {A B _ _ _ _ _ _} F {_ _ _ _ _ _} p.
-Arguments fmap_id {A B _ _ _ _ _ _} F {_ _} a.
-Arguments fmap_comp {A B _ _ _ _ _ _} F {_ _ _ _ _} f g.
+Arguments fmap2 {A B _ _ _ _ _ _ _ _} F {_ _ _ _ _ _} p.
+Arguments fmap_id {A B _ _ _ _ _ _ _ _} F {_ _} a.
+Arguments fmap_comp {A B _ _ _ _ _ _ _ _} F {_ _ _ _ _} f g.
 
 (** Identity functor *)
 
@@ -352,3 +354,9 @@ Proof.
   apply gpd_moveL_V1.
   refine (cat_assoc _ _ _ $@ (f $@L gpd_h_Vh g f^$) $@ gpd_isretr f).
 Defined.
+
+Class Is3Graph (A : Type) `{Is2Graph A}
+  := isgraph_hom_hom : forall (a b : A), Is2Graph (a $-> b).
+Global Existing Instance isgraph_hom_hom | 30.
+Typeclasses Transparent Is3Graph.
+
diff --git a/theories/WildCat/EmptyCat.v b/theories/WildCat/EmptyCat.v
index 8e43c33b52c..7a94753cf4f 100644
--- a/theories/WildCat/EmptyCat.v
+++ b/theories/WildCat/EmptyCat.v
@@ -18,6 +18,12 @@ Proof.
   constructor; intros [].
 Defined.
 
+Global Instance is2graph_empty : Is2Graph Empty.
+Proof.
+  intros f g.
+  by apply Build_IsGraph.
+Defined.
+
 Global Instance is1cat_empty : Is1Cat Empty.
 Proof.
   snrapply Build_Is1Cat; intros [].
diff --git a/theories/WildCat/Equiv.v b/theories/WildCat/Equiv.v
index 660f11ae254..a70725031cb 100644
--- a/theories/WildCat/Equiv.v
+++ b/theories/WildCat/Equiv.v
@@ -31,7 +31,7 @@ Class HasEquivs (A : Type) `{Is1Cat A} :=
 (** Since apparently a field of a record can't be the source of a coercion (Coq complains about the uniform inheritance condition, although as officially stated that condition appears to be satisfied), we redefine all the fields of [HasEquivs]. *)
 
 Definition CatEquiv {A} `{HasEquivs A} (a b : A)
-  := @CatEquiv' A _ _ _ _ a b.
+  := @CatEquiv' A _ _ _ _ _ a b.
 
 Notation "a $<~> b" := (CatEquiv a b).
 Infix "≅" := CatEquiv : wc_iso_scope.
@@ -39,7 +39,7 @@ Arguments CatEquiv : simpl never.
 
 Definition cate_fun {A} `{HasEquivs A} {a b : A} (f : a $<~> b)
   : a $-> b
-  := @cate_fun' A _ _ _ _ a b f.
+  := @cate_fun' A _ _ _ _ _ a b f.
 
 Coercion cate_fun : CatEquiv >-> Hom.
 
@@ -71,7 +71,7 @@ Definition cate_adjointify {A} `{HasEquivs A} {a b : A}
            (f : a $-> b) (g : b $-> a)
            (r : f $o g $== Id b) (s : g $o f $== Id a)
   : a $<~> b
-  := @Build_CatEquiv _ _ _ _ _ a b f (catie_adjointify f g r s).
+  := @Build_CatEquiv _ _ _ _ _ _ a b f (catie_adjointify f g r s).
 
 (** This one we define to construct the whole inverse equivalence. *)
 Definition cate_inv {A} `{HasEquivs A} {a b : A} (f : a $<~> b) : b $<~> a.
@@ -111,11 +111,11 @@ Definition id_cate {A} `{HasEquivs A} (a : A)
   := Build_CatEquiv (Id a).
 
 Global Instance reflexive_cate {A} `{HasEquivs A}
-  : Reflexive (@CatEquiv A _ _ _ _)
+  : Reflexive (@CatEquiv A _ _ _ _ _)
   := id_cate.
 
 Global Instance symmetric_cate {A} `{HasEquivs A}
-  : Symmetric (@CatEquiv A _ _ _ _)
+  : Symmetric (@CatEquiv A _ _ _ _ _)
   := fun a b f => cate_inv f.
 
 (** Equivalences can be composed. *)
@@ -185,7 +185,7 @@ Proof.
 Defined.
 
 Global Instance transitive_cate {A} `{HasEquivs A}
-  : Transitive (@CatEquiv A _ _ _ _)
+  : Transitive (@CatEquiv A _ _ _ _ _)
   := fun a b c f g => g $oE f.
 
 (** Some more convenient equalities for equivalences. The naming scheme is similar to [PathGroupoids.v].*)
@@ -231,7 +231,7 @@ Proof.
 Defined.
 
 Class IsUnivalent1Cat (A : Type) `{HasEquivs A}
-  := { isequiv_cat_equiv_path : forall a b, IsEquiv (@cat_equiv_path A _ _ _ _ a b) }.
+  := { isequiv_cat_equiv_path : forall a b, IsEquiv (@cat_equiv_path A _ _ _ _ _ a b) }.
 Global Existing Instance isequiv_cat_equiv_path.
 
 Definition cat_path_equiv {A : Type} `{IsUnivalent1Cat A} (a b : A)
@@ -258,9 +258,10 @@ Proof.
   - intros a b c ; apply compose_cate.
 Defined.
 
-Global Instance isgraph_core_hom {A : Type} `{HasEquivs A} (a b : core A)
-  : IsGraph (a $-> b).
+Global Instance is2graph_core {A : Type} `{HasEquivs A}
+  : Is2Graph (core A).
 Proof.
+  intros a b.
   apply Build_IsGraph.
   intros f g ; exact (cate_fun f $== cate_fun g).
 Defined.
@@ -298,9 +299,11 @@ Global Instance is0functor_core_precomp {A : Type} `{HasEquivs A}
 Proof.
   apply Build_Is0Functor.
   intros f g al; cbn in h.
-  exact (compose_cate_fun f h
-           $@ (al $@R h)
+  (** Why can't coq resolve this? *)
+  refine (compose_cate_fun f h
+           $@ (_ $@R h)
            $@ (compose_cate_fun g h)^$).
+  exact al.
 Defined.
 
 Global Instance is1cat_core {A : Type} `{HasEquivs A}
diff --git a/theories/WildCat/Forall.v b/theories/WildCat/Forall.v
index 7149921e5bf..7f8cba81063 100644
--- a/theories/WildCat/Forall.v
+++ b/theories/WildCat/Forall.v
@@ -31,19 +31,20 @@ Proof.
   intros f g p a; exact ((p a)^$).
 Defined.
 
+Global Instance is2graph_forall (A : Type) (B : A -> Type)
+  `{forall a, IsGraph (B a)} `{forall a, Is2Graph (B a)}
+  : Is2Graph (forall a, B a).
+Proof.
+  intros x y; srapply Build_IsGraph.
+  intros f g; exact (forall a, f a $-> g a).
+Defined.
+
 Global Instance is1cat_forall (A : Type) (B : A -> Type)
   `{forall a, IsGraph (B a)} `{forall a, Is01Cat (B a)}
-  `{forall a, Is1Cat (B a)}
+  `{forall a, Is2Graph (B a)} `{forall a, Is1Cat (B a)}
   : Is1Cat (forall a, B a).
 Proof.
   srapply Build_Is1Cat.
-  + intros x y; srapply Build_IsGraph.
-    intros f g; exact (forall a, f a $== g a).
-  + intros x y; srapply Build_Is01Cat.
-    - intros f a; apply Id.
-    - intros f g h q p a; exact (p a $@ q a).
-  + intros x y; srapply Build_Is0Gpd.
-    intros f g p a; exact (gpd_rev (p a)).
   + intros x y z h; srapply Build_Is0Functor.
     intros f g p a.
     exact (h a $@L p a).
diff --git a/theories/WildCat/FunctorCat.v b/theories/WildCat/FunctorCat.v
index c42f9706133..2ab28f205ac 100644
--- a/theories/WildCat/FunctorCat.v
+++ b/theories/WildCat/FunctorCat.v
@@ -27,7 +27,7 @@ Proof.
   exact (NatTrans F G).
 Defined.
 
-Global Instance is0cat_fun01 (A B : Type) `{IsGraph A} `{Is1Cat B} : Is01Cat (Fun01 A B).
+Global Instance is01cat_fun01 (A B : Type) `{IsGraph A} `{Is1Cat B} : Is01Cat (Fun01 A B).
 Proof.
   srapply Build_Is01Cat.
   - intros [F ?]; cbn.
@@ -36,14 +36,19 @@ Proof.
     exists (trans_comp gamma alpha); exact _.
 Defined.
 
+Global Instance is2graph_fun01 (A B : Type) `{IsGraph A, Is1Cat B}
+  : Is2Graph (Fun01 A B).
+Proof.
+  intros [F ?] [G ?]; apply Build_IsGraph.
+  intros [alpha ?] [gamma ?].
+  exact (forall a, alpha a $== gamma a).
+Defined.
+
 (** In fact, in this case it is automatically also a 0-coherent 2-category and a 1-coherent 1-category, with a totally incoherent notion of 2-cell between 1-coherent natural transformations. *)
 
-Global Instance is0coh2cat_fun01 (A B : Type) `{IsGraph A} `{Is1Cat B} : Is1Cat (Fun01 A B).
+Global Instance is1cat_fun01 (A B : Type) `{IsGraph A} `{Is1Cat B} : Is1Cat (Fun01 A B).
 Proof.
   srapply Build_Is1Cat.
-  - intros [F ?] [G ?]; apply Build_IsGraph.
-    intros [alpha ?] [gamma ?].
-    exact (forall a, alpha a $== gamma a).
   - intros [F ?] [G ?]; srapply Build_Is01Cat.
     + intros [alpha ?] a; cbn.
       reflexivity.
@@ -127,16 +132,20 @@ Defined.
 
 Global Instance isgraph_fun11 {A B : Type} `{Is1Cat A} `{Is1Cat B}
   : IsGraph (Fun11 A B)
-  := induced_graph fun01_fun11.
+  := isgraph_induced fun01_fun11.
 
 Global Instance is01cat_fun11 {A B : Type} `{Is1Cat A} `{Is1Cat B}
   : Is01Cat (Fun11 A B)
-  := induced_01cat fun01_fun11.
+  := is01cat_induced fun01_fun11.
+
+Global Instance is2graph_fun11 {A B : Type} `{Is1Cat A, Is1Cat B}
+  : Is2Graph (Fun11 A B)
+  := is2graph_induced fun01_fun11.
 
 Global Instance is1cat_fun11 {A B :Type} `{Is1Cat A} `{Is1Cat B}
   : Is1Cat (Fun11 A B)
-  := induced_1cat fun01_fun11.
+  := is1cat_induced fun01_fun11.
 
 Global Instance hasequivs_fun11 {A B : Type} `{Is1Cat A} `{HasEquivs B}
   : HasEquivs (Fun11 A B)
-  := induced_hasequivs fun01_fun11.
+  := hasequivs_induced fun01_fun11.
diff --git a/theories/WildCat/Induced.v b/theories/WildCat/Induced.v
index 6bc34ce9b02..ac69f3a428e 100644
--- a/theories/WildCat/Induced.v
+++ b/theories/WildCat/Induced.v
@@ -13,14 +13,14 @@ This needs to be separate from Core because of HasEquivs usage.  We don't make t
 Section Induced_category.
   Context {A B : Type} (f : A -> B).
 
-  Local Instance induced_graph `{IsGraph B} : IsGraph A.
+  Local Instance isgraph_induced `{IsGraph B} : IsGraph A.
   Proof.
     srapply Build_IsGraph.
     intros a1 a2. 
     exact (f a1 $-> f a2).
   Defined.
 
-  Local Instance induced_01cat `{Is01Cat B} : Is01Cat A.
+  Local Instance is01cat_induced `{Is01Cat B} : Is01Cat A.
   Proof.
     srapply Build_Is01Cat.
     + intro a. cbn in *. 
@@ -29,37 +29,50 @@ Section Induced_category.
       exact ( g1 $o g2).
   Defined.
 
-  Local Instance induced_0gpd `{Is0Gpd B} : Is0Gpd A.
+  Local Instance is0gpd_induced `{Is0Gpd B} : Is0Gpd A.
   Proof.
     rapply Build_Is0Gpd.
     intros a b g; cbn in *; exact (g^$).
   Defined.
 
   (** The structure map along which we induce the category structure becomes a functor with respect to the induced structure *) 
-  Local Instance inducingmap_is0functor `{Is01Cat B} : Is0Functor f.
+  Local Instance is0functor_induced `{IsGraph B} : Is0Functor f.
   Proof.
     srapply Build_Is0Functor.
     intros a b. cbn in *. exact idmap.
   Defined.
 
-  Local Instance induced_1cat `{Is1Cat B} : Is1Cat A.
+  Local Instance is2graph_induced `{Is2Graph B} : Is2Graph A.
   Proof.
-    srapply Build_Is1Cat.
-    + intros a b. cbn in *. exact _.
-    + intros a b. cbn in *. exact _.
-    + intros a b. cbn in *. exact _.
-    + intros a b c. cbn in *. exact _.
+    intros a b.
+    srapply Build_IsGraph.
+    intros a1 a2.
+    exact (fmap f a1 $-> fmap f a2).
+  Defined.
+
+  Local Instance is1cat_induced `{Is1Cat B} : Is1Cat A.
+  Proof.
+    srapply Build_Is1Cat;
+      unfold isgraph_induced, is2graph_induced,
+        is01cat_induced, is0functor_induced in *;
+      cbn in *.
+    + intros a b.
+      rapply is01cat_hom.
+    + intros a b.
+      rapply is0gpd_hom.
+    + intros a b c.
+      rapply is0functor_postcomp.
     + intros a b c h.
-      exact (is0functor_precomp (f a) (f b) (f c) h).
-    + intros a b c d; cbn in *. 
-      intros u v w. apply cat_assoc.
-    + intros a b; cbn in *.
-      intros u. apply cat_idl.
-    + intros a b; cbn in *.
-      intros u. apply cat_idr.
+      rapply is0functor_precomp.
+    + intros a b c d u v w.
+      rapply cat_assoc.
+    + intros a b u.
+      rapply cat_idl.
+    + intros a b u.
+      apply cat_idr.
   Defined.
 
-  Local Instance inducingmap_is1functor `{Is1Cat B} : Is1Functor f.
+  Local Instance is1functor_induced `{Is1Cat B} : Is1Functor f.
   Proof.
     srapply Build_Is1Functor.
     + intros a b g h. cbn in *. exact idmap.
@@ -67,12 +80,12 @@ Section Induced_category.
     + intros a b c g h. cbn in *. exact (Id _). 
   Defined.
 
-  Instance induced_hasmorext `{X : HasMorExt B} : HasMorExt A.
+  Instance hasmorext_induced `{X : HasMorExt B} : HasMorExt A.
   Proof.
     constructor. intros. apply X.
   Defined.
 
-  Definition induced_hasequivs `{HasEquivs B} : HasEquivs A.
+  Definition hasequivs_induced `{HasEquivs B} : HasEquivs A.
   Proof.
     srapply Build_HasEquivs.
     + intros a b. exact (f a $<~> f b).
diff --git a/theories/WildCat/NatTrans.v b/theories/WildCat/NatTrans.v
index e4de75ce666..4b38ce91a14 100644
--- a/theories/WildCat/NatTrans.v
+++ b/theories/WildCat/NatTrans.v
@@ -17,7 +17,7 @@ Class Is1Natural {A B : Type} `{IsGraph A} `{Is1Cat B}
   isnat : forall a a' (f : a $-> a'),
      (alpha a') $o (fmap F f) $== (fmap G f) $o (alpha a).
 
-Arguments isnat {_ _ _ _ _ _ _ _ _ _} alpha {alnat _ _} f : rename.
+Arguments isnat {_ _ _ _ _ _ _ _ _ _ _} alpha {alnat _ _} f : rename.
 
 Record NatTrans {A B : Type} `{IsGraph A} `{Is1Cat B} (F G : A -> B)
   {ff : Is0Functor F} {fg : Is0Functor G} :=
diff --git a/theories/WildCat/Opposite.v b/theories/WildCat/Opposite.v
index 7eeef30eda8..b34f0b419fd 100644
--- a/theories/WildCat/Opposite.v
+++ b/theories/WildCat/Opposite.v
@@ -30,15 +30,19 @@ Section Op.
     + cbv; exact (fun a b c g f => f $o g).
   Defined.
 
+  (** We don't invert 2-cells as this is op on the first level. *)
+  Global Instance is2graph_op : Is2Graph A^op.
+  Proof.
+    intros a b; unfold op in *; cbn; exact _.
+  Defined.
+
   Global Instance is1cat_op : Is1Cat A^op.
   Proof.
     srapply Build_Is1Cat; unfold op in *; cbv in *.
-    - intros a b.
-      apply isgraph_hom.
     - intros a b.
       apply is01cat_hom.
     - intros a b.
-      apply isgpd_hom.
+      apply is0gpd_hom.
     - intros a b c h.
       srapply Build_Is0Functor.
       intros f g p.
@@ -67,12 +71,14 @@ Proof.
     apply cat_idl_strong.
 Defined.
 
-(* Opposites are definitionally involutive. You can test this by uncommenting the stuff below. *)
+(* Opposites are (almost) definitionally involutive. You can test this by uncommenting the stuff below. *)
+
 (*
-Definition test1 A {ac : Is01Cat A} : A = (A^op)^op := 1.
-Definition test2 A {ac : Is01Cat A} : ac = is01cat_op (A^op) := 1.
-Definition test3 A {ac : Is01Cat A} {ac2 : Is1Cat A} : ac2 = is1cat_op (A^op) := 1.
-Definition test4 A {ac : Is01Cat A} {ac2 : Is1Cat A} {ac11 : Is1Cat A} : ac11 = is1coh1cat_op (A^op) := 1.
+Definition test1 A `{Is01Cat A} : A = (A^op)^op := 1.
+Definition test2 A `{x : Is01Cat A} : x = is01cat_op (A^op) := 1.
+Definition test3 A `{x : Is2Graph A} : x = is2graph_op (A^op) := 1.
+(** Doesn't work *)
+Definition test4 A `{x : Is1Cat A} : x = is1cat_op (A^op) := 1.
 *)
 
 (** Opposite groupoids *)
@@ -111,7 +117,7 @@ Proof.
     apply is01cat_hom.
   - intros a b.
     apply is0coh1gpd_op.
-    apply isgpd_hom.
+    apply is0gpd_hom.
   - intros a b c.
     srapply Build_Is0Coh1Functor.
     intros [f g] [h k] [p q].
@@ -122,8 +128,8 @@ Defined.
 
 (** Opposite functors *)
 
-Global Instance is0coh1fun_op  A `{Is01Cat A} B `{Is01Cat B}
-       (F : A -> B) `{!Is0Functor F}
+Global Instance is0functor_op  A `{Is01Cat A} B `{Is01Cat B}
+       (F : A -> B) `{x : !Is0Functor F}
   : Is0Functor (F : A ^op -> B ^op).
 Proof.
   apply Build_Is0Functor.
@@ -134,12 +140,12 @@ Proof.
   assumption.
 Defined.
 
-Global Instance is0coh2fun_op A B `{Is1Cat A} `{Is1Cat B}
+Global Instance is1functor_op A B `{Is1Cat A} `{Is1Cat B}
        (F : A -> B) `{!Is0Functor F, !Is1Functor F}
   : Is1Functor (F : A^op -> B^op).
 Proof.
   apply Build_Is1Functor; unfold op in *; cbn in *.
-  - intros a b; apply fmap2; assumption.
+  - intros a b; rapply fmap2; assumption.
   - intros a; exact (fmap_id F a).
   - intros a b c f g; exact (fmap_comp F g f).
 Defined.
@@ -179,17 +185,17 @@ Proof.
   - apply cate_fun'.
   - apply cate_isequiv'.
   - apply cate_buildequiv'.
-  - apply cate_buildequiv_fun'.
+  - rapply cate_buildequiv_fun'.
   - apply cate_inv'.
-  - apply cate_isretr'.
-  - apply cate_issect'.
+  - rapply cate_isretr'.
+  - rapply cate_issect'.
   - intros f g s t.
     exact (catie_adjointify f g t s).
 Defined.
 
 Global Instance isequivs_op {A : Type} `{HasEquivs A}
        {a b : A} (f : a $-> b) {ief : CatIsEquiv f}
-  : @CatIsEquiv A^op _ _ _ _ b a f.
+  : @CatIsEquiv A^op _ _ _ _ _ b a f.
 Proof.
   assumption.
 Defined.
diff --git a/theories/WildCat/PointedCat.v b/theories/WildCat/PointedCat.v
index 7f0634081a3..c570c694404 100644
--- a/theories/WildCat/PointedCat.v
+++ b/theories/WildCat/PointedCat.v
@@ -29,7 +29,7 @@ Section ZeroLaws.
     := (isterminal_zero_object a).2 h
       $@ ((isterminal_zero_object a).2 zero_morphism)^$.
 
-  Local Arguments zero_morphism {_ _ _ _ _} _ _.
+  Local Arguments zero_morphism {_ _ _ _ _ _} _ _.
 
   Definition cat_zero_l : zero_morphism b c $o f $== zero_morphism a c.
   Proof.
diff --git a/theories/WildCat/Prod.v b/theories/WildCat/Prod.v
index db30f3eebd0..034f33950f1 100644
--- a/theories/WildCat/Prod.v
+++ b/theories/WildCat/Prod.v
@@ -36,20 +36,17 @@ Proof.
   exact ( (f1^$, f2^$) ).
 Defined.
 
+Global Instance is2graph_prod A B `{Is2Graph A, Is2Graph B}
+  : Is2Graph (A * B).
+Proof.
+  intros [x1 x2] [y1 y2].
+  rapply isgraph_prod.
+Defined.
+
 Global Instance is1cat_prod A B `{Is1Cat A} `{Is1Cat B}
   : Is1Cat (A * B).
 Proof.
   srapply (Build_Is1Cat).
-  - intros [x1 x2] [y1 y2].
-    rapply isgraph_prod.
-  - intros [x1 x2] [y1 y2].
-    rapply is01cat_prod.
-  - intros [x1 x2] [y1 y2].
-    apply is0gpd_prod.
-    + cbn.
-      apply isgpd_hom.
-    + cbn.
-      apply isgpd_hom.
   - intros [x1 x2] [y1 y2] [z1 z2] [h1 h2].
     srapply Build_Is0Functor.  
     intros [f1 f2] [g1 g2] [p1 p2]; cbn in *. 
@@ -75,7 +72,7 @@ Defined.
 Global Instance hasequivs_prod A B `{HasEquivs A} `{HasEquivs B}
   : HasEquivs (A * B).
 Proof.
-  srefine (Build_HasEquivs (A * B) _ _ _
+  srefine (Build_HasEquivs (A * B) _ _ _ _
              (fun a b => (fst a $<~> fst b) * (snd a $<~> snd b))
              _ _ _ _ _ _ _ _ _).
   1:intros a b f; exact (CatIsEquiv (fst f) * CatIsEquiv (snd f)).
@@ -97,7 +94,7 @@ Defined.
 Global Instance isequivs_prod A B `{HasEquivs A} `{HasEquivs B}
        {a1 a2 : A} {b1 b2 : B} {f : a1 $-> a2} {g : b1 $-> b2}
        {ef : CatIsEquiv f} {eg : CatIsEquiv g}
-  : @CatIsEquiv (A*B) _ _ _ _ (a1,b1) (a2,b2) (f,g) := (ef,eg).
+  : @CatIsEquiv (A*B) _ _ _ _ _ (a1,b1) (a2,b2) (f,g) := (ef,eg).
 
 (** More coherent two-variable functors. *)
 
@@ -106,16 +103,16 @@ Definition fmap22 {A B C : Type} `{Is1Cat A} `{Is1Cat B} `{Is1Cat C}
   {a1 a2 : A} {b1 b2 : B} (f1 : a1 $-> a2) (f2 : b1 $-> b2) (g1 : a1 $-> a2) (g2 : b1 $-> b2)
   (alpha : f1 $== g1) (beta : f2 $== g2)
   : (fmap11 F f1 f2) $== (fmap11 F g1 g2)
-  := @fmap2 _ _ _ _ _ _ _ _ (uncurry F) _ _ (a1, b1) (a2, b2) (f1, f2) (g1, g2) (alpha, beta).
+  := @fmap2 _ _ _ _ _ _ _ _ _ _ (uncurry F) _ _ (a1, b1) (a2, b2) (f1, f2) (g1, g2) (alpha, beta).
 
 Global Instance iemap11 {A B C : Type} `{HasEquivs A} `{HasEquivs B} `{HasEquivs C}
            (F : A -> B -> C) `{!Is0Functor (uncurry F), !Is1Functor (uncurry F)}
            {a1 a2 : A} {b1 b2 : B} (f1 : a1 $<~> a2) (f2 : b1 $<~> b2)
   : CatIsEquiv (fmap11 F f1 f2)
-  := @iemap _ _ _ _ _ _ _ _ _ _ (uncurry F) _ _ (a1, b1) (a2, b2) (f1, f2).
+  := @iemap _ _ _ _ _ _ _ _ _ _ _ _ (uncurry F) _ _ (a1, b1) (a2, b2) (f1, f2).
 
 Definition emap11 {A B C : Type} `{HasEquivs A} `{HasEquivs B} `{HasEquivs C}
            (F : A -> B -> C) `{!Is0Functor (uncurry F), !Is1Functor (uncurry F)}
            {a1 a2 : A} {b1 b2 : B} (fe1 : a1 $<~> a2)
            (fe2 : b1 $<~> b2) : (F a1 b1) $<~> (F a2 b2)
-  := @emap _ _ _ _ _ _ _ _ _ _ (uncurry F) _ _ (a1, b1) (a2, b2) (fe1, fe2).
+  := @emap _ _ _ _ _ _ _ _ _ _ _ _ (uncurry F) _ _ (a1, b1) (a2, b2) (fe1, fe2).
diff --git a/theories/WildCat/Sum.v b/theories/WildCat/Sum.v
index 3cd3d360766..adacf8debf2 100644
--- a/theories/WildCat/Sum.v
+++ b/theories/WildCat/Sum.v
@@ -25,14 +25,19 @@ Proof.
     try contradiction; cbn; apply cat_comp.
 Defined.
 
+Global Instance is2graph_sum A B `{Is2Graph A, Is2Graph B}
+  : Is2Graph (A + B).
+Proof.
+  intros x y; apply Build_IsGraph.
+  destruct x as [a1 | b1], y as [a2 | b2];
+  try contradiction; cbn; apply Hom.
+Defined.
+
 (* Note: [try contradiction] deals with empty cases. *)
 Global Instance is1cat_sum A B `{ Is1Cat A } `{ Is1Cat B}
   : Is1Cat (A + B).
 Proof.
   srapply Build_Is1Cat.
-  - intros x y; apply Build_IsGraph.
-    destruct x as [a1 | b1], y as [a2 | b2];
-    try contradiction; cbn; apply Hom.
   - intros x y.
     srapply Build_Is01Cat;
     destruct x as [a1 | b1], y as [a2 | b2];
diff --git a/theories/WildCat/TwoOneCat.v b/theories/WildCat/TwoOneCat.v
index 4fb274ff73a..5f9e77d600e 100644
--- a/theories/WildCat/TwoOneCat.v
+++ b/theories/WildCat/TwoOneCat.v
@@ -5,7 +5,7 @@ Require Import WildCat.NatTrans.
 
 (** * Wild (2,1)-categories *)
 
-Class Is21Cat (A : Type) `{Is1Cat A} :=
+Class Is21Cat (A : Type) `{Is1Cat A, !Is3Graph A} :=
 {
   is1cat_hom : forall (a b : A), Is1Cat (a $-> b) ;
   is1gpd_hom : forall (a b : A), Is1Gpd (a $-> b) ;
diff --git a/theories/WildCat/Type.v b/theories/WildCat/Type.v
index 5d0cf786b9e..b23e56ea966 100644
--- a/theories/WildCat/Type.v
+++ b/theories/WildCat/Type.v
@@ -14,8 +14,12 @@ Proof.
   + exact (fun a b c g f => g o f).
 Defined.
 
-Global Instance isgraph_arrow {A B : Type} : IsGraph (A $-> B)
-  := Build_IsGraph _ (fun f g => f == g).
+Global Instance is2graph_type : Is2Graph Type
+  := fun x y => Build_IsGraph _ (fun f g => f == g).
+
+(** Sometimes we need typeclasses to pick up that [A -> B] is a graph, but this cannot be done without first converting it to [A $-> B]. *)
+Global Instance isgraph_arrow {A B : Type} : IsGraph (A -> B)
+  := isgraph_hom A B.
 
 Global Instance is01cat_arrow {A B : Type} : Is01Cat (A $-> B).
 Proof.
@@ -60,7 +64,7 @@ Defined.
 
 Global Instance hasequivs_type : HasEquivs Type.
 Proof.
-  srefine (Build_HasEquivs Type _ _ _ Equiv (@IsEquiv) _ _ _ _ _ _ _ _); intros A B.
+  srefine (Build_HasEquivs Type _ _ _ _ Equiv (@IsEquiv) _ _ _ _ _ _ _ _); intros A B.
   all:intros f.
   - exact f.
   - exact _.
diff --git a/theories/WildCat/UnitCat.v b/theories/WildCat/UnitCat.v
index b63aaf952f3..7704bf2199a 100644
--- a/theories/WildCat/UnitCat.v
+++ b/theories/WildCat/UnitCat.v
@@ -20,6 +20,9 @@ Proof.
   constructor; intros; exact tt.
 Defined.
 
+Global Instance is2graph_unit : Is2Graph Unit
+  := fun f g => isgraph_unit.
+
 Global Instance is1cat_unit : Is1Cat Unit.
 Proof.
   econstructor.
diff --git a/theories/WildCat/Yoneda.v b/theories/WildCat/Yoneda.v
index 8663ef15318..c2db59fb452 100644
--- a/theories/WildCat/Yoneda.v
+++ b/theories/WildCat/Yoneda.v
@@ -21,12 +21,13 @@ Defined.
 
 (** This requires morphism extensionality! *)
 Global Instance is1functor_hom {A} `{HasMorExt A}
-  : @Is1Functor (A^op * A) Type _ _ _ _ _ _ (uncurry (@Hom A _)) _.
+  : @Is1Functor (A^op * A) Type _ _ _ _ _ _ _ _ (uncurry (@Hom A _)) _.
 Proof.
   apply Build_Is1Functor.
-  - intros [a1 a2] [b1 b2] [f1 f2] [g1 g2] [p1 p2] q; cbn in *.
+  - intros [a1 a2] [b1 b2] [f1 f2] [g1 g2] [p1 p2] q;
+      unfold fst, snd in *.
     apply path_hom.
-    exact (((p2 $@R q) $@R _) $@ (_ $@L p1)).
+    refine (((p2 $@R q) $@R _) $@ ((g2 $o q) $@L p1)).
   - intros [a1 a2] f; cbn in *.
     apply path_hom.
     exact (cat_idr _ $@ cat_idl f).
@@ -168,21 +169,21 @@ Definition un_yoneda {A : Type} `{Is01Cat A} (a : A)
 Global Instance is1natural_yoneda {A : Type} `{Is1Cat A} (a : A)
        (F : A^op -> Type) `{!Is0Functor F, !Is1Functor F} (x : F a)
   : Is1Natural (yon a) F (yoneda a F x)
-  := @is1natural_opyoneda (A^op) _ _ _ a F _ _ x.
+  := @is1natural_opyoneda (A^op) _ _ _ _ a F _ _ x.
 
 Definition yoneda_issect {A : Type} `{Is1Cat A} (a : A)
            (F : A^op -> Type) `{!Is0Functor F, !Is1Functor F} (x : F a)
   : un_yoneda a F (yoneda a F x) = x
-  := @opyoneda_issect (A^op) _ _ _ a F _ _ x.
+  := @opyoneda_issect (A^op) _ _ _ _ a F _ _ x.
 
 Definition yoneda_isretr {A : Type} `{Is1Cat_Strong A} (a : A)
            (F : A^op -> Type) `{!Is0Functor F}
            (* Without the hint here, Coq guesses to first project from [Is1Cat_Strong A] and then pass to opposites, whereas what we need is to first pass to opposites and then project. *)
-           `{@Is1Functor _ _ _ _ (is1cat_is1cat_strong A^op) _ _ _ F _}
+           `{@Is1Functor _ _ _ _ _ (is1cat_is1cat_strong A^op) _ _ _ _ F _}
            (alpha : yon a $=> F) {alnat : Is1Natural (yon a) F alpha}
            (b : A)
   : yoneda a F (un_yoneda a F alpha) b $== alpha b
-  := @opyoneda_isretr A^op _ _ (is1cat_strong_op A) a F _ _ alpha alnat b.
+  := @opyoneda_isretr A^op _ _ _ (is1cat_strong_op A) a F _ _ alpha alnat b.
 
 Definition yon_cancel {A : Type} `{Is01Cat A} (a b : A)
   : (yon a $=> yon b) -> (a $-> b)
@@ -194,5 +195,5 @@ Definition yon1 {A : Type} `{Is01Cat A} (a : A) : Fun01 A^op Type
 Definition yon_equiv {A : Type} `{HasEquivs A} `{!Is1Cat_Strong A}
            (a b : A)
   : (yon1 a $<~> yon1 b) -> (a $<~> b)
-  := (@opyon_equiv A^op _ _ _ _ _ a b).
+  := (@opyon_equiv A^op _ _ _ _ _ _ a b).