fact: Definition trijoin_ind (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.
imports: Basics Types.Paths WildCat Join.Core HoTT.Tactics