(A B C P : Type) : trijoinrecdata_0gpd A B C P $-> trijoinrecdata_0gpd B A C P. Proof. snrapply Build_Morphism_0Gpd. - cbn. intros [f1 f2 f3 f12 f13 f23 f123]. snrapply (Build_TriJoinRecData f2 f1 f3). + intros b a; exact (f12 a b)^. + exact f23. + exact f13. + intros a b c; cbn beta. apply moveR_Vp. symmetry; apply f123. - apply Build_Is0Functor. intros f g h; cbn in *. snrapply Build_TriJoinRecPath; intros; simpl. 1, 2, 3, 5, 6: apply h. + cbn zeta. prism_ind_two g h b a _X_; cbn beta. apply concat_p1_1p. + cbn beta zeta. prism_ind g h b a c; cbn beta. by triangle_ind f b a c. Defined.
Require Import Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.Core.