Morphisms of coalgebras of polynomial endofunctors

module trees.morphisms-coalgebras-polynomial-endofunctors where
Imports
open import foundation.commuting-squares-of-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functoriality-dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.structure-identity-principle
open import foundation.universe-levels

open import trees.coalgebras-polynomial-endofunctors
open import trees.polynomial-endofunctors

Idea

A morphism of coalgebras of a polynomial endofunctor P A B consists of a function f : X → Y between their underlying types, equipped with a homotopy witnessing that the square

              f
      X -------------> Y
      |                |
      |                |
      V                V
  P A B X ---------> P A B Y
           P A B f

commutes.

Definitions

Morphisms of coalgebras for polynomial endofunctors

hom-coalgebra-polynomial-endofunctor :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : A  UU l2}
  (X : coalgebra-polynomial-endofunctor l3 A B) 
  (Y : coalgebra-polynomial-endofunctor l4 A B)  UU (l1  l2  l3  l4)
hom-coalgebra-polynomial-endofunctor {A = A} {B} X Y =
  Σ ( type-coalgebra-polynomial-endofunctor X 
      type-coalgebra-polynomial-endofunctor Y)
    ( λ f 
      ( coherence-square-maps f
         ( structure-coalgebra-polynomial-endofunctor X)
         ( structure-coalgebra-polynomial-endofunctor Y)
         ( map-polynomial-endofunctor A B f)))

map-hom-coalgebra-polynomial-endofunctor :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : A  UU l2}
  (X : coalgebra-polynomial-endofunctor l3 A B) 
  (Y : coalgebra-polynomial-endofunctor l4 A B) 
  hom-coalgebra-polynomial-endofunctor X Y 
  type-coalgebra-polynomial-endofunctor X 
  type-coalgebra-polynomial-endofunctor Y
map-hom-coalgebra-polynomial-endofunctor X Y f = pr1 f

structure-hom-coalgebra-polynomial-endofunctor :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : A  UU l2}
  (X : coalgebra-polynomial-endofunctor l3 A B) 
  (Y : coalgebra-polynomial-endofunctor l4 A B) 
  (f : hom-coalgebra-polynomial-endofunctor X Y) 
  coherence-square-maps
    ( map-hom-coalgebra-polynomial-endofunctor X Y f)
    ( structure-coalgebra-polynomial-endofunctor X)
    ( structure-coalgebra-polynomial-endofunctor Y)
    ( map-polynomial-endofunctor A B
      ( map-hom-coalgebra-polynomial-endofunctor X Y f))
structure-hom-coalgebra-polynomial-endofunctor X Y f = pr2 f

Properties

The identity type of morphisms of coalgebras of polynomial endofunctors

