(A B C P : Type) : ZeroGpd := Build_ZeroGpd (TriJoinRecData A B C P) _ _ _. Global Instance is0functor_trijoinrecdata_fun {A B C P Q : Type} (g : P -> Q) : Is0Functor (@trijoinrecdata_fun A B C P Q g). Proof. apply Build_Is0Functor. intros f1 f2 h. snrapply Build_TriJoinRecPath; intros; cbn. 1, 2, 3: apply (ap g). 1: apply (h1 h). 1: apply (h2 h). 1: apply (h3 h). 1, 2, 3: refine ((ap_pp g _ _)^ @ _ @ ap_pp g _ _); apply (ap (ap g)). 1: apply (h12 h). 1: apply (h13 h). 1: apply (h23 h). prism_ind f2 h a b c. triangle_ind f1 a b c; cbn. reflexivity. Defined.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.