{P : Type} {a b c : P} {ab : a = b} {ac : a = c} {bc : b = c} (abc : ab @ bc = ac) : prism abc abc (equiv_p1_1q idpath) (equiv_p1_1q idpath) (equiv_p1_1q idpath). Proof. induction ab, bc, abc; simpl. reflexivity. Defined.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.