module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : A  UU l2}
  (X : coalgebra-polynomial-endofunctor l3 A B)
  (Y : coalgebra-polynomial-endofunctor l4 A B)
  (f : hom-coalgebra-polynomial-endofunctor X Y)
  where

  htpy-hom-coalgebra-polynomial-endofunctor :
    (g : hom-coalgebra-polynomial-endofunctor X Y)  UU (l1  l2  l3  l4)
  htpy-hom-coalgebra-polynomial-endofunctor g =
    Σ ( map-hom-coalgebra-polynomial-endofunctor X Y f ~
        map-hom-coalgebra-polynomial-endofunctor X Y g)
      ( λ H 
        ( ( structure-hom-coalgebra-polynomial-endofunctor X Y f) ∙h
          ( structure-coalgebra-polynomial-endofunctor Y ·l H)) ~
        ( ( ( htpy-polynomial-endofunctor A B H) ·r
            ( structure-coalgebra-polynomial-endofunctor X)) ∙h
          ( structure-hom-coalgebra-polynomial-endofunctor X Y g)))

  refl-htpy-hom-coalgebra-polynomial-endofunctor :
    htpy-hom-coalgebra-polynomial-endofunctor f
  pr1 refl-htpy-hom-coalgebra-polynomial-endofunctor = refl-htpy
  pr2 refl-htpy-hom-coalgebra-polynomial-endofunctor z =
    ( right-unit) 
    ( inv
      ( ap
        ( concat'
          ( map-polynomial-endofunctor A B
            ( map-hom-coalgebra-polynomial-endofunctor X Y f)
            ( structure-coalgebra-polynomial-endofunctor X z))
          ( structure-hom-coalgebra-polynomial-endofunctor X Y f z))
        ( coh-refl-htpy-polynomial-endofunctor A B
          ( map-hom-coalgebra-polynomial-endofunctor X Y f)
          ( structure-coalgebra-polynomial-endofunctor X z))))

  htpy-eq-hom-coalgebra-polynomial-endofunctor :
    (g : hom-coalgebra-polynomial-endofunctor X Y) 
    f  g  htpy-hom-coalgebra-polynomial-endofunctor g
  htpy-eq-hom-coalgebra-polynomial-endofunctor .f refl =
    refl-htpy-hom-coalgebra-polynomial-endofunctor

  is-contr-total-htpy-hom-coalgebra-polynomial-endofunctor :
    is-contr
      ( Σ ( hom-coalgebra-polynomial-endofunctor X Y)
          ( htpy-hom-coalgebra-polynomial-endofunctor))
  is-contr-total-htpy-hom-coalgebra-polynomial-endofunctor =
    is-contr-total-Eq-structure
      ( λ ( g :
            type-coalgebra-polynomial-endofunctor X 
            type-coalgebra-polynomial-endofunctor Y)
          ( G :
            coherence-square-maps g
              ( structure-coalgebra-polynomial-endofunctor X)
              ( structure-coalgebra-polynomial-endofunctor Y)
              ( map-polynomial-endofunctor A B g))
          ( H : map-hom-coalgebra-polynomial-endofunctor X Y f ~ g) 
          ( ( structure-hom-coalgebra-polynomial-endofunctor X Y f) ∙h
            ( structure-coalgebra-polynomial-endofunctor Y ·l H)) ~
          ( ( ( htpy-polynomial-endofunctor A B H) ·r
              ( structure-coalgebra-polynomial-endofunctor X)) ∙h
            ( G)))
      ( is-contr-total-htpy (map-hom-coalgebra-polynomial-endofunctor X Y f))
      ( map-hom-coalgebra-polynomial-endofunctor X Y f , refl-htpy)
      ( is-contr-equiv'
        ( Σ ( coherence-square-maps
              ( map-hom-coalgebra-polynomial-endofunctor X Y f)
              ( structure-coalgebra-polynomial-endofunctor X)
              ( structure-coalgebra-polynomial-endofunctor Y)
              ( map-polynomial-endofunctor A B
                ( map-hom-coalgebra-polynomial-endofunctor X Y f)))
            ( λ G 
              ( ( structure-hom-coalgebra-polynomial-endofunctor X Y f) ∙h
                ( refl-htpy)) ~
              ( G)))
        ( equiv-tot
          ( λ G 
            equiv-concat-htpy'
              ( ( structure-hom-coalgebra-polynomial-endofunctor X Y f) ∙h
                ( refl-htpy))
              ( λ x 
                ap
                  ( concat'
                    ( ( map-polynomial-endofunctor A B
                        ( map-hom-coalgebra-polynomial-endofunctor X Y f)
                        ( structure-coalgebra-polynomial-endofunctor X x)))
                    (G x))
                  ( inv
                    ( coh-refl-htpy-polynomial-endofunctor A B
                      ( map-hom-coalgebra-polynomial-endofunctor X Y f)
                      ( structure-coalgebra-polynomial-endofunctor X x))))))
        ( is-contr-total-htpy
          ( ( structure-hom-coalgebra-polynomial-endofunctor X Y f) ∙h
            ( refl-htpy))))

  is-equiv-htpy-eq-hom-coalgebra-polynomial-endofunctor :
    (g : hom-coalgebra-polynomial-endofunctor X Y) 
    is-equiv (htpy-eq-hom-coalgebra-polynomial-endofunctor g)
  is-equiv-htpy-eq-hom-coalgebra-polynomial-endofunctor =
    fundamental-theorem-id
      ( is-contr-total-htpy-hom-coalgebra-polynomial-endofunctor)
      ( htpy-eq-hom-coalgebra-polynomial-endofunctor)

  extensionality-hom-coalgebra-polynomial-endofunctor :
    (g : hom-coalgebra-polynomial-endofunctor X Y) 
    (f  g)  htpy-hom-coalgebra-polynomial-endofunctor g
  pr1 (extensionality-hom-coalgebra-polynomial-endofunctor g) =
    htpy-eq-hom-coalgebra-polynomial-endofunctor g
  pr2 (extensionality-hom-coalgebra-polynomial-endofunctor g) =
    is-equiv-htpy-eq-hom-coalgebra-polynomial-endofunctor g

  eq-htpy-hom-coalgebra-polynomial-endofunctor :
    (g : hom-coalgebra-polynomial-endofunctor X Y) 
    htpy-hom-coalgebra-polynomial-endofunctor g  f  g
  eq-htpy-hom-coalgebra-polynomial-endofunctor g =
    map-inv-is-equiv (is-equiv-htpy-eq-hom-coalgebra-polynomial-endofunctor g)