Lax reflexive globular maps

Content created by Egbert Rijke.

Created on 2024-12-03.
Last modified on 2024-12-03.

{-# OPTIONS --guardedness #-}

module globular-types.lax-reflexive-globular-maps where
Imports 
open import foundation.universe-levels

open import globular-types.globular-maps
open import globular-types.reflexive-globular-types

Idea

A lax reflexive globular map between two reflexive globular types G and H is a globular map f : G → H equipped with a family of 2-cells

  (x : G₀) → H₂ (refl H (f₀ x)) (f₁ (refl G x))

from the image of the reflexivity cell at x in G to the reflexivity cell at f₀ x, such that the globular map f' : G' x y → H' (f₀ x) (f₀ y) is again lax reflexive.

Lack of composition for lax reflexive globular maps

Note that the lax reflexive globular maps lack composition. For the composition of g and f to exist, there should be a 2-cell from g (f (refl G x)) to refl K (g (f x)), we need to compose the 2-cell that g preserves reflexivity with the action of g on the 2-cell that f preserves reflexivity. However, since the reflexive globular type G is not assumed to be transitive, it might lack such instances of the compositions.

Lax reflexive globular maps versus the morphisms of presheaves on the reflexive globe category

When reflexive globular types are viewed as type valued presheaves over the reflexive globe category, the resulting notion of morphism is that of reflexive globular maps, which is stricter than the notion of lax reflexive globular maps.

Lax versus colax

The notion of colax reflexive globular map is almost the same, except with the direction of the 2-cell reversed. In general, the direction of lax coherence cells is determined by applying the morphism componentwise first, and then the operations, while the direction of colax coherence cells is determined by first applying the operations and then the morphism.

Definitions

The predicate of laxly preserving reflexivity

record
  is-lax-reflexive-globular-map
    {l1 l2 l3 l4 : Level}
    (G : Reflexive-Globular-Type l1 l2) (H : Reflexive-Globular-Type l3 l4)
    (f : globular-map-Reflexive-Globular-Type G H) :
    UU (l1 ⊔ l2 ⊔ l4)
  where
  coinductive

  field
    preserves-refl-1-cell-is-lax-reflexive-globular-map :
      (x : 0-cell-Reflexive-Globular-Type G) →
      2-cell-Reflexive-Globular-Type H
        ( refl-1-cell-Reflexive-Globular-Type H)
        ( 1-cell-globular-map f (refl-1-cell-Reflexive-Globular-Type G {x}))

  field
    is-lax-reflexive-1-cell-globular-map-is-lax-reflexive-globular-map :
      {x y : 0-cell-Reflexive-Globular-Type G} →
      is-lax-reflexive-globular-map
        ( 1-cell-reflexive-globular-type-Reflexive-Globular-Type G x y)
        ( 1-cell-reflexive-globular-type-Reflexive-Globular-Type H _ _)
        ( 1-cell-globular-map-globular-map-Reflexive-Globular-Type G H f)

open is-lax-reflexive-globular-map public

Lax reflexive globular maps

record
  lax-reflexive-globular-map
    {l1 l2 l3 l4 : Level}
    (G : Reflexive-Globular-Type l1 l2)
    (H : Reflexive-Globular-Type l3 l4) :
    UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  where

  field
    globular-map-lax-reflexive-globular-map :
      globular-map-Reflexive-Globular-Type G H

  0-cell-lax-reflexive-globular-map :
    0-cell-Reflexive-Globular-Type G → 0-cell-Reflexive-Globular-Type H
  0-cell-lax-reflexive-globular-map =
    0-cell-globular-map globular-map-lax-reflexive-globular-map

  1-cell-lax-reflexive-globular-map :
    {x y : 0-cell-Reflexive-Globular-Type G} →
    1-cell-Reflexive-Globular-Type G x y →
    1-cell-Reflexive-Globular-Type H
      ( 0-cell-lax-reflexive-globular-map x)
      ( 0-cell-lax-reflexive-globular-map y)
  1-cell-lax-reflexive-globular-map =
    1-cell-globular-map globular-map-lax-reflexive-globular-map

  1-cell-globular-map-lax-reflexive-globular-map :
    {x y : 0-cell-Reflexive-Globular-Type G} →
    globular-map-Reflexive-Globular-Type
      ( 1-cell-reflexive-globular-type-Reflexive-Globular-Type G x y)
      ( 1-cell-reflexive-globular-type-Reflexive-Globular-Type H
        ( 0-cell-lax-reflexive-globular-map x)
        ( 0-cell-lax-reflexive-globular-map y))
  1-cell-globular-map-lax-reflexive-globular-map =
    1-cell-globular-map-globular-map globular-map-lax-reflexive-globular-map

  field
    is-lax-reflexive-lax-reflexive-globular-map :
      is-lax-reflexive-globular-map G H
        globular-map-lax-reflexive-globular-map

  preserves-refl-1-cell-lax-reflexive-globular-map :
    (x : 0-cell-Reflexive-Globular-Type G) →
    2-cell-Reflexive-Globular-Type H
      ( refl-1-cell-Reflexive-Globular-Type H)
      ( 1-cell-lax-reflexive-globular-map
        ( refl-1-cell-Reflexive-Globular-Type G {x}))
  preserves-refl-1-cell-lax-reflexive-globular-map =
    preserves-refl-1-cell-is-lax-reflexive-globular-map
      is-lax-reflexive-lax-reflexive-globular-map

  is-lax-reflexive-2-cell-globular-map-is-lax-reflexive-globular-map :
    {x y : 0-cell-Reflexive-Globular-Type G} →
    is-lax-reflexive-globular-map
      ( 1-cell-reflexive-globular-type-Reflexive-Globular-Type G x y)
      ( 1-cell-reflexive-globular-type-Reflexive-Globular-Type H
        ( 0-cell-lax-reflexive-globular-map x)
        ( 0-cell-lax-reflexive-globular-map y))
      ( 1-cell-globular-map-lax-reflexive-globular-map)
  is-lax-reflexive-2-cell-globular-map-is-lax-reflexive-globular-map =
    is-lax-reflexive-1-cell-globular-map-is-lax-reflexive-globular-map
      is-lax-reflexive-lax-reflexive-globular-map

  1-cell-lax-reflexive-globular-map-lax-reflexive-globular-map :
    {x y : 0-cell-Reflexive-Globular-Type G} →
    lax-reflexive-globular-map
      ( 1-cell-reflexive-globular-type-Reflexive-Globular-Type G x y)
      ( 1-cell-reflexive-globular-type-Reflexive-Globular-Type H
        ( 0-cell-lax-reflexive-globular-map x)
        ( 0-cell-lax-reflexive-globular-map y))
  globular-map-lax-reflexive-globular-map
    1-cell-lax-reflexive-globular-map-lax-reflexive-globular-map =
    1-cell-globular-map-lax-reflexive-globular-map
  is-lax-reflexive-lax-reflexive-globular-map
    1-cell-lax-reflexive-globular-map-lax-reflexive-globular-map =
    is-lax-reflexive-2-cell-globular-map-is-lax-reflexive-globular-map

open lax-reflexive-globular-map public

The identity lax reflexive globular map

map-id-lax-reflexive-globular-map :
  {l1 l2 : Level} (G : Reflexive-Globular-Type l1 l2) →
  globular-map-Reflexive-Globular-Type G G
map-id-lax-reflexive-globular-map G = id-globular-map _

is-lax-reflexive-id-lax-reflexive-globular-map :
  {l1 l2 : Level} (G : Reflexive-Globular-Type l1 l2) →
  is-lax-reflexive-globular-map G G (map-id-lax-reflexive-globular-map G)
preserves-refl-1-cell-is-lax-reflexive-globular-map
  ( is-lax-reflexive-id-lax-reflexive-globular-map G)
  x =
  refl-2-cell-Reflexive-Globular-Type G
is-lax-reflexive-1-cell-globular-map-is-lax-reflexive-globular-map
  ( is-lax-reflexive-id-lax-reflexive-globular-map G) =
  is-lax-reflexive-id-lax-reflexive-globular-map
    ( 1-cell-reflexive-globular-type-Reflexive-Globular-Type G _ _)

id-lax-reflexive-globular-map :
  {l1 l2 : Level} (G : Reflexive-Globular-Type l1 l2) →
  lax-reflexive-globular-map G G
globular-map-lax-reflexive-globular-map
  ( id-lax-reflexive-globular-map G) =
  map-id-lax-reflexive-globular-map G
is-lax-reflexive-lax-reflexive-globular-map
  ( id-lax-reflexive-globular-map G) =
  ( is-lax-reflexive-id-lax-reflexive-globular-map G)

See also

Recent changes