Last active
March 13, 2023 21:29
-
-
Save FrozenWinters/1c708573c995486cff11c997aa9cb427 to your computer and use it in GitHub Desktop.
weak and strict 1-categories
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# 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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment