{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.