Equivalences between globular types

Content created by Fredrik Bakke.

Created on 2024-10-09.
Last modified on 2024-10-09.

{-# OPTIONS --guardedness #-}

module structured-types.equivalences-globular-types where
Imports 
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.identity-types
open import foundation.universe-levels

open import structured-types.globular-types

Idea

An equivalence f between globular types A and B is an equivalence F₀ of -cells, and for every pair of -cells x and y, an equivalence of -cells

  Fₙ₊₁ : (𝑛+1)-Cell A x y ≃ (𝑛+1)-Cell B (Fₙ x) (Fₙ y).

Definitions

Equivalences between globular types

record
  equiv-Globular-Type
  {l1 l2 l3 l4 : Level} (A : Globular-Type l1 l2) (B : Globular-Type l3 l4)
  : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  where
  coinductive
  field
    equiv-0-cell-equiv-Globular-Type :
      0-cell-Globular-Type A ≃ 0-cell-Globular-Type B

  map-0-cell-equiv-Globular-Type :
      0-cell-Globular-Type A → 0-cell-Globular-Type B
  map-0-cell-equiv-Globular-Type = map-equiv equiv-0-cell-equiv-Globular-Type

  field
    globular-type-1-cell-equiv-Globular-Type :
      {x y : 0-cell-Globular-Type A} →
      equiv-Globular-Type
        ( 1-cell-globular-type-Globular-Type A x y)
        ( 1-cell-globular-type-Globular-Type B
          ( map-0-cell-equiv-Globular-Type x)
          ( map-0-cell-equiv-Globular-Type y))

open equiv-Globular-Type public

module _
  {l1 l2 l3 l4 : Level}
  {A : Globular-Type l1 l2} {B : Globular-Type l3 l4}
  (F : equiv-Globular-Type A B)
  where

  equiv-1-cell-equiv-Globular-Type :
    {x y : 0-cell-Globular-Type A} →
    1-cell-Globular-Type A x y ≃
    1-cell-Globular-Type B
      ( map-0-cell-equiv-Globular-Type F x)
      ( map-0-cell-equiv-Globular-Type F y)
  equiv-1-cell-equiv-Globular-Type =
    equiv-0-cell-equiv-Globular-Type
      ( globular-type-1-cell-equiv-Globular-Type F)

  map-1-cell-equiv-Globular-Type :
    {x y : 0-cell-Globular-Type A} →
    1-cell-Globular-Type A x y →
    1-cell-Globular-Type B
      ( map-0-cell-equiv-Globular-Type F x)
      ( map-0-cell-equiv-Globular-Type F y)
  map-1-cell-equiv-Globular-Type =
    map-0-cell-equiv-Globular-Type (globular-type-1-cell-equiv-Globular-Type F)

module _
  {l1 l2 l3 l4 : Level}
  {A : Globular-Type l1 l2} {B : Globular-Type l3 l4}
  (F : equiv-Globular-Type A B)
  where

  equiv-2-cell-equiv-Globular-Type :
    {x y : 0-cell-Globular-Type A}
    {f g : 1-cell-Globular-Type A x y} →
    2-cell-Globular-Type A f g ≃
    2-cell-Globular-Type B
      ( map-1-cell-equiv-Globular-Type F f)
      ( map-1-cell-equiv-Globular-Type F g)
  equiv-2-cell-equiv-Globular-Type =
    equiv-1-cell-equiv-Globular-Type
      ( globular-type-1-cell-equiv-Globular-Type F)

  map-2-cell-equiv-Globular-Type :
    {x y : 0-cell-Globular-Type A}
    {f g : 1-cell-Globular-Type A x y} →
    2-cell-Globular-Type A f g →
    2-cell-Globular-Type B
      ( map-1-cell-equiv-Globular-Type F f)
      ( map-1-cell-equiv-Globular-Type F g)
  map-2-cell-equiv-Globular-Type =
    map-1-cell-equiv-Globular-Type (globular-type-1-cell-equiv-Globular-Type F)

module _
  {l1 l2 l3 l4 : Level}
  {A : Globular-Type l1 l2} {B : Globular-Type l3 l4}
  (F : equiv-Globular-Type A B)
  where

  equiv-3-cell-equiv-Globular-Type :
    {x y : 0-cell-Globular-Type A}
    {f g : 1-cell-Globular-Type A x y} →
    {H K : 2-cell-Globular-Type A f g} →
    3-cell-Globular-Type A H K ≃
    3-cell-Globular-Type B
      ( map-2-cell-equiv-Globular-Type F H)
      ( map-2-cell-equiv-Globular-Type F K)
  equiv-3-cell-equiv-Globular-Type =
    equiv-2-cell-equiv-Globular-Type
      ( globular-type-1-cell-equiv-Globular-Type F)

The identity equiv on a globular type

id-equiv-Globular-Type :
  {l1 l2 : Level} (A : Globular-Type l1 l2) → equiv-Globular-Type A A
id-equiv-Globular-Type A =
  λ where
  .equiv-0-cell-equiv-Globular-Type → id-equiv
  .globular-type-1-cell-equiv-Globular-Type {x} {y} →
    id-equiv-Globular-Type (1-cell-globular-type-Globular-Type A x y)

Composition of equivalences of globular types

comp-equiv-Globular-Type :
  {l1 l2 l3 l4 l5 l6 : Level}
  {A : Globular-Type l1 l2}
  {B : Globular-Type l3 l4}
  {C : Globular-Type l5 l6} →
  equiv-Globular-Type B C → equiv-Globular-Type A B → equiv-Globular-Type A C
comp-equiv-Globular-Type g f =
  λ where
  .equiv-0-cell-equiv-Globular-Type →
    equiv-0-cell-equiv-Globular-Type g ∘e equiv-0-cell-equiv-Globular-Type f
  .globular-type-1-cell-equiv-Globular-Type →
    comp-equiv-Globular-Type
      ( globular-type-1-cell-equiv-Globular-Type g)
      ( globular-type-1-cell-equiv-Globular-Type f)

Recent changes