{A B C P : Type} {f g : TriJoinRecData A B C P} := { h1 : forall a, j1 f a = j1 g a; h2 : forall b, j2 f b = j2 g b; h3 : forall c, j3 f c = j3 g c; h12 : forall a b, j12 f a b @ h2 b = h1 a @ j12 g a b; h13 : forall a c, j13 f a c @ h3 c = h1 a @ j13 g a c; h23 : forall b c, j23 f b c @ h3 c = h2 b @ j23 g b c; h123 : forall a b c, prism (j123 f a b c) (j123 g a b c) (h12 a b) (h13 a c) (h23 b c); }.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.