{A B C P} (f : TriJoinRecData A C B P) : trijoin_rec f o trijoin_id_sym A B C == trijoin_rec (trijoinrecdata_id_sym f). Proof. etransitivity. { refine (cat_postwhisker (A:=Type) (trijoin_rec f) _). apply functor_join_join_rec. } unfold join_sym_recdata, jl, jr, jg. refine ((trijoin_rec_nat A B C (trijoin_rec f) _)^$ $@ _). refine (fmap trijoin_rec _). bundle_trijoinrecpath; intros; cbn. - apply trijoin_rec_beta_join13. - apply trijoin_rec_beta_join12. - lhs refine (ap _ (ap_V _ _)). lhs refine (ap_V (trijoin_rec f) _). apply (ap inverse). apply trijoin_rec_beta_join23. - unfold prism'. rewrite ap_trijoin_V. rewrite trijoin_rec_beta_join123. set (f' := f). destruct f as [f1 f2 f3 f12 f13 f23 f123]; cbn. generalize (f123 a c b). generalize (trijoin_rec_beta_join23 f' c b); cbn. generalize (f23 c b). generalize (trijoin_rec_beta_join13 f' a b); cbn. generalize (f13 a b). generalize (trijoin_rec_beta_join12 f' a c); cbn. generalize (f12 a c); cbn. intros p12 beta12 p13 beta13 p23 beta23 p123. induction beta12, beta13, beta23; cbn. rewrite 3 concat_p1, concat_1p. reflexivity. Defined.
Require Import Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.Core.