Weak 1-Categories

1cat.agda

{-# OPTIONS --cubical #-}

module 1cat where

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

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

-- Weak 1-Category
record WeakCat ℓ₁ ℓ₂ ℓ₃ : Type (lsuc (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where
  infixl 20 _◾_
  field
    𝑜𝑏₀ : Type ℓ₁
    𝑜𝑏₁ : 𝑜𝑏₀ → 𝑜𝑏₀ → Type ℓ₂
    𝑜𝑏₂ : {x y z : 𝑜𝑏₀} → 𝑜𝑏₁ x y → 𝑜𝑏₁ x z → 𝑜𝑏₁ y z → Type ℓ₃
    isProp-𝑜𝑏₂ : {x y z : 𝑜𝑏₀} (α : 𝑜𝑏₁ x y) (β : 𝑜𝑏₁ x z)
      (γ : 𝑜𝑏₁ y z) → isProp (𝑜𝑏₂ α β γ)

    -- inner horn filling says that 𝑜𝑏₂ behavess like equality
    𝑜𝑏₂-𝑓𝑖𝑙𝑙ʸ : {x y z w : 𝑜𝑏₀} {α : 𝑜𝑏₁ x y} {β : 𝑜𝑏₁ x z} {γ : 𝑜𝑏₁ y z}
      (𝑓₁ : 𝑜𝑏₂ α β γ) {δ : 𝑜𝑏₁ x w} {ε : 𝑜𝑏₁ y w} (𝑓₂ : 𝑜𝑏₂ α δ ε)
      {ζ : 𝑜𝑏₁ z w} (𝑓₄ : 𝑜𝑏₂ γ ε ζ) → 𝑜𝑏₂ β δ ζ
    𝑜𝑏₂-𝑓𝑖𝑙𝑙ᶻ : {x y z w : 𝑜𝑏₀} {α : 𝑜𝑏₁ x y} {β : 𝑜𝑏₁ x z} {γ : 𝑜𝑏₁ y z}
      (𝑓₁ : 𝑜𝑏₂ α β γ) {δ : 𝑜𝑏₁ x w} {ε : 𝑜𝑏₁ y w}
      {ζ : 𝑜𝑏₁ z w} (𝑓₃ : 𝑜𝑏₂ β δ ζ) (𝑓₄ : 𝑜𝑏₂ γ ε ζ) → 𝑜𝑏₂ α δ ε
      
    _◾_ : {x y z : 𝑜𝑏₀} → 𝑜𝑏₁ x y → 𝑜𝑏₁ y z → 𝑜𝑏₁ x z
    𝑓𝑖𝑙𝑙 : {x y z : 𝑜𝑏₀} (α : 𝑜𝑏₁ x y) (β : 𝑜𝑏₁ y z) → 𝑜𝑏₂ α (α ◾ β) β
    𝑖𝑑 : (x : 𝑜𝑏₀) → 𝑜𝑏₁ x x
    σ₁ : {x y : 𝑜𝑏₀} (α : 𝑜𝑏₁ x y) → 𝑜𝑏₂ α α (𝑖𝑑 y)
    σ₂ : {x y : 𝑜𝑏₀} (α : 𝑜𝑏₁ x y) → 𝑜𝑏₂ (𝑖𝑑 x) α α