proposition: Proposition cofree_comonoid_REL_map_unique : isaprop (∑ f', f = # (underlying_commutative_comonoid REL_sym_mon_closed_cat) f' · map_to_cofree_comonoid_REL X).
proof: Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. apply homset_property. } use subtypePath. { intro. apply is_locally_propositional_commutative_comonoid. } enough (comonoid_mor_REL_to_monoid_mor (pr1 φ₁) = comonoid_mor_REL_to_monoid_mor (pr1 φ₂)) as H. { use funextsec ; intro y₁. use funextsec ; intro y₂. use hPropUnivalence. - intro p. exact (eqweqmaphProp (eqtohomot (eqtohomot (maponpaths pr1 H) y₂) y₁) p). - intro p. exact (eqweqmaphProp (!eqtohomot (eqtohomot (maponpaths pr1 H) y₂) y₁) p). } use free_abmonoid_mor_eq. intro x ; cbn. use funextsec ; intro y. use hPropUnivalence. - intros a. unfold comonoid_mor_REL_to_map in a. assert (p := eqweqmaphProp (eqtohomot (eqtohomot (!(pr2 φ₁) @ pr2 φ₂) y) x) (hinhpr (_ ,, a ,, idpath _))). revert p. use factor_through_squash_hProp. cbn ; intros [ b [ p₁ p₂ ] ]. rewrite <- p₂ in p₁. exact p₁. - intros a. unfold comonoid_mor_REL_to_map in a. assert (p := eqweqmaphProp (!eqtohomot (eqtohomot (!(pr2 φ₁) @ pr2 φ₂) y) x) (hinhpr (_ ,, a ,, idpath _))). revert p. use factor_through_squash_hProp. cbn ; intros [ b [ p₁ p₂ ] ]. rewrite <- p₂ in p₁. exact p₁. Qed.
imports: UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.Algebra.Free_Monoids_and_Groups UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Categories.Rel UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Monads.Comonads UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Functors UniMath.CategoryTheory.Monoidal.Adjunctions UniMath.CategoryTheory.Monoidal.FunctorCategories UniMath.CategoryTheory.Monoidal.Displayed.TotalMonoidal UniMath.CategoryTheory.Monoidal.Displayed.Symmetric UniMath.CategoryTheory.Monoidal.Structure.Cartesian UniMath.CategoryTheory.Monoidal.Structure.Symmetric UniMath.CategoryTheory.Monoidal.Structure.Closed UniMath.CategoryTheory.Monoidal.Comonoids.Category UniMath.CategoryTheory.Monoidal.Comonoids.Monoidal UniMath.CategoryTheory.Monoidal.Comonoids.Symmetric UniMath.CategoryTheory.Monoidal.Comonoids.CommComonoidsCartesian UniMath.CategoryTheory.Monoidal.Examples.Relations UniMath.Semantics.LinearLogic.LafontCategory