Definition bifunctor_assoc {B C:category} : [B, [C^op,HSET]] ⟶ [[B,C]^op,HSET]. Proof. unshelve refine (makeFunctor _ _ _ _). { intros X. unshelve refine (makeFunctor_op _ _ _ _). { intro F. exact (F ⟹ X). } { intros F' F p xe. exact (xe ⟲⟲ p). } { abstract ( intros F; apply funextsec; intro xe; apply θ_subset; simpl; apply funextsec; intro b; apply arrow_mor_id) using _K_. } { abstract ( intros F F' F'' p q; simpl; apply funextsec; intro xe; apply θ_subset; simpl; apply funextsec; intro b; unfold θ_map_1; exact (arrow_mor_mor_assoc _ _ _)) using _L_. } } { intros X Y p. simpl. unshelve refine (_,,_). { intros F. simpl. intro x. exact (φ_map x p). } { abstract ( intros F G q; simpl in F, G; simpl; apply funextsec; intro w; unshelve refine (total2_paths2_f _ _); [ apply funextsec; intro b; unfold φ_map, φ_map_1, θ_map_1; simpl; unfold θ_map_1; simpl; apply nattrans_arrow_mor_assoc | apply funextsec; intro b; apply funextsec; intro b'; apply funextsec; intro b''; apply setproperty ]) using _L_. } } { abstract( simpl; intro F; apply nat_trans_eq; [ exact (homset_property HSET) | intro G; simpl; unfold φ_map; simpl; unfold φ_map_1; simpl; apply funextsec; intro w; simpl; unshelve refine (total2_paths_f _ _); [ simpl; apply funextsec; intro b; reflexivity | apply funextsec; intro b; apply funextsec; intro b'; apply funextsec; intro f; simpl; apply setproperty] ]) using _L_. } { abstract (intros F F' F'' p q; simpl; apply nat_trans_eq; [ exact (homset_property HSET) | intro G; simpl; apply funextsec; intro w; unshelve refine (total2_paths2_f _ _); [ unfold φ_map, φ_map_1; simpl; apply funextsec; intro b; apply pathsinv0, nattrans_nattrans_arrow_assoc | apply funextsec; intro b; apply funextsec; intro b'; apply funextsec; intro f; apply setproperty ]]) using _L_. } Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.RepresentableFunctors.Precategories. Require Import UniMath.MoreFoundations.Tactics.