TriangleIdentity Join Empty. Proof. intros A B x; cbn. lhs nrapply (functor_join_compose idmap _ idmap _). lhs_V nrapply '. unfold join_assoc; cbn. apply join_sym_nat. Defined.
Require Import Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.Core.