(A B C : Type) : NatEquiv (opyon_0gpd (TriJoin A B C)) (trijoinrecdata_0gpd_fun A B C). Proof. snrapply Build_NatEquiv'. 1: apply trijoin_rec_inv_nattrans. intro P. apply isequiv_0gpd_issurjinj. apply Build_IsSurjInj. - intros f; cbn in f. exists (trijoin_rec f). apply trijoin_rec_beta. - exact (@isinj_trijoin_rec_inv A B C P). Defined.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.