(A B C : Type) {P Q : Type} (g : P -> Q) (f : TriJoinRecData A B C P) : trijoin_rec (trijoinrecdata_fun g f) $== g o trijoin_rec f. Proof. exact (isnat (trijoin_rec_natequiv A B C) g f). Defined.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.