weak and strict 1-categories

weak-cat.agda

{-# OPTIONS --cubical #-}

module weak-cat 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

-- 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 (𝑜𝑏₂ α β γ)

    -- horn filling says that 𝑜𝑏₂ behavess like equality
    -- inner horn comp
    𝑜𝑏₂-𝑓𝑖𝑙𝑙ʸ : {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} (𝑓₃ : 𝑜𝑏₂ β δ ζ) (𝑓₄ : 𝑜𝑏₂ γ ε ζ) → 𝑜𝑏₂ α δ ε

    -- outer horn comp [not sure if needed?]
    𝑜𝑏₂-𝑓𝑖𝑙𝑙ˣ : {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) α α

  𝑎𝑠𝑠𝑜𝑐¹ : {x y z w : 𝑜𝑏₀} (α : 𝑜𝑏₁ x y) (β : 𝑜𝑏₁ y z) (γ : 𝑜𝑏₁ z w) →
    𝑜𝑏₂ (α ◾ β) (α ◾ (β ◾ γ)) γ
  𝑎𝑠𝑠𝑜𝑐¹ α β γ = 𝑜𝑏₂-𝑓𝑖𝑙𝑙ʸ (𝑓𝑖𝑙𝑙 α β) (𝑓𝑖𝑙𝑙 α (β ◾ γ)) (𝑓𝑖𝑙𝑙 β γ)

  𝑎𝑠𝑠𝑜𝑐² : {x y z w : 𝑜𝑏₀} (α : 𝑜𝑏₁ x y) (β : 𝑜𝑏₁ y z) (γ : 𝑜𝑏₁ z w) →
    𝑜𝑏₂ α ((α ◾ β) ◾ γ) (β ◾ γ)
  𝑎𝑠𝑠𝑜𝑐² α β γ = 𝑜𝑏₂-𝑓𝑖𝑙𝑙ᶻ (𝑓𝑖𝑙𝑙 α β) (𝑓𝑖𝑙𝑙 (α ◾ β) γ) (𝑓𝑖𝑙𝑙 β γ)

  𝑖𝑠𝑜 : {x y : 𝑜𝑏₀} → 𝑜𝑏₁ x y → Type (ℓ₂ ⊔ ℓ₃)
  𝑖𝑠𝑜 {x} {y} α = Σ (𝑜𝑏₁ y x) (λ β → 𝑜𝑏₂ α (𝑖𝑑 x) β × 𝑜𝑏₂ β (𝑖𝑑 y) α)

  𝑐𝑜𝑚𝑝-𝑖𝑠𝑜 : {x y z : 𝑜𝑏₀} {α : 𝑜𝑏₁ x y} {β : 𝑜𝑏₁ y z} {γ : 𝑜𝑏₁ x z} →
    𝑜𝑏₂ α γ β → 𝑖𝑠𝑜 α → 𝑖𝑠𝑜 β → 𝑖𝑠𝑜 γ
  𝑐𝑜𝑚𝑝-𝑖𝑠𝑜 𝑓 p q =
    fst q ◾ fst p ,
    𝑜𝑏₂-𝑓𝑖𝑙𝑙ʸ 𝑓 (fst (snd p))
      (𝑜𝑏₂-𝑓𝑖𝑙𝑙ᶻ (fst (snd q)) (σ₂ (fst p)) (𝑓𝑖𝑙𝑙 (fst q) (fst p))) ,
    𝑜𝑏₂-𝑓𝑖𝑙𝑙ᶻ (𝑜𝑏₂-𝑓𝑖𝑙𝑙ʸ (𝑓𝑖𝑙𝑙 (fst q) (fst p)) (σ₁ (fst q)) (snd (snd p)))
      (snd (snd q)) 𝑓

  𝑖𝑑-𝑖𝑠𝑜 : (x : 𝑜𝑏₀) → 𝑖𝑠𝑜 (𝑖𝑑 x)
  𝑖𝑑-𝑖𝑠𝑜 x = 𝑖𝑑 x , σ₁ (𝑖𝑑 x) , σ₂ (𝑖𝑑 x)

  ◾-𝑖𝑠𝑜 : {x y z : 𝑜𝑏₀} {α : 𝑜𝑏₁ x y} {β : 𝑜𝑏₁ y z} → 𝑖𝑠𝑜 α → 𝑖𝑠𝑜 β → 𝑖𝑠𝑜 (α ◾ β)
  ◾-𝑖𝑠𝑜 {α = α} {β} p q = 𝑐𝑜𝑚𝑝-𝑖𝑠𝑜 (𝑓𝑖𝑙𝑙 α β) p q

-- Strict 1-Category
record Cat ℓ₁ ℓ₂ : Type (lsuc (ℓ₁ ⊔ ℓ₂)) where
  field
    𝑜𝑏 : Type ℓ₁
    𝑚𝑜𝑟 : 𝑜𝑏 → 𝑜𝑏 → Type ℓ₂
    𝑐𝑜𝑚𝑝 : {x y z : 𝑜𝑏} → 𝑚𝑜𝑟 x y → 𝑚𝑜𝑟 y z → 𝑚𝑜𝑟 x z
    𝑎𝑠𝑠𝑜𝑐 : {x y z w : 𝑜𝑏} (α : 𝑚𝑜𝑟 x y) (β : 𝑚𝑜𝑟 y z) (γ : 𝑚𝑜𝑟 z w) →
      𝑐𝑜𝑚𝑝 (𝑐𝑜𝑚𝑝 α β) γ ≡ 𝑐𝑜𝑚𝑝 α (𝑐𝑜𝑚𝑝 β γ)
    𝑖𝑑 : (x : 𝑜𝑏) → 𝑚𝑜𝑟 x x
    𝑖𝑑-L : {x y : 𝑜𝑏} (α : 𝑚𝑜𝑟 x y) → 𝑐𝑜𝑚𝑝 (𝑖𝑑 x) α ≡ α
    𝑖𝑑-R : {x y : 𝑜𝑏} (α : 𝑚𝑜𝑟 x y) → 𝑐𝑜𝑚𝑝 α (𝑖𝑑 y) ≡ α

-- Strictification
module _ (𝒞 : WeakCat ℓ₁ ℓ₂ ℓ₃) where
  open WeakCat 𝒞

  data RezkMor : (x y : 𝑜𝑏₀) → Type (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃) where
    R₀ : {x y : 𝑜𝑏₀} → 𝑜𝑏₁ x y → RezkMor x y
    R₁ : {x y z : 𝑜𝑏₀} {α : 𝑜𝑏₁ x y} {β : 𝑜𝑏₁ y z} {γ : 𝑜𝑏₁ x z}
      (𝑓 : 𝑜𝑏₂ α γ β) → R₀ (α ◾ β) ≡ R₀ γ
    R-trunc : {x y : 𝑜𝑏₀} → isSet (RezkMor x y)

  compR : {x y z : 𝑜𝑏₀} → RezkMor x y → RezkMor y z → RezkMor x z  
  compR (R₀ α) (R₀ β) = R₀ (α ◾ β)
  compR (R₀ α) (R₁ {α = β} {γ} {δ} 𝑔 i) =
    R₁ (𝑜𝑏₂-𝑓𝑖𝑙𝑙ᶻ (𝑓𝑖𝑙𝑙 α β) (𝑜𝑏₂-𝑓𝑖𝑙𝑙ʸ (𝑓𝑖𝑙𝑙 α β) (𝑓𝑖𝑙𝑙 α δ) 𝑔) (𝑓𝑖𝑙𝑙 β γ)) i
  compR (R₀ α) (R-trunc β γ p q i j) =
    R-trunc (compR (R₀ α) β) (compR (R₀ α) γ)
      (λ k → compR (R₀ α) (p k)) (λ k → compR (R₀ α) (q k)) i j
  compR (R₁ {α = α} {β} {γ} 𝑓 i) (R₀ δ) =
    R₁ (𝑜𝑏₂-𝑓𝑖𝑙𝑙ʸ (𝑓𝑖𝑙𝑙 α β) (𝑜𝑏₂-𝑓𝑖𝑙𝑙ᶻ 𝑓 (𝑓𝑖𝑙𝑙 γ δ) (𝑓𝑖𝑙𝑙 β δ)) (𝑓𝑖𝑙𝑙 β δ)) i
  compR (R₁ {α = α} {β} {γ} 𝑓 i) (R₁ {α = δ} {ε} {ζ} 𝑔 j) =
    isSet→SquareP
      (λ i j → R-trunc)
      (λ k → compR (R₀ (α ◾ β)) (R₁ 𝑔 k))
      (λ k → compR (R₀ γ) (R₁ 𝑔 k))
      (λ k → compR (R₁ 𝑓 k) (R₀ (δ ◾ ε)))
      (λ k → compR (R₁ 𝑓 k) (R₀ ζ)) i j
  compR (R₁ 𝑓 i) (R-trunc α β p q j k) =
    R-trunc (compR (R₁ 𝑓 i) α) (compR (R₁ 𝑓 i) β)
      (λ k → compR (R₁ 𝑓 i) (p k)) (λ k → compR (R₁ 𝑓 i) (q k)) j k
  compR (R-trunc α β p q i j) γ =
    R-trunc (compR α γ) (compR β γ)
      (λ k → compR (p k) γ) (λ k → compR (q k) γ) i j

  -- termination justified by Astra's theory of CW-HITs
  -- can be avoided by doing a further case split
  {-# TERMINATING #-}
  assocR : {x y z w : 𝑜𝑏₀} (α : RezkMor x y) (β : RezkMor y z) (γ : RezkMor z w) →
    compR (compR α β) γ ≡ compR α (compR β γ)
  assocR (R₀ α) (R₀ β) (R₀ γ) = R₁ (𝑎𝑠𝑠𝑜𝑐¹ α β γ)
  assocR (R₀ α) (R₀ β) (R₁ {α = γ} {δ} {ε} 𝑓 j) =
    isSet→SquareP
      (λ i j → R-trunc)
      (R₁ (𝑎𝑠𝑠𝑜𝑐¹ α β (γ ◾ δ)))
      (R₁ (𝑎𝑠𝑠𝑜𝑐¹ α β ε))
      (λ k → compR (compR (R₀ α) (R₀ β)) (R₁ 𝑓 k))
      (λ k → compR (R₀ α) (compR (R₀ β) (R₁ 𝑓 k))) j
  assocR (R₀ α) (R₀ β) (R-trunc γ δ p q j k) i =
    R-trunc _ _ (λ l → assocR (R₀ α) (R₀ β) (p l) i) (λ l → assocR (R₀ α) (R₀ β) (q l) i) j k
  assocR (R₀ α) (R₁ {α = β} {γ} {δ} 𝑓 j) ε i =
    isSet→SquareP
      (λ i j → R-trunc)
      (assocR (R₀ α) (R₀ (β ◾ γ)) ε)
      (assocR (R₀ α) (R₀ δ) ε)
      (λ k → compR (compR (R₀ α) (R₁ 𝑓 k)) ε)
      (λ k → compR (R₀ α) (compR (R₁ 𝑓 k) ε)) j i
  assocR (R₀ α) (R-trunc β γ p q j k) δ i =
    R-trunc _ _ (λ l → assocR (R₀ α) (p l) δ i) (λ l → assocR (R₀ α) (q l) δ i) j k
  assocR (R₁ {α = α} {β} {γ} 𝑓 j) δ ε =
    isSet→SquareP
      (λ i j → R-trunc)
      (assocR (R₀ (α ◾ β)) δ ε)
      (assocR (R₀ γ) δ ε )
      (λ k → compR (compR (R₁ 𝑓 k) δ) ε)
      (λ k → compR (R₁ 𝑓 k) (compR δ ε)) j
  assocR (R-trunc α β p q j k) γ δ i =
    R-trunc _ _ (λ l → assocR (p l) γ δ i) (λ l → assocR (q l) γ δ i) j k

  completion : Cat ℓ₁ (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)
  Cat.𝑜𝑏 completion = 𝑜𝑏₀
  Cat.𝑚𝑜𝑟 completion x y = RezkMor x y
  Cat.𝑐𝑜𝑚𝑝 completion α β = compR α β
  Cat.𝑎𝑠𝑠𝑜𝑐 completion α β γ = assocR α β γ
  Cat.𝑖𝑑 completion x = R₀ (𝑖𝑑 x)
  Cat.𝑖𝑑-L completion = {!!}
  Cat.𝑖𝑑-R completion = {!!}

  -- Rezk completion on objects [not used]
  data RezkOb : Type (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃) where
    R₀ : 𝑜𝑏₀ → RezkOb
    R₁ : {x y : 𝑜𝑏₀} {α : 𝑜𝑏₁ x y} → 𝑖𝑠𝑜 α → R₀ x ≡ R₀ y
    R₂ : {x y z : 𝑜𝑏₀} {α : 𝑜𝑏₁ x y} {β : 𝑜𝑏₁ y z} {γ : 𝑜𝑏₁ x z}
      (𝑓 : 𝑜𝑏₂ α γ β) (p : 𝑖𝑠𝑜 α) (q : 𝑖𝑠𝑜 β) →
      R₁ p ∙ R₁ q ≡ R₁ (𝑐𝑜𝑚𝑝-𝑖𝑠𝑜 𝑓 p q)
    R-trunc : isGroupoid RezkOb