Library UniMath.Semantics.LinearLogic.RelationalModel

Require Import UniMath.MoreFoundations.All.
Require Import UniMath.Algebra.Monoids.
Require Import UniMath.Algebra.Free_Monoids_and_Groups.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Categories.Rel.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.Adjunctions.Coreflections.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.Monads.Comonads.
Require Import UniMath.CategoryTheory.Monoidal.Categories.
Require Import UniMath.CategoryTheory.Monoidal.Functors.
Require Import UniMath.CategoryTheory.Monoidal.Adjunctions.
Require Import UniMath.CategoryTheory.Monoidal.FunctorCategories.
Require Import UniMath.CategoryTheory.Monoidal.Displayed.TotalMonoidal.
Require Import UniMath.CategoryTheory.Monoidal.Displayed.Symmetric.
Require Import UniMath.CategoryTheory.Monoidal.Structure.Cartesian.
Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric.
Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed.
Require Import UniMath.CategoryTheory.Monoidal.Comonoids.Category.
Require Import UniMath.CategoryTheory.Monoidal.Comonoids.Monoidal.
Require Import UniMath.CategoryTheory.Monoidal.Comonoids.Symmetric.
Require Import UniMath.CategoryTheory.Monoidal.Comonoids.CommComonoidsCartesian.
Require Import UniMath.CategoryTheory.Monoidal.Examples.Relations.
Require Import UniMath.Semantics.LinearLogic.LafontCategory.

Import MonoidalNotations.

Local Open Scope cat.
Local Open Scope moncat.

Opaque free_abmonoid free_abmonoid_extend free_abmonoid_unit.

1. The cofree comonoid on a set

Section CofreeComonoid.
  Context (X : hSet).

  Let Mmonoid : abmonoid := free_abmonoid X.
  Let M : hSet := Mmonoid.
  Let z : M := unel Mmonoid.
  Let m : M → M → M := λ x y, op x y.

  Definition cofree_comonoid_REL_comult
    : REL_sym_mon_closed_cat ⟦ M , (M × M)%set ⟧
    := λ x y, (m (pr1 y) (pr2 y) = x)%logic.

  Definition cofree_comonoid_REL_counit
    : REL_sym_mon_closed_cat ⟦ M , unitset ⟧
    := λ x y, (x = z)%logic.

  Proposition cofree_comonoid_REL_counit_left
    : cofree_comonoid_REL_comult
      · (cofree_comonoid_REL_counit #⊗ identity _)
      · mon_lunitor _
      =
      identity _.
  Show proof.
    use funextsec ; intro x.
    use funextsec ; intro y.
    use hPropUnivalence.
    - use factor_through_squash_hProp.
      intros H.
      induction H as [ [ [] a ] [ H p ] ] ; cbn in a, p.
      revert H.
      use factor_through_squash_hProp.
      intros H.
      induction H as [ [ b c ] [ q H ] ] ; cbn in q.
      revert H.
      use factor_through_squash_hProp.
      intros [ [ [] d ] [ [ r₁ r₂ ] [ r₃ r₄ ] ] ].
      cbn in r₁, r₂, r₃, r₄ ; cbn.
      refine (!q @ _ @ p).
      rewrite <- r₄.
      rewrite <- r₁.
      rewrite r₂.
      apply (lunax Mmonoid).
    - intros p ; cbn in p.
      induction p.
      refine (hinhpr _).
      refine ((tt ,, x) ,, _).
      refine (_ ,, idpath _).
      refine (hinhpr _).
      refine ((z ,, x) ,, _ ,, _).
      + apply (lunax Mmonoid).
      + refine (hinhpr _).
        refine ((tt ,, x) ,, _) ; cbn.
        repeat split ; apply idpath.

  Proposition cofree_comonoid_REL_coassoc
    : cofree_comonoid_REL_comult
      · cofree_comonoid_REL_comult #⊗ identity _
      · mon_lassociator _ _ _
      =
      cofree_comonoid_REL_comult
      · identity _ #⊗ cofree_comonoid_REL_comult.
  Show proof.
    use funextsec ; intro x.
    use funextsec ; intro y.
    induction y as [ y₁ [ y₂ y₃ ]].
    use hPropUnivalence.
    - use factor_through_squash_hProp.
      intros H.
      induction H as [ [ [ a₁ a₂ ] a₃ ] [ H [ p₁ [ p₂ p₃ ] ] ] ] ; cbn in p₁, p₂, p₃.
      revert H.
      use factor_through_squash_hProp.
      intros H.
      induction H as [ [ b₁ b₂ ] [ q H ] ] ; cbn in q.
      revert H.
      use factor_through_squash_hProp.
      intros H.
      cbn in H.
      induction H as [ [ [ c₁ c₂ ] c₃ ] [ [ r₁ r₂ ] [ r₃ r₄ ] ] ] ; cbn in r₁, r₂, r₃, r₄.
      induction p₁, p₂, p₃, r₁, r₄.
      pose (r₅ := maponpaths dirprod_pr1 r₃) ; cbn in r₅.
      pose (r₆ := maponpaths dirprod_pr2 r₃) ; cbn in r₆.
      induction r₅, r₆.
      rewrite <- r₂ in q.
      assert (m (m c₁ c₂) b₂ = m c₁ (m c₂ b₂)) as s.
      {
        exact (assocax Mmonoid c₁ c₂ b₂).
      }
      rewrite s in q.
      refine (hinhpr _).
      refine ((c₁ ,, m c₂ b₂) ,, _).
      split.
      + exact q.
      + refine (hinhpr _).
        exact ((_ ,, _) ,, (idpath _ ,, idpath _) ,, (idpath _ ,, idpath _)).
    - use factor_through_squash_hProp.
      intros H.
      induction H as [ [ a₁ a₂ ] [ p H ]] ; cbn in p.
      revert H.
      use factor_through_squash_hProp.
      intros H.
      induction H as [ [ b₁ b₂ ] [ [ q₁ q₂ ] [ q₃ q₄ ]]] ; cbn in q₁, q₂, q₃, q₄.
      induction q₁, q₂, q₃.
      rewrite <- q₄ in p ; clear q₄.
      assert (m a₁ (m y₂ y₃) = m (m a₁ y₂) y₃) as s.
      {
        exact (!(assocax Mmonoid a₁ y₂ y₃)).
      }
      rewrite s in p.
      refine (hinhpr (((a₁ ,, y₂) ,, y₃) ,, _)).
      refine (_ ,, idpath _ ,, idpath _ ,, idpath _).
      refine (hinhpr ((m a₁ y₂ ,, y₃) ,, p ,, _)).
      refine (hinhpr _) ; cbn.
      simple refine (((a₁ ,, y₂) ,, y₃) ,, _) ; repeat split.

  Proposition cofree_comonoid_REL_comm
    : cofree_comonoid_REL_comult
      · sym_mon_braiding REL_sym_mon_closed_cat _ _
      =
      cofree_comonoid_REL_comult.
  Show proof.
    use funextsec ; intro x.
    use funextsec ; intro y.
    induction y as [ y₁ y₂ ].
    use hPropUnivalence.
    - use factor_through_squash_hProp ; cbn.
      intros [ [ a₁ a₂ ] [ p₁ [ p₂ p₃ ] ] ] ; cbn in p₁, p₂, p₃.
      induction p₂, p₃.
      refine (_ @ p₁).
      apply (commax Mmonoid).
    - intro p ; cbn in p.
      refine (hinhpr ((y₂ ,, y₁) ,, _ ,, _ ,, _)) ; cbn.
      + refine (_ @ p).
        apply (commax Mmonoid).
      + apply idpath.
      + apply idpath.

  Definition cofree_comonoid_REL
    : commutative_comonoid REL_sym_mon_closed_cat.
  Show proof.
    use make_commutative_comonoid.
    - exact M.
    - exact cofree_comonoid_REL_comult.
    - exact cofree_comonoid_REL_counit.
    - exact cofree_comonoid_REL_counit_left.
    - exact cofree_comonoid_REL_coassoc.
    - exact cofree_comonoid_REL_comm.
End CofreeComonoid.

Definition map_to_cofree_comonoid_REL
           (X : REL)
  : REL ⟦ cofree_comonoid_REL X , X ⟧
  := λ y x, (free_abmonoid_unit x = y)%logic.

2. Every comonoid in `REL` gives rise to a monoid in `SET`

Section ComonoidToMonoid.
  Context (C : commutative_comonoid REL_sym_mon_closed_cat).

  Let U : hSet := underlying_commutative_comonoid _ C.

  Definition REL_comonoid_to_mult
             (X Y : U → hProp)
             (y : U)
    : hProp
    := ∃ (x₁ x₂ : U), X x₁ ∧ Y x₂ ∧ comonoid_comult _ C y (x₁ ,, x₂).

  Definition REL_comonoid_to_unit
    : U → hProp
    := λ x, comonoid_counit _ C x tt.

  Definition REL_comonoid_to_setwithbinop
    : setwithbinop.
  Show proof.
    use make_setwithbinop.
    - exact (funset U hPropset).
    - exact REL_comonoid_to_mult.

  Proposition REL_comonoid_to_assoc
    : isassoc (pr2 REL_comonoid_to_setwithbinop).
  Show proof.
    intros X Y Z.
    use funextsec ; intro y.
    use hPropUnivalence.
    - use factor_through_squash_hProp.
      intros ( a₁ & a₂ & H & p₁ & p₂ ).
      revert H.
      use factor_through_squash_hProp.
      intros ( b₁ & b₂ & q₁ & q₂ & q₃ ).
      pose (eqweqmaphProp
              (eqtohomot
                 (eqtohomot
                    (comonoid_to_law_assoc _ C)
                    y)
                 (b₁ ,, (b₂ ,, a₂))))
        as H.
      cbn in H.
      assert (H' := H (hinhpr
                         ((((b₁ ,, b₂) ,, a₂)
                           ,,
                           hinhpr
                             ((a₁ ,, a₂)
                              ,,
                              p₂
                              ,,
                              idpath _
                              ,,
                              q₃)
                           ,,
                           idpath _
                           ,,
                           idpath _
                           ,,
                           idpath _)))).
      revert H'.
      use factor_through_squash_hProp.
      intros [ [ c₁ c₂ ] [ r₁ [ r₂ r₃ ] ] ] ; cbn in r₁, r₂, r₃.
      induction r₂.
      apply hinhpr.
      simple refine (c₁ ,, c₂ ,, q₁ ,, _ ,, _).
      + use hinhpr ; cbn.
        exact (b₂ ,, a₂ ,, q₂ ,, p₁ ,, r₃).
      + exact r₁.
    - use factor_through_squash_hProp.
      intros ( a₁ & a₂ & p₁ & H & p₂ ).
      revert H.
      use factor_through_squash_hProp.
      intros ( b₁ & b₂ & q₁ & q₂ & q₃ ).
      pose (eqweqmaphProp
              (!eqtohomot
                 (eqtohomot
                    (comonoid_to_law_assoc _ C)
                    y)
                 (a₁ ,, (b₁ ,, b₂))))
        as H.
      assert (H' := H (hinhpr ((a₁ ,, a₂) ,, p₂ ,, idpath _ ,, q₃))).
      revert H'.
      use factor_through_squash_hProp.
      intros [ [ [ c₁ c₂ ] c₃ ] [ K [ r₁ [ r₂ r₃ ] ] ] ] ; cbn in r₁, r₂, r₃.
      revert K.
      use factor_through_squash_hProp.
      intros [ [ d₁ d₂ ] [ s₁ [ s₂ s₃ ] ] ] ; cbn in s₁, s₂, s₃.
      induction r₁, r₂, r₃, s₂.
      apply hinhpr.
      simple refine (d₁ ,, d₂ ,, _ ,, q₂ ,, s₁).
      apply hinhpr ; cbn.
      simple refine (c₁ ,, c₂ ,, p₁ ,, q₁ ,, _) ; cbn.
      exact s₃.

  Proposition REL_comonoid_to_lunit
    : islunit (pr2 REL_comonoid_to_setwithbinop) REL_comonoid_to_unit.
  Show proof.
  intro X.
  use funextsec ; intro y ; cbn in y.
  use hPropUnivalence.
  - use factor_through_squash_hProp.
    intros ( x₁ & x₂ & p₁ & p₂ & p₃ ).
    unfold REL_comonoid_to_unit in p₁.
    assert (y = x₂) as q.
    {
      apply (eqweqmaphProp (eqtohomot (eqtohomot (comonoid_to_law_unit_left _ C) y) x₂)).
      cbn.
      use hinhpr.
      refine ((tt ,, x₂) ,, _ ,, idpath _).
      use hinhpr ; cbn.
      refine ((x₁ ,, x₂) ,, _) ; cbn.
      refine (p₃ ,, idpath _ ,, p₁).
    }
    rewrite q.
    exact p₂.
  - intro Hy.
    assert (q := eqweqmaphProp
                   (!eqtohomot
                      (eqtohomot
                         (comonoid_to_law_unit_left _ C)
                         y)
                      y)
                   (idpath _)).
    revert q.
    use factor_through_squash_hProp.
    intros [ [ [] a ] [ H p ] ] ; cbn in p.
    induction p.
    revert H.
    use factor_through_squash_hProp.
    intros [ [ b₁ b₂ ] [ q₁ [ q₂ q₃ ] ] ] ; cbn in q₁, q₂, q₃.
    induction q₂.
    use hinhpr.
    refine (b₁ ,, b₂ ,, _ ,, _ ,, _) ; cbn.
    + exact q₃.
    + exact Hy.
    + exact q₁.

  Proposition REL_comonoid_to_comm
    : iscomm (pr2 REL_comonoid_to_setwithbinop).
  Show proof.
    intros X Y.
    use funextsec ; intro y ; cbn in y.
    use hPropUnivalence.
    - use factor_through_squash_hProp.
      intros ( x₁ & x₂ & p₁ & p₂ & H ).
      use hinhpr.
      refine (x₂ ,, x₁ ,, p₂ ,, p₁ ,, _).
      assert (q := eqweqmaphProp
                     (!eqtohomot
                        (eqtohomot
                           (commutative_comonoid_is_commutative _ C)
                           y)
                        (x₁ ,, x₂))
                     H).
      revert q.
      use factor_through_squash_hProp.
      intros [ [ a₁ a₂ ] [ q₁ [ q₂ q₃ ] ] ] ; cbn in q₁, q₂, q₃.
      induction q₂, q₃.
      exact q₁.
    - use factor_through_squash_hProp.
      intros ( x₁ & x₂ & p₁ & p₂ & H ).
      use hinhpr.
      refine (x₂ ,, x₁ ,, p₂ ,, p₁ ,, _).
      assert (q := eqweqmaphProp
                     (!eqtohomot
                        (eqtohomot
                           (commutative_comonoid_is_commutative _ C)
                           y)
                        (x₁ ,, x₂))
                     H).
      revert q.
      use factor_through_squash_hProp.
      intros [ [ a₁ a₂ ] [ q₁ [ q₂ q₃ ] ] ] ; cbn in q₁, q₂, q₃.
      induction q₂, q₃.
      exact q₁.

  Proposition REL_comonoid_to_runit
    : isrunit (pr2 REL_comonoid_to_setwithbinop) REL_comonoid_to_unit.
  Show proof.
    intro X.
    refine (REL_comonoid_to_comm _ _ @ _).
    apply REL_comonoid_to_lunit.

  Definition REL_comonoid_to_is_unital
    : isunital (pr2 REL_comonoid_to_setwithbinop).
  Show proof.
    use make_isunital.
    - exact REL_comonoid_to_unit.
    - split.
      + exact REL_comonoid_to_lunit.
      + exact REL_comonoid_to_runit.

  Definition REL_comonoid_to_is_monoidop
    : ismonoidop (pr2 REL_comonoid_to_setwithbinop).
  Show proof.
    use make_ismonoidop.
    - exact REL_comonoid_to_assoc.
    - exact REL_comonoid_to_is_unital.

  Definition REL_comonoid_to_is_abmonoidop
    : isabmonoidop (pr2 REL_comonoid_to_setwithbinop).
  Show proof.
    use make_isabmonoidop.
    - exact REL_comonoid_to_is_monoidop.
    - exact REL_comonoid_to_comm.

  Definition REL_comonoid_to_monoid
    : abmonoid.
  Show proof.
    use make_abmonoid.
    - exact REL_comonoid_to_setwithbinop.
    - exact REL_comonoid_to_is_abmonoidop.
End ComonoidToMonoid.

3. The universal property of the cofree comonoid in `REL`

Section CofreeComonoidUMP.
  Context (X : REL)
          (C : commutative_comonoid REL_sym_mon_closed_cat)
          (f : underlying_commutative_comonoid _ C --> X).

  Definition cofree_comonoid_REL_underlying
    : underlying_commutative_comonoid _ C
      -->
      underlying_commutative_comonoid _ (cofree_comonoid_REL X)
    := λ c x, @free_abmonoid_extend X (REL_comonoid_to_monoid C) (λ c x, f x c) x c.

  Proposition cofree_comonoid_REL_map_comult
    : comonoid_comult REL_sym_mon_closed_cat C
      · cofree_comonoid_REL_underlying #⊗ cofree_comonoid_REL_underlying
      =
      cofree_comonoid_REL_underlying
      · comonoid_comult REL_sym_mon_closed_cat (cofree_comonoid_REL X).
  Show proof.
    use funextsec ; intro y.
    use funextsec ; intros [ x₁ x₂ ] ; cbn in x₁, x₂.
    use hPropUnivalence.
    - use factor_through_squash_hProp.
      intros [ [ a₁ a₂ ] [ p H ] ].
      revert H.
      use factor_through_squash_hProp.
      intros [ [ b₁ b₂ ] [ [ q₁ q₂ ] [ q₃ q₄ ] ] ] ; cbn in q₁, q₂, q₃, q₄.
      induction q₁, q₃.
      pose (eqweqmaphProp
              (!(eqtohomot
                   (monoidfunmul
                      (@free_abmonoid_extend X (REL_comonoid_to_monoid C) (λ c x, f x c))
                      b₁ x₂)
                   y))
              (hinhpr (a₁ ,, a₂ ,, q₂ ,, q₄ ,, p)))
        as q.
      apply hinhpr.
      exact (_ ,, q ,, idpath _).
    - use factor_through_squash_hProp.
      intros [ a [ p₁ p₂ ]] ; cbn in p₁, p₂.
      induction p₂.
      assert (H := eqweqmaphProp
                     (eqtohomot
                        (monoidfunmul
                           (@free_abmonoid_extend X (REL_comonoid_to_monoid C) (λ c x, f x c))
                           x₁ x₂)
                        y)
                     p₁).
      revert H.
      use factor_through_squash_hProp.
      intros [ a₁ [ a₂ [ q₁ [ q₂ q₃ ] ] ] ] ; cbn in a₁, a₂, q₁, q₂, q₃.
      refine (hinhpr ((a₁ ,, a₂) ,, q₃ ,, _)).
      apply hinhpr ; cbn.
      simple refine ((x₁ ,, a₂) ,, (_ ,, _) ,, (_ ,, _)) ; cbn.
      + apply idpath.
      + exact q₁.
      + apply idpath.
      + exact q₂.

  Proposition cofree_comonoid_REL_map_counit
    : comonoid_counit REL_sym_mon_closed_cat C
      =
      cofree_comonoid_REL_underlying
      · comonoid_counit REL_sym_mon_closed_cat (cofree_comonoid_REL X).
  Show proof.
    use funextsec ; intros x₁.
    use funextsec ; intros x₂.
    induction x₂.
    use hPropUnivalence.
    - intros y.
      refine (hinhpr (_ ,, _ ,, idpath _)).
      exact (eqweqmaphProp
               (!eqtohomot
                  (monoidfununel
                     (@free_abmonoid_extend X (REL_comonoid_to_monoid C) (λ c x, f x c)))
                  x₁)
               y).
    - use factor_through_squash_hProp.
      intros [ a [ p₁ p₂ ]] ; cbn in p₁, p₂, a.
      apply (eqweqmaphProp
               (eqtohomot
                  (monoidfununel
                     (@free_abmonoid_extend X (REL_comonoid_to_monoid C) (λ c x, f x c)))
                  x₁)).
      rewrite <- p₂.
      exact p₁.

  Definition cofree_comonoid_REL_map
    : C --> cofree_comonoid_REL X.
  Show proof.
    use make_commutative_comonoid_mor.
    - exact (cofree_comonoid_REL_underlying).
    - exact cofree_comonoid_REL_map_comult.
    - exact cofree_comonoid_REL_map_counit.

  Proposition cofree_comonoid_REL_map_comm
    : f = cofree_comonoid_REL_underlying · map_to_cofree_comonoid_REL X.
  Show proof.
    use funextsec ; intro x.
    use funextsec ; intro y.
    use hPropUnivalence.
    - intro p.
      use hinhpr.
      exact (free_abmonoid_unit y ,, p ,, idpath _).
    - use factor_through_squash_hProp.
      intros ( a & H & p ).
      simpl in a, H, p.
      rewrite <- p in H.
      exact H.

  Section ToMonoidMor.
    Context (φ : C --> cofree_comonoid_REL X).

    Definition comonoid_mor_REL_to_map
      : free_abmonoid X → REL_comonoid_to_monoid C
      := λ x y, pr1 φ y x.

    Proposition ismonoidfun_comonoid_mor_REL_to_map
      : ismonoidfun comonoid_mor_REL_to_map.
    Show proof.
      split.
      - intros y₁ y₂.
        use funextsec ; intro x.
        use hPropUnivalence.
        + intro z.
          assert (H := eqweqmaphProp
                         (!eqtohomot
                            (eqtohomot (underlying_comonoid_mor_comult φ) x)
                            (y₁ ,, y₂))
                         (hinhpr (_ ,, z ,, idpath _))).
          revert H.
          use factor_through_squash_hProp.
          intros [ [ a₁ a₂ ] [ p H ] ].
          revert H.
          use factor_through_squash_hProp.
          intros [ [ b₁ b₂ ] [ [ q₁ q₂ ] [ q₃ q₄ ] ] ] ; cbn in q₁, q₂, q₃, q₄.
          induction q₁, q₃.
          apply hinhpr.
          exact (a₁ ,, a₂ ,, q₂ ,, q₄ ,, p).
        + use factor_through_squash_hProp.
          intros ( a₁ & a₂ & p₁ & p₂ & p₃ ).
          assert (H := eqweqmaphProp
                         (eqtohomot
                            (eqtohomot (underlying_comonoid_mor_comult φ) x)
                            (y₁ ,, y₂))
                         (hinhpr
                            ((a₁ ,, a₂)
                             ,,
                             p₃
                             ,,
                             hinhpr ((_ ,, _)
                                     ,,
                                     (idpath _ ,, p₁)
                                     ,,
                                     (idpath _ ,, p₂))))).
          revert H.
          use factor_through_squash_hProp.
          cbn.
          intros [ b [ q₁ q₂ ]].
          rewrite <- q₂ in q₁.
          exact q₁.
      - use funextsec ; intro x.
        use hPropUnivalence.
        + intro z.
          exact (eqweqmaphProp
                   (!eqtohomot (eqtohomot (underlying_comonoid_mor_counit φ) x) tt)
                   (hinhpr (_ ,, z ,, idpath _))).
        + intro z ; cbn in z.
          assert (H := eqweqmaphProp
                         (eqtohomot (eqtohomot (underlying_comonoid_mor_counit φ) x) tt)
                         z).
          revert H.
          use factor_through_squash_hProp.
          intros [ a [ p q ]] ; cbn in q.
          rewrite q in p.
          exact p.

    Definition comonoid_mor_REL_to_monoid_mor
      : monoidfun (free_abmonoid X) (REL_comonoid_to_monoid C)
      := make_monoidfun ismonoidfun_comonoid_mor_REL_to_map.
  End ToMonoidMor.

  Proposition cofree_comonoid_REL_map_unique
    (g : C --> cofree_comonoid_REL X)
    (Hg : f = # (underlying_commutative_comonoid REL_sym_mon_closed_cat) g · map_to_cofree_comonoid_REL X)
    : g = cofree_comonoid_REL_map.
  Show proof.
    use subtypePath.
    {
      intro.
      apply is_locally_propositional_commutative_comonoid.
    }
    enough (comonoid_mor_REL_to_monoid_mor g
            =
            comonoid_mor_REL_to_monoid_mor cofree_comonoid_REL_map)
      as H.
    {
      use funextsec ; intro y₁.
      use funextsec ; intro y₂.
      use hPropUnivalence.
      - intro p.
        exact (eqweqmaphProp (eqtohomot (monoidfun_eq H y₂) y₁) p).
      - intro p.
        exact (eqweqmaphProp (!eqtohomot (monoidfun_eq H y₂) y₁) p).
    }
    refine (invmap monoidfun_eq (abelian_monoid_morphism_eq (free_abmonoid_mor_eq
      (f := monoidfun_to_abelian_monoid_morphism (comonoid_mor_REL_to_monoid_mor _))
      (g := monoidfun_to_abelian_monoid_morphism (comonoid_mor_REL_to_monoid_mor _)) _))).
    intro x ; cbn.
    use funextsec ; intro y.
    use hPropUnivalence.
    - intros a.
      unfold comonoid_mor_REL_to_map in a.
      assert (p := eqweqmaphProp
                     (eqtohomot
                        (eqtohomot (!Hg @ cofree_comonoid_REL_map_comm) 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 (!Hg @ cofree_comonoid_REL_map_comm) y)
                        x)
                     (hinhpr (_ ,, a ,, idpath _))).
      revert p.
      use factor_through_squash_hProp.
      cbn ; intros [ b [ p₁ p₂ ] ].
      rewrite <- p₂ in p₁.
      exact p₁.

End CofreeComonoidUMP.

Definition cofree_comonoid_REL_coreflection_data
  (X : REL_sym_mon_closed_cat)
  : coreflection_data X (underlying_commutative_comonoid REL_sym_mon_closed_cat).
Show proof.
  use make_coreflection_data.
  - exact (cofree_comonoid_REL X).
  - exact (map_to_cofree_comonoid_REL X).

Corollary cofree_comonoid_REL_is_coreflection
  (X : REL_sym_mon_closed_cat)
  : is_coreflection (cofree_comonoid_REL_coreflection_data X).
Show proof.
  intro f.
  use make_coreflection_arrow.
  - apply cofree_comonoid_REL_map.
    exact f.
  - apply cofree_comonoid_REL_map_comm.
  - apply cofree_comonoid_REL_map_unique.

4. The relational model of linear logic

Definition relational_model
  : lafont_category.
Show proof.
  use make_lafont_category.
  - exact REL_sym_mon_closed_cat.
  - use coreflections_to_is_left_adjoint.
    intro X.
    use make_coreflection.
    + exact (cofree_comonoid_REL_coreflection_data X).
    + exact (cofree_comonoid_REL_is_coreflection X).