Proposition collage_profunctor_is_precategory : is_precategory collage_profunctor_precategory_data. Proof. use make_is_precategory_one_assoc. - intros x₁ x₂ f. induction x₁ as [ x₁ | y₁ ] ; induction x₂ as [ x₂ | y₂ ] ; try (apply (fromempty f)) ; cbn in *. + apply id_left. + apply lmap_id. + apply id_left. - intros x₁ x₂ f. induction x₁ as [ x₁ | y₁ ] ; induction x₂ as [ x₂ | y₂ ] ; try (apply (fromempty f)) ; cbn in *. + apply id_right. + apply rmap_id. + apply id_right. - intros x₁ x₂ x₃ x₄ f g h. induction x₁ as [ x₁ | y₁ ] ; induction x₂ as [ x₂ | y₂ ] ; induction x₃ as [ x₃ | y₃ ] ; induction x₄ as [ x₄ | y₄ ] ; try (apply (fromempty f)) ; try (apply (fromempty g)) ; try (apply (fromempty h)) ; cbn in *. + apply assoc. + apply rmap_comp. + apply lmap_rmap. + refine (!_). apply lmap_comp. + apply assoc. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Profunctors.Core. Require Import UniMath.CategoryTheory.Profunctors.Examples. Require Import UniMath.CategoryTheory.Profunctors.Squares.