TriJoinRecData' {A B C P : Type} {j1' : A -> P} {j2' : B -> P} {j3' : C -> P} := { j12' : forall a b, j1' a = j2' b; j13' : forall a c, j1' a = j3' c; j23' : forall b c, j2' b = j3' c; j123' : forall a b c, j12' a b @ j23' b c = j13' a c; }.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.