(A B C : Type) (P : TriJoin A B C -> Type) (join1' : forall a, P (join1 a)) (join2' : forall b, P (join2 b)) (join3' : forall c, P (join3 c)) (join12' : forall a b, join12 a b # join1' a = join2' b) (join13' : forall a c, join13 a c # join1' a = join3' c) (join23' : forall b c, join23 b c # join2' b = join3' c) (join123' : forall a b c, transport_pp _ (join12 a b) (join23 b c) (join1' a) @ ap (transport _ (join23 b c)) (join12' a b) @ join23' b c = transport2 _ (join123 a b c) _ @ join13' a c) : forall x, P x. Proof. snrapply Join_ind. - exact join1'. - snrapply Join_ind. + exact join2'. + exact join3'. + intros b c. lhs rapply (transport_compose P). apply join23'. - intro a. snrapply Join_ind. + simpl. exact (join12' a). + simpl. exact (join13' a). + intros b c; cbn beta zeta. lhs nrapply (transport_paths_FlFr_D (jglue b c)). lhs nrapply (1 @@ _). 1: nrapply Join_ind_beta_jglue. apply trijoin_ind_helper, join123'. Defined.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.