proposition: Lemma comm_comm_eq_id (A B C:category) : bifunctor_comm A B C ∙ bifunctor_comm B A C = functor_identity _.
proof: Proof. intros. unshelve refine (Functor_eq _ _). { intro F. change (functor_identity [A, [B, C]] ◾ F) with F. unshelve refine (Functor_eq _ _). { intro a. unshelve refine (Functor_eq _ _); reflexivity. } { intros a a' f; simpl. Abort. End Working. Definition θ_1 {B C:category} (F : [B, C]) (X : [B, [C^op, HSET]]) : hSet := (∏ b, F ◾ b ⇒ X ◾ b) % set. Definition θ_2 {B C:category} (F : [B, C]) (X : [B, [C^op, HSET]]) (x : θ_1 F X) : hSet := hProp_to_hSet (∀ (b' b:B) (f:b'-->b), (x b ⟲ F ▭ f = X ▭ f ⟳ x b' )) % logic. Definition θ {B C:category} (F : [B, C]) (X : [B, [C^op, HSET]]) : hSet := ( ∑ x : θ_1 F X, θ_2 F X x ) % set. Local Notation "F ⟹ X" := (θ F X) (at level 39) : cat. Definition θ_subset {B C:category} {F : [B, C]} {X : [B, [C^op, HSET]]} (t u : F ⟹ X) : pr1 t = pr1 u -> t = u. Proof. apply subtypePath. intros x. apply impred; intro b;apply impred; intro b'; apply impred; intro f. apply setproperty. Defined.
imports: UniMath.Foundations.Preamble UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.RepresentableFunctors.Precategories UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.yoneda UniMath.CategoryTheory.Categories.HSET.Core