proposition: Lemma bifunctor_assoc_repn {B C:category} (X : [B, [C^op,SET]]) : (∏ b, Representation (X ◾ b)) -> Representation (bifunctor_assoc X).
proof: Proof. intro r. set (X' := addStructure X r). change (categoryWithStructure [C ^op, SET] Representation) with (RepresentedFunctor C) in X'. set (F := universalObjectFunctor C □ X'). exists F. unshelve refine (_,,_). { unshelve refine (_,,_). { intro b. exact (universalElement (r b)). } { abstract (intros b b' f; exact (!universalObjectFunctor_comm C (X' ▭ f))) using _K_. } } { intro F'. apply UniqueConstruction_to_weq. split. { intro x'. unfold arrow in x'. unshelve refine (_,,_). { unshelve refine (makeNattrans _ _). { intro b. exact (r b \\ pr1 x' b). } { abstract (intros b b' f; simpl; unshelve refine (univ_arrow_mor_assoc (F' ▭ f) (pr1 x' b') (r b') @ _); intermediate_path (r b' \\ (X ▭ f ⟳ pr1 x' b)); [ apply maponpaths, (pr2 x' b b' f) | unfold F; rewrite comp_func_on_mor; rewrite (universalObjectFunctor_on_map C (X' ▭ f)); change (pr2 (X' ◾ b')) with (r b'); change (pr2 (X' ◾ b)) with (r b); change (X' ▭ f) with (X ▭ f); unshelve refine (_ @ !univ_arrow_mor_assoc _ _ _); apply maponpaths; rewrite <- nattrans_arrow_mor_assoc; apply (maponpaths (λ k, X ▭ f ⟳ k)); apply pathsinv0; exact (universalMapProperty (r b) (pr1 x' b)) ]) using _R_. } } { abstract (unshelve refine (total2_paths_f _ _); [ simpl; apply funextsec; intro b; unshelve refine (universalMapProperty _ _) | apply funextsec; intro b; apply funextsec; intro b'; apply funextsec; intro f; simpl; apply setproperty ] ) using _L_. } } { abstract (intros p q e; apply nat_trans_eq; [ apply homset_property | intros b; apply (mapUniqueness _ (r b) _ (p ◽ b) (q ◽ b)); exact (maponpaths (λ k, pr1 k b) e)]) using _M_. } } Defined.
imports: UniMath.Foundations.Preamble UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.yoneda UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.MonoEpiIso UniMath.CategoryTheory.RepresentableFunctors.Bifunctor UniMath.CategoryTheory.RepresentableFunctors.Precategories UniMath.MoreFoundations.Tactics