fact: Definition trijoin_rec_beta_join13 {A B C P : Type} (f : TriJoinRecData A B C P) (a : A) (c : C) : ap (trijoin_rec f) (join13 a c) = j13 f a c := Join_rec_beta_jglue _ _ _ _ _.
imports: Basics Types.Paths WildCat Join.Core HoTT.Tactics