{A B C} : functor_trijoin idmap idmap idmap == (idmap : TriJoin A B C -> TriJoin A B C). Proof. apply moveR_trijoin_rec. change (trijoinrecdata_trijoin A B C $== trijoinrecdata_fun idmap (trijoinrecdata_trijoin A B C)). symmetry. exact (fmap_id (trijoinrecdata_0gpd A B C) _ (trijoinrecdata_trijoin A B C)). Defined.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.