Library UniMath.CategoryTheory.EnrichedCats.Examples.DialgebraEnriched

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.categories.Dialgebras.
Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment.
Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor.
Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation.
Require Import UniMath.CategoryTheory.Monoidal.Categories.
Require Import UniMath.CategoryTheory.limits.equalizers.

Import MonoidalNotations.

Local Open Scope cat.
Local Open Scope moncat.

Section EnrichedDialgebras.
  Context (V : monoidal_cat)
          (EV : Equalizers V)
          {C₁ C₂ : category}
          {F G : C₁ C₂}
          {E₁ : enrichment C₁ V}
          {E₂ : enrichment C₂ V}
          (FE : functor_enrichment F E₁ E₂)
          (GE : functor_enrichment G E₁ E₂).

1. The enrichment of dialgebras
  Definition dialgebra_enrichment_mor_left
             {x y : C₁}
             (f : F x --> G x)
             (g : F y --> G y)
    : E₁ x , y --> E₂ F x , G y
    := GE x y · precomp_arr _ _ f.

  Definition dialgebra_enrichment_mor_right
             {x y : C₁}
             (f : F x --> G x)
             (g : F y --> G y)
    : E₁ x , y --> E₂ F x , G y
    := FE x y · postcomp_arr _ _ g.

  Definition dialgebra_enrichment_mor
             {x y : C₁}
             (f : F x --> G x)
             (g : F y --> G y)
    : V
    := EV _ _
         (dialgebra_enrichment_mor_left f g)
         (dialgebra_enrichment_mor_right f g).

  Definition dialgebra_enrichment_mor_incl
             {x y : C₁}
             (f : F x --> G x)
             (g : F y --> G y)
    : dialgebra_enrichment_mor f g --> E₁ x , y
    := EqualizerArrow
         (EV _ _
             (dialgebra_enrichment_mor_left f g)
             (dialgebra_enrichment_mor_right f g)).

  Definition dialgebra_enrichment_mor_incl_eq
             {x y : C₁}
             (f : F x --> G x)
             (g : F y --> G y)
    : dialgebra_enrichment_mor_incl f g · dialgebra_enrichment_mor_left f g
      =
      dialgebra_enrichment_mor_incl f g · dialgebra_enrichment_mor_right f g.
  Show proof.
    exact (EqualizerEqAr
             (EV _ _
                (dialgebra_enrichment_mor_left f g)
                (dialgebra_enrichment_mor_right f g))).

  Definition dialgebra_enrichment_mor_eq_of_mor
             {x y : C₁}
             (f : F x --> G x)
             (g : F y --> G y)
             {v : V}
             {φ φ : v --> dialgebra_enrichment_mor f g}
             (p : φ · dialgebra_enrichment_mor_incl f g
                  =
                  φ · dialgebra_enrichment_mor_incl f g)
    : φ = φ.
  Show proof.
    use (isEqualizerInsEq
           (pr22 (EV _ _
                     (dialgebra_enrichment_mor_left f g)
                     (dialgebra_enrichment_mor_right f g)))).
    exact p.

  Definition dialgebra_enrichment_id_eq
             {x : C₁}
             (f : F x --> G x)
    : enriched_id E₁ x · dialgebra_enrichment_mor_left f f
      =
      enriched_id E₁ x · dialgebra_enrichment_mor_right f f.
  Show proof.
    unfold dialgebra_enrichment_mor_left, dialgebra_enrichment_mor_right.
    rewrite !assoc.
    rewrite !functor_enrichment_id.
    rewrite enriched_id_precomp_arr.
    rewrite enriched_id_postcomp_arr.
    apply idpath.

  Definition dialgebra_enrichment_id
             {x : C₁}
             (f : F x --> G x)
    : I_{V} --> dialgebra_enrichment_mor f f.
  Show proof.
    use EqualizerIn.
    - exact (enriched_id E₁ x).
    - exact (dialgebra_enrichment_id_eq f).

  Definition dialgebra_enrichment_id_incl
             {x : C₁}
             (f : F x --> G x)
    : dialgebra_enrichment_id f · dialgebra_enrichment_mor_incl f f
      =
      enriched_id E₁ x.
  Show proof.
    apply EqualizerCommutes.

  Definition dialgebra_enrichment_comp_mor
             {x y z : C₁}
             (f₁ : F x --> G x)
             (f₂ : F y --> G y)
             (f₃ : F z --> G z)
    : dialgebra_enrichment_mor f₂ f₃ dialgebra_enrichment_mor f₁ f₂
      -->
      E₁ x, z
    := dialgebra_enrichment_mor_incl f₂ f₃ #⊗ dialgebra_enrichment_mor_incl f₁ f₂
       · enriched_comp _ _ _ _.

  Definition dialgebra_enrichment_comp_eq
             {x y z : C₁}
             (f₁ : F x --> G x)
             (f₂ : F y --> G y)
             (f₃ : F z --> G z)
    : dialgebra_enrichment_comp_mor f₁ f₂ f₃
      · dialgebra_enrichment_mor_left f₁ f₃
      =
      dialgebra_enrichment_comp_mor f₁ f₂ f₃
      · dialgebra_enrichment_mor_right f₁ f₃.
  Show proof.
    unfold dialgebra_enrichment_comp_mor.
    unfold dialgebra_enrichment_mor_left, dialgebra_enrichment_mor_right.
    rewrite !assoc'.
    rewrite !(maponpaths (λ z, _ · z) (assoc _ _ _)).
    rewrite !functor_enrichment_comp.
    rewrite !assoc'.
    rewrite enriched_comp_precomp_arr.
    rewrite enriched_comp_postcomp_arr.
    rewrite !assoc.
    rewrite <- !tensor_comp_mor.
    rewrite !id_right.
    etrans.
    {
      apply maponpaths_2.
      apply maponpaths.
      rewrite !assoc'.
      exact (dialgebra_enrichment_mor_incl_eq f₁ f₂).
    }
    unfold dialgebra_enrichment_mor_right.
    rewrite !assoc.
    rewrite tensor_comp_l_id_r.
    rewrite !assoc'.
    rewrite <- precomp_postcomp_arr_assoc.
    rewrite !assoc.
    apply maponpaths_2.
    rewrite <- tensor_comp_mor.
    rewrite id_right.
    apply maponpaths_2.
    rewrite !assoc'.
    exact (dialgebra_enrichment_mor_incl_eq f₂ f₃).

  Definition dialgebra_enrichment_comp
             {x y z : C₁}
             (f₁ : F x --> G x)
             (f₂ : F y --> G y)
             (f₃ : F z --> G z)
    : dialgebra_enrichment_mor f₂ f₃ dialgebra_enrichment_mor f₁ f₂
      -->
      dialgebra_enrichment_mor f₁ f₃.
  Show proof.
    use EqualizerIn.
    - exact (dialgebra_enrichment_comp_mor f₁ f₂ f₃).
    - exact (dialgebra_enrichment_comp_eq f₁ f₂ f₃).

  Definition dialgebra_enrichment_comp_incl
             {x y z : C₁}
             (f₁ : F x --> G x)
             (f₂ : F y --> G y)
             (f₃ : F z --> G z)
    : dialgebra_enrichment_comp f₁ f₂ f₃ · dialgebra_enrichment_mor_incl f₁ f₃
      =
      dialgebra_enrichment_comp_mor f₁ f₂ f₃.
  Show proof.
    apply EqualizerCommutes.

  Definition dialgebra_enrichment_from_arr_eq
             {x y : C₁}
             {f : F x --> G x}
             {g : F y --> G y}
             (h : x --> y)
             (p : f · # G h = # F h · g)
    : enriched_from_arr E₁ h · dialgebra_enrichment_mor_left f g
      =
      enriched_from_arr E₁ h · dialgebra_enrichment_mor_right f g.
  Show proof.
    unfold dialgebra_enrichment_mor_left, dialgebra_enrichment_mor_right.
    rewrite !assoc.
    rewrite <- !functor_enrichment_from_arr.
    rewrite enriched_from_arr_precomp.
    rewrite enriched_from_arr_postcomp.
    rewrite p.
    apply idpath.

  Definition dialgebra_enrichment_from_arr
             {x y : C₁}
             {f : F x --> G x}
             {g : F y --> G y}
             (h : x --> y)
             (p : f · # G h = # F h · g)
    : I_{V} --> dialgebra_enrichment_mor f g.
  Show proof.
    use EqualizerIn.
    - exact (enriched_from_arr E₁ h).
    - exact (dialgebra_enrichment_from_arr_eq h p).

  Definition dialgebra_enrichment_from_arr_incl
             {x y : C₁}
             {f : F x --> G x}
             {g : F y --> G y}
             (h : x --> y)
             (p : f · # G h = # F h · g)
    : dialgebra_enrichment_from_arr h p · dialgebra_enrichment_mor_incl f g
      =
      enriched_from_arr E₁ h.
  Show proof.
    apply EqualizerCommutes.

  Definition dialgebra_enrichment_to_arr_mor
             {x y : C₁}
             {f : F x --> G x}
             {g : F y --> G y}
             (h : I_{V} --> dialgebra_enrichment_mor f g)
    : x --> y
    := enriched_to_arr E₁ (h · dialgebra_enrichment_mor_incl _ _).

  Definition dialgebra_enrichment_to_arr_eq
             {x y : C₁}
             {f : F x --> G x}
             {g : F y --> G y}
             (h : I_{V} --> dialgebra_enrichment_mor f g)
    : f · # G (dialgebra_enrichment_to_arr_mor h)
      =
      # F (dialgebra_enrichment_to_arr_mor h) · g.
  Show proof.
    unfold dialgebra_enrichment_to_arr_mor.
    use (invmaponpathsweq (_ ,, isweq_enriched_from_arr E₂ _ _)).
    cbn.
    rewrite !enriched_from_arr_comp.
    rewrite (functor_enrichment_from_arr FE).
    rewrite (functor_enrichment_from_arr GE).
    rewrite !enriched_from_to_arr.
    pose (dialgebra_enrichment_mor_incl_eq f g) as p.
    unfold dialgebra_enrichment_mor_left in p.
    unfold dialgebra_enrichment_mor_right in p.
    rewrite !assoc in p.
    etrans.
    {
      rewrite mon_linvunitor_I_mon_rinvunitor_I.
      rewrite tensor_split'.
      rewrite !assoc.
      rewrite <- tensor_rinvunitor.
      rewrite !assoc'.
      apply maponpaths.
      refine (_ @ p).
      rewrite !assoc'.
      do 2 apply maponpaths.
      rewrite !assoc.
      apply idpath.
    }
    refine (!_).
    etrans.
    {
      rewrite tensor_split.
      rewrite !assoc.
      rewrite <- tensor_linvunitor.
      apply idpath.
    }
    rewrite !assoc'.
    do 3 apply maponpaths.
    rewrite !assoc.
    apply idpath.

  Definition dialgebra_enrichment_data
    : enrichment_data (dialgebra F G) V.
  Show proof.
    simple refine (_ ,, _ ,, _ ,, _ ,, _).
    - exact (λ f g, dialgebra_enrichment_mor (pr2 f) (pr2 g)).
    - exact (λ f, dialgebra_enrichment_id (pr2 f)).
    - exact (λ f₁ f₂ f₃, dialgebra_enrichment_comp (pr2 f₁) (pr2 f₂) (pr2 f₃)).
    - exact (λ f g τ, dialgebra_enrichment_from_arr (pr1 τ) (pr2 τ)).
    - refine (λ f g τ, dialgebra_enrichment_to_arr_mor τ ,, _).
      exact (dialgebra_enrichment_to_arr_eq τ).

  Definition dialgebra_enrichment_laws
    : enrichment_laws dialgebra_enrichment_data.
  Show proof.
    repeat split.
    - intros f g.
      use dialgebra_enrichment_mor_eq_of_mor.
      cbn.
      rewrite !assoc'.
      rewrite dialgebra_enrichment_comp_incl.
      unfold dialgebra_enrichment_comp_mor.
      rewrite !assoc.
      refine (!_).
      etrans.
      {
        apply maponpaths_2.
        refine (!_).
        apply tensor_comp_mor.
      }
      rewrite id_left.
      rewrite dialgebra_enrichment_id_incl.
      rewrite tensor_split.
      rewrite !assoc'.
      rewrite <- enrichment_id_left.
      rewrite tensor_lunitor.
      apply idpath.
    - intros f g.
      use dialgebra_enrichment_mor_eq_of_mor.
      cbn.
      rewrite !assoc'.
      rewrite dialgebra_enrichment_comp_incl.
      unfold dialgebra_enrichment_comp_mor.
      rewrite !assoc.
      refine (!_).
      etrans.
      {
        apply maponpaths_2.
        refine (!_).
        apply tensor_comp_mor.
      }
      rewrite id_left.
      rewrite dialgebra_enrichment_id_incl.
      rewrite tensor_split'.
      rewrite !assoc'.
      rewrite <- enrichment_id_right.
      rewrite tensor_runitor.
      apply idpath.
    - intros w x y z.
      use dialgebra_enrichment_mor_eq_of_mor.
      cbn.
      rewrite !assoc'.
      rewrite !dialgebra_enrichment_comp_incl.
      unfold dialgebra_enrichment_comp_mor.
      rewrite !assoc.
      etrans.
      {
        apply maponpaths_2.
        refine (!_).
        apply tensor_comp_mor.
      }
      rewrite id_left.
      rewrite !dialgebra_enrichment_comp_incl.
      unfold dialgebra_enrichment_comp_mor.
      etrans.
      {
        apply maponpaths_2.
        apply tensor_comp_r_id_r.
      }
      rewrite !assoc'.
      etrans.
      {
        apply maponpaths.
        apply enrichment_assoc.
      }
      rewrite !assoc.
      apply maponpaths_2.
      etrans.
      {
        apply maponpaths_2.
        apply tensor_lassociator.
      }
      rewrite !assoc'.
      apply maponpaths.
      refine (!(tensor_comp_mor _ _ _ _) @ _ @ tensor_comp_mor _ _ _ _).
      rewrite id_left, id_right.
      apply maponpaths.
      rewrite dialgebra_enrichment_comp_incl.
      apply idpath.
    - intros x y f.
      use subtypePath.
      {
        intro.
        apply homset_property.
      }
      cbn.
      unfold dialgebra_enrichment_to_arr_mor.
      rewrite dialgebra_enrichment_from_arr_incl.
      apply enriched_to_from_arr.
    - intros x y f.
      cbn.
      use dialgebra_enrichment_mor_eq_of_mor.
      rewrite dialgebra_enrichment_from_arr_incl.
      unfold dialgebra_enrichment_to_arr_mor.
      rewrite enriched_from_to_arr.
      apply idpath.
    - intros f.
      use subtypePath.
      {
        intro.
        apply homset_property.
      }
      cbn.
      unfold dialgebra_enrichment_to_arr_mor.
      rewrite dialgebra_enrichment_id_incl.
      rewrite enriched_to_arr_id.
      apply idpath.
    - intros x y z f g.
      use subtypePath.
      {
        intro.
        apply homset_property.
      }
      cbn.
      unfold dialgebra_enrichment_to_arr_mor.
      rewrite !assoc'.
      rewrite dialgebra_enrichment_comp_incl.
      etrans.
      {
        apply (enriched_to_arr_comp E₁ (pr1 f) (pr1 g)).
      }
      apply maponpaths.
      rewrite !assoc'.
      apply maponpaths.
      unfold dialgebra_enrichment_comp_mor.
      rewrite !assoc.
      apply maponpaths_2.
      refine (_ @ tensor_comp_mor _ _ _ _).
      rewrite !dialgebra_enrichment_from_arr_incl.
      apply idpath.

  Definition dialgebra_enrichment
    : enrichment (dialgebra F G) V.
  Show proof.
    simple refine (_ ,, _).
    - exact dialgebra_enrichment_data.
    - exact dialgebra_enrichment_laws.

  Proposition dialgebra_enrichment_precomp_arr
              {f g : dialgebra F G}
              (h : dialgebra F G)
              (τ : f --> g)
    : precomp_arr dialgebra_enrichment h τ · dialgebra_enrichment_mor_incl _ _
      =
      dialgebra_enrichment_mor_incl _ _ · precomp_arr _ _ (pr1 τ).
  Show proof.
    unfold precomp_arr.
    cbn.
    rewrite !assoc'.
    rewrite dialgebra_enrichment_comp_incl.
    unfold dialgebra_enrichment_comp_mor.
    rewrite !assoc.
    apply maponpaths_2.
    rewrite !assoc'.
    rewrite <- tensor_comp_mor.
    rewrite id_left.
    rewrite dialgebra_enrichment_from_arr_incl.
    rewrite tensor_split'.
    rewrite !assoc.
    apply maponpaths_2.
    rewrite tensor_rinvunitor.
    apply idpath.

  Proposition dialgebra_enrichment_postcomp_arr
              {f g : dialgebra F G}
              (h : dialgebra F G)
              (τ : f --> g)
    : postcomp_arr dialgebra_enrichment h τ · dialgebra_enrichment_mor_incl _ _
      =
      dialgebra_enrichment_mor_incl _ _ · postcomp_arr _ _ (pr1 τ).
  Show proof.
    unfold postcomp_arr.
    cbn.
    rewrite !assoc'.
    rewrite dialgebra_enrichment_comp_incl.
    unfold dialgebra_enrichment_comp_mor.
    rewrite !assoc.
    apply maponpaths_2.
    rewrite !assoc'.
    rewrite <- tensor_comp_mor.
    rewrite id_left.
    rewrite dialgebra_enrichment_from_arr_incl.
    rewrite tensor_split.
    rewrite !assoc.
    apply maponpaths_2.
    rewrite tensor_linvunitor.
    apply idpath.

2. Enrichment of the first projection
  Definition dialgebra_pr1_enrichment
    : functor_enrichment (dialgebra_pr1 F G) dialgebra_enrichment E₁.
  Show proof.
    simple refine (_ ,, _).
    - exact (λ f g, dialgebra_enrichment_mor_incl (pr2 f) (pr2 g)).
    - repeat split.
      + abstract
          (intro f ; cbn ;
           apply dialgebra_enrichment_id_incl).
      + abstract
          (intros x y z ; cbn ;
           apply dialgebra_enrichment_comp_incl).
      + abstract
          (intros x y f ; cbn ;
           refine (!_) ;
           apply dialgebra_enrichment_from_arr_incl).

  Definition dialgebra_nat_trans_enrichment
    : nat_trans_enrichment
        (dialgebra_nat_trans F G)
        (functor_comp_enrichment dialgebra_pr1_enrichment FE)
        (functor_comp_enrichment dialgebra_pr1_enrichment GE).
  Show proof.
    use nat_trans_enrichment_via_comp.
    intros f g ; cbn ; unfold dialgebra_nat_trans_data.
    rewrite !assoc'.
    exact (dialgebra_enrichment_mor_incl_eq (pr2 f) (pr2 g)).

3. Enrichment of functors to dialgebras
  Section FunctorToDialgebraEnrichment.
    Context {C₀ : category}
            {E₀ : enrichment C₀ V}
            {K : C₀ C₁}
            {EK : functor_enrichment K E₀ E₁}
            (τ : K F K G)
            (Eτ : nat_trans_enrichment
                    τ
                    (functor_comp_enrichment EK FE)
                    (functor_comp_enrichment EK GE)).

    Definition nat_trans_to_dialgebra_enrichment_mor_eq
               (x y : C₀)
      : EK x y · dialgebra_enrichment_mor_left (τ x) (τ y)
        =
        EK x y · dialgebra_enrichment_mor_right (τ x) (τ y).
    Show proof.
      unfold dialgebra_enrichment_mor_left, dialgebra_enrichment_mor_right.
      rewrite !assoc.
      exact (nat_trans_enrichment_to_comp Eτ x y).

    Definition nat_trans_to_dialgebra_enrichment_mor
               (x y : C₀)
      : E₀ x , y --> dialgebra_enrichment_mor (τ x) (τ y).
    Show proof.
      use EqualizerIn.
      - exact (EK x y).
      - exact (nat_trans_to_dialgebra_enrichment_mor_eq x y).

    Definition nat_trans_to_dialgebra_enrichment_mor_incl
               (x y : C₀)
      : nat_trans_to_dialgebra_enrichment_mor x y
        · dialgebra_enrichment_mor_incl (τ x) (τ y)
        =
        EK x y.
    Show proof.
      apply EqualizerCommutes.

    Definition nat_trans_to_dialgebra_enrichment
      : functor_enrichment
          (nat_trans_to_dialgebra K τ)
          E₀
          dialgebra_enrichment.
    Show proof.
      simple refine (_ ,, _).
      - exact nat_trans_to_dialgebra_enrichment_mor.
      - repeat split.
        + abstract
            (intros x ;
             use dialgebra_enrichment_mor_eq_of_mor ; cbn ;
             rewrite !assoc' ;
             rewrite nat_trans_to_dialgebra_enrichment_mor_incl ;
             rewrite dialgebra_enrichment_id_incl ;
             apply (functor_enrichment_id EK)).
        + abstract
            (intros x y z ;
             use dialgebra_enrichment_mor_eq_of_mor ; cbn ;
             rewrite !assoc' ;
             rewrite nat_trans_to_dialgebra_enrichment_mor_incl ;
             rewrite dialgebra_enrichment_comp_incl ;
             refine (functor_enrichment_comp EK x y z @ _) ;
             unfold dialgebra_enrichment_comp_mor ;
             rewrite !assoc ;
             apply maponpaths_2 ;
             refine (_ @ tensor_comp_mor _ _ _ _) ;
             rewrite !nat_trans_to_dialgebra_enrichment_mor_incl ;
             apply idpath).
        + abstract
            (intros x y f ;
             use dialgebra_enrichment_mor_eq_of_mor ; cbn ;
             rewrite !assoc' ;
             rewrite nat_trans_to_dialgebra_enrichment_mor_incl ;
             rewrite dialgebra_enrichment_from_arr_incl ;
             apply (functor_enrichment_from_arr EK)).

    Definition nat_trans_to_dialgebra_pr1_enrichment
      : nat_trans_enrichment
          (nat_trans_to_dialgebra_pr1 K τ)
          (functor_comp_enrichment
             nat_trans_to_dialgebra_enrichment
             dialgebra_pr1_enrichment)
          EK.
    Show proof.
      use nat_trans_enrichment_via_comp.
      intros x y ; cbn.
      rewrite precomp_arr_id, id_right.
      rewrite postcomp_arr_id, id_right.
      refine (!_).
      apply nat_trans_to_dialgebra_enrichment_mor_incl.
  End FunctorToDialgebraEnrichment.

4. Enrichment of natural transformations to dialgebras
  Definition make_nat_trans_to_dialgebra_enrichment
             {C₀ : category}
             {E₀ : enrichment C₀ V}
             {H₁ H₂ : C₀ dialgebra F G}
             {EH₁ : functor_enrichment H₁ E₀ dialgebra_enrichment}
             {EH₂ : functor_enrichment H₂ E₀ dialgebra_enrichment}
             {τ : H₁ dialgebra_pr1 F G H₂ dialgebra_pr1 F G}
             (Eτ : nat_trans_enrichment
                     τ
                     (functor_comp_enrichment EH₁ dialgebra_pr1_enrichment)
                     (functor_comp_enrichment EH₂ dialgebra_pr1_enrichment))
             (p : (x : C₀), pr2 (H₁ x) · # G x) = # F x) · pr2 (H₂ x))
    : nat_trans_enrichment
        (build_nat_trans_to_dialgebra _ _ τ p)
        EH₁
        EH₂.
  Show proof.
    use nat_trans_enrichment_via_comp.
    intros x y ; cbn.
    use dialgebra_enrichment_mor_eq_of_mor.
    rewrite !assoc'.
    etrans.
    {
      apply maponpaths.
      apply dialgebra_enrichment_precomp_arr.
    }
    refine (!_).
    etrans.
    {
      apply maponpaths.
      apply dialgebra_enrichment_postcomp_arr.
    }
    refine (!_).
    rewrite !assoc.
    exact (nat_trans_enrichment_to_comp Eτ x y).
End EnrichedDialgebras.