{A B C J : Type} (f : TriJoinRecData A B C J) : NatTrans (opyon_0gpd J) (trijoinrecdata_0gpd_fun A B C). Proof. snrapply Build_NatTrans. - rapply opyoneda_0gpd; exact f. - exact _. Defined.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.