fact: Definition prism_ind {P : Type} (a b c : P) (ab : a = b) (ac : a = c) (bc : b = c) (abc : ab @ bc = ac) (Q : forall (a' b' c' : P) (ab' : a' = b') (ac' : a' = c') (bc' : b' = c') (abc' : ab' @ bc' = ac') (k1 : a = a') (k2 : b = b') (k3 : c = c') (k12 : ab @ k2 = k1 @ ab') (k13 : ac @ k3 = k1 @ ac') (k23 : bc @ k3 = k2 @ bc') (k123 : prism abc abc' k12 k13 k23), Type) (s : Q a b c ab ac bc abc idpath idpath idpath (equiv_p1_1q idpath) (equiv_p1_1q idpath) (equiv_p1_1q idpath) (prism_id abc)) : forall a' b' c' ab' ac' bc' abc' k1 k2 k3 k12 k13 k23 k123, Q a' b' c' ab' ac' bc' abc' k1 k2 k3 k12 k13 k23 k123.
imports: Basics Types.Paths WildCat Join.Core HoTT.Tactics