{A : Type} `{Is1Cat A} (a : A) : A -> ZeroGpd := fun b => Build_ZeroGpd (a $-> b) _ _ _. Global Instance is0functor_hom_0gpd {A : Type} `{Is1Cat A} : Is0Functor (A:=A^op*A) (B:=ZeroGpd) (uncurry ( (A:=A))). Proof. nrapply Build_Is0Functor. intros [a1 a2] [b1 b2] [f1 f2]; unfold op in *; cbn in *. rapply (Build_Morphism_0Gpd ( a1 a2) ( b1 b2) (cat_postcomp b1 f2 o cat_precomp a2 f1)). Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import WildCat.Universe. Require Import WildCat.Opposite. Require Import WildCat.FunctorCat. Require Import WildCat.NatTrans. Require Import WildCat.Prod. Require Import WildCat.Bifunctor. Require Import WildCat.ZeroGroupoid.