fact: Definition trijoin_rec_beta {A B C P : Type} (f : TriJoinRecData A B C P) : TriJoinRecPath (trijoin_rec_inv (trijoin_rec f)) f := bundle_trijoinrecpath (trijoin_rec_beta' f).
imports: Basics Types.Paths WildCat Join.Core HoTT.Tactics