{A B C A' B' C'} (f : A -> A') (g : B -> B') (h : C -> C') : functor_join f (functor_join g h) == functor_trijoin f g h := functor_join_join_rec f (functor_join_recdata g h).
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.