Definition of a weak 2-category

weak2cat.agda

{-# OPTIONS --cubical #-}

module weak2cat where

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) public
open import Cubical.Core.Everything public
open import Cubical.Foundations.Everything public

open import Cubical.Data.Sigma

private
  variable
    ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level

record 2Cat ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Type (lsuc (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)) where
  field
    𝑜𝑏₀ : Type ℓ₁
    𝑜𝑏₁ : 𝑜𝑏₀ → 𝑜𝑏₀ → Type ℓ₂
    𝑜𝑏₂ : {x y z : 𝑜𝑏₀} → 𝑜𝑏₁ x y → 𝑜𝑏₁ x z → 𝑜𝑏₁ y z → Type ℓ₃
    𝑜𝑏₃ : {x y z w : 𝑜𝑏₀} {α : 𝑜𝑏₁ x y} {β : 𝑜𝑏₁ x z} {γ : 𝑜𝑏₁ y z}
      (𝑓₁ : 𝑜𝑏₂ α β γ) {δ : 𝑜𝑏₁ x w} {ε : 𝑜𝑏₁ y w} (𝑓₂ : 𝑜𝑏₂ α δ ε)
      {ζ : 𝑜𝑏₁ z w} (𝑓₃ : 𝑜𝑏₂ β δ ζ) (𝑓₄ : 𝑜𝑏₂ γ ε ζ) → Type ℓ₄
    isProp-𝑜𝑏₃ : {x y z w : 𝑜𝑏₀} {α : 𝑜𝑏₁ x y} {β : 𝑜𝑏₁ x z} {γ : 𝑜𝑏₁ y z}
      (𝑓₁ : 𝑜𝑏₂ α β γ) {δ : 𝑜𝑏₁ x w} {ε : 𝑜𝑏₁ y w} (𝑓₂ : 𝑜𝑏₂ α δ ε)
      {ζ : 𝑜𝑏₁ z w} (𝑓₃ : 𝑜𝑏₂ β δ ζ) (𝑓₄ : 𝑜𝑏₂ γ ε ζ) →
      isProp (𝑜𝑏₃ 𝑓₁ 𝑓₂ 𝑓₃ 𝑓₄)

    -- inner horn filling says that 𝑜𝑏₃ behaves like equality
    𝑜𝑏₃-𝑓𝑖𝑙𝑙ʸ : {x y z w v : 𝑜𝑏₀} {α : 𝑜𝑏₁ x y} {β : 𝑜𝑏₁ x z} {γ : 𝑜𝑏₁ y z}
      {𝑓₁ : 𝑜𝑏₂ α β γ} {δ : 𝑜𝑏₁ x w} {ε : 𝑜𝑏₁ y w} {𝑓₂ : 𝑜𝑏₂ α δ ε}
      {ζ : 𝑜𝑏₁ z w} {𝑓₃ : 𝑜𝑏₂ β δ ζ} {𝑓₄ : 𝑜𝑏₂ γ ε ζ}
      (Δ₁ : 𝑜𝑏₃ 𝑓₁ 𝑓₂ 𝑓₃ 𝑓₄) {η : 𝑜𝑏₁ x v} {θ : 𝑜𝑏₁ y v} {𝑓₅ : 𝑜𝑏₂ α η θ}
      {ι : 𝑜𝑏₁ z v} {𝑓₆ : 𝑜𝑏₂ β η ι} {𝑓₇ : 𝑜𝑏₂ γ θ ι}
      (Δ₂ : 𝑜𝑏₃ 𝑓₁ 𝑓₅ 𝑓₆ 𝑓₇) {κ : 𝑜𝑏₁ w v} {𝑓₈ : 𝑜𝑏₂ δ η κ}
      {𝑓₉ : 𝑜𝑏₂ ε θ κ} (Δ₃ : 𝑜𝑏₃ 𝑓₂ 𝑓₅ 𝑓₈ 𝑓₉) {𝑓₁₀ : 𝑜𝑏₂ ζ ι κ}
      (Δ₅ : 𝑜𝑏₃ 𝑓₄ 𝑓₇ 𝑓₉ 𝑓₁₀) → 𝑜𝑏₃ 𝑓₃ 𝑓₆ 𝑓₈ 𝑓₁₀
    𝑜𝑏₃-𝑓𝑖𝑙𝑙ᶻ : {x y z w v : 𝑜𝑏₀} {α : 𝑜𝑏₁ x y} {β : 𝑜𝑏₁ x z} {γ : 𝑜𝑏₁ y z}
      {𝑓₁ : 𝑜𝑏₂ α β γ} {δ : 𝑜𝑏₁ x w} {ε : 𝑜𝑏₁ y w} {𝑓₂ : 𝑜𝑏₂ α δ ε}
      {ζ : 𝑜𝑏₁ z w} {𝑓₃ : 𝑜𝑏₂ β δ ζ} {𝑓₄ : 𝑜𝑏₂ γ ε ζ}
      (Δ₁ : 𝑜𝑏₃ 𝑓₁ 𝑓₂ 𝑓₃ 𝑓₄) {η : 𝑜𝑏₁ x v} {θ : 𝑜𝑏₁ y v} {𝑓₅ : 𝑜𝑏₂ α η θ}
      {ι : 𝑜𝑏₁ z v} {𝑓₆ : 𝑜𝑏₂ β η ι} {𝑓₇ : 𝑜𝑏₂ γ θ ι}
      (Δ₂ : 𝑜𝑏₃ 𝑓₁ 𝑓₅ 𝑓₆ 𝑓₇) {κ : 𝑜𝑏₁ w v} {𝑓₈ : 𝑜𝑏₂ δ η κ}
      {𝑓₉ : 𝑜𝑏₂ ε θ κ} {𝑓₁₀ : 𝑜𝑏₂ ζ ι κ} (Δ₄ : 𝑜𝑏₃ 𝑓₃ 𝑓₆ 𝑓₈ 𝑓₁₀)
      (Δ₅ : 𝑜𝑏₃ 𝑓₄ 𝑓₇ 𝑓₉ 𝑓₁₀) → 𝑜𝑏₃ 𝑓₂ 𝑓₅ 𝑓₈ 𝑓₉
    𝑜𝑏₃-𝑓𝑖𝑙𝑙ʷ : {x y z w v : 𝑜𝑏₀} {α : 𝑜𝑏₁ x y} {β : 𝑜𝑏₁ x z} {γ : 𝑜𝑏₁ y z}
      {𝑓₁ : 𝑜𝑏₂ α β γ} {δ : 𝑜𝑏₁ x w} {ε : 𝑜𝑏₁ y w} {𝑓₂ : 𝑜𝑏₂ α δ ε}
      {ζ : 𝑜𝑏₁ z w} {𝑓₃ : 𝑜𝑏₂ β δ ζ} {𝑓₄ : 𝑜𝑏₂ γ ε ζ}
      (Δ₁ : 𝑜𝑏₃ 𝑓₁ 𝑓₂ 𝑓₃ 𝑓₄) {η : 𝑜𝑏₁ x v} {θ : 𝑜𝑏₁ y v} {𝑓₅ : 𝑜𝑏₂ α η θ}
      {ι : 𝑜𝑏₁ z v} {𝑓₆ : 𝑜𝑏₂ β η ι} {𝑓₇ : 𝑜𝑏₂ γ θ ι}
      {κ : 𝑜𝑏₁ w v} {𝑓₈ : 𝑜𝑏₂ δ η κ} {𝑓₉ : 𝑜𝑏₂ ε θ κ}
      (Δ₃ : 𝑜𝑏₃ 𝑓₂ 𝑓₅ 𝑓₈ 𝑓₉) {𝑓₁₀ : 𝑜𝑏₂ ζ ι κ} (Δ₄ : 𝑜𝑏₃ 𝑓₃ 𝑓₆ 𝑓₈ 𝑓₁₀)
      (Δ₅ : 𝑜𝑏₃ 𝑓₄ 𝑓₇ 𝑓₉ 𝑓₁₀) → 𝑜𝑏₃ 𝑓₁ 𝑓₅ 𝑓₆ 𝑓₇

    _◾₁_ : {x y z : 𝑜𝑏₀} → 𝑜𝑏₁ x y → 𝑜𝑏₁ y z → 𝑜𝑏₁ x z
    𝑓𝑖𝑙𝑙₁ : {x y z : 𝑜𝑏₀} (α : 𝑜𝑏₁ x y) (β : 𝑜𝑏₁ y z) → 𝑜𝑏₂ α (α ◾₁ β) β

    _◾₂ˣ_ : {x y z w : 𝑜𝑏₀} {α : 𝑜𝑏₁ x y} {β : 𝑜𝑏₁ x z}
      {γ : 𝑜𝑏₁ y z} {δ : 𝑜𝑏₁ x w} {ε : 𝑜𝑏₁ z w} →
      𝑜𝑏₂ α β γ → 𝑜𝑏₂ β δ ε → 𝑜𝑏₂ α δ (γ ◾₁ ε)
    _◾₂ᶻ_ : {x y z w : 𝑜𝑏₀} {α : 𝑜𝑏₁ x y} {β : 𝑜𝑏₁ y z}
      {γ : 𝑜𝑏₁ x w} {δ : 𝑜𝑏₁ y w} {ε : 𝑜𝑏₁ z w} →
      𝑜𝑏₂ β δ ε → 𝑜𝑏₂ α γ δ → 𝑜𝑏₂ (α ◾₁ β) γ ε
    𝑓𝑖𝑙𝑙₂ˣ : {x y z w : 𝑜𝑏₀} {α : 𝑜𝑏₁ x y} {β : 𝑜𝑏₁ x z}
      {γ : 𝑜𝑏₁ y z} {δ : 𝑜𝑏₁ x w} {ε : 𝑜𝑏₁ z w}
      (𝑓 : 𝑜𝑏₂ α β γ) (𝑔 : 𝑜𝑏₂ β δ ε) → 𝑜𝑏₃ 𝑓 (𝑓 ◾₂ˣ 𝑔) 𝑔 (𝑓𝑖𝑙𝑙₁ γ ε)
    𝑓𝑖𝑙𝑙₂ᶻ : {x y z w : 𝑜𝑏₀} {α : 𝑜𝑏₁ x y} {β : 𝑜𝑏₁ y z}
      {γ : 𝑜𝑏₁ x w} {δ : 𝑜𝑏₁ y w} {ε : 𝑜𝑏₁ z w}
      (𝑓 : 𝑜𝑏₂ β δ ε) (𝑔 : 𝑜𝑏₂ α γ δ) → 𝑜𝑏₃ (𝑓𝑖𝑙𝑙₁ α β) 𝑔 (𝑓 ◾₂ᶻ 𝑔) 𝑓
    
    σ₀ : (x : 𝑜𝑏₀) → 𝑜𝑏₁ x x
    σ₁ˣ : {x y : 𝑜𝑏₀} (α : 𝑜𝑏₁ x y) → 𝑜𝑏₂ α α (σ₀ y)
    σ₁ᶻ : {x y : 𝑜𝑏₀} (α : 𝑜𝑏₁ x y) → 𝑜𝑏₂ (σ₀ x) α α
    σ₂α : {x y z : 𝑜𝑏₀} {α : 𝑜𝑏₁ x y} {β : 𝑜𝑏₁ x z} {γ : 𝑜𝑏₁ y z}
      (𝑓 : 𝑜𝑏₂ α β γ) → 𝑜𝑏₃ 𝑓 𝑓 (σ₁ˣ β) (σ₁ˣ γ)
    σ₂δ : {x y z : 𝑜𝑏₀} {α : 𝑜𝑏₁ x y} {β : 𝑜𝑏₁ x z} {γ : 𝑜𝑏₁ y z}
      (𝑓 : 𝑜𝑏₂ α β γ) → 𝑜𝑏₃ (σ₁ˣ α) 𝑓 𝑓 (σ₁ᶻ γ)
    σ₂ζ : {x y z : 𝑜𝑏₀} {α : 𝑜𝑏₁ x y} {β : 𝑜𝑏₁ x z} {γ : 𝑜𝑏₁ y z}
      (𝑓 : 𝑜𝑏₂ α β γ) → 𝑜𝑏₃ (σ₁ᶻ α) (σ₁ᶻ β) 𝑓 𝑓