Skip to content

Instantly share code, notes, and snippets.

@FrozenWinters

FrozenWinters/CwF.agda

Last active February 20, 2024 00:20
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save FrozenWinters/1d40f0faefcafb3882f7af5e9980dd9a to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save FrozenWinters/1d40f0faefcafb3882f7af5e9980dd9a to your computer and use it in GitHub Desktop.
Download ZIP
Categories with Families
Raw
CwF.agda
{-# OPTIONS --cubical #-}
module CwF where
open import Agda.Primitive using (Level; lzero; lsuc; _βŠ”_) public
open import Cubical.Core.Everything public
open import Cubical.Foundations.Everything renaming (cong to ap) public
-- Category with Families (4.1.1)
record Category : Type₁ where
field
𝐢𝑑π‘₯ : Type
𝑆𝑒𝑏 : 𝐢𝑑π‘₯ β†’ 𝐢𝑑π‘₯ β†’ Type
𝑖𝑑 : {Ξ“ : 𝐢𝑑π‘₯} β†’ 𝑆𝑒𝑏 Ξ“ Ξ“
π‘π‘œπ‘šπ‘ : {Ξ£ Ξ” Ξ“ : 𝐢𝑑π‘₯} β†’ 𝑆𝑒𝑏 Ξ” Ξ“ β†’ 𝑆𝑒𝑏 Ξ£ Ξ” β†’ 𝑆𝑒𝑏 Ξ£ Ξ“
𝑖𝑑-L : {Ξ” Ξ“ : 𝐢𝑑π‘₯} (Οƒ : 𝑆𝑒𝑏 Ξ” Ξ“) β†’ π‘π‘œπ‘šπ‘ 𝑖𝑑 Οƒ ≑ Οƒ
𝑖𝑑-R : {Ξ” Ξ“ : 𝐢𝑑π‘₯} (Οƒ : 𝑆𝑒𝑏 Ξ” Ξ“) β†’ π‘π‘œπ‘šπ‘ Οƒ 𝑖𝑑 ≑ Οƒ
π‘Žπ‘ π‘ π‘œπ‘ : {Ξ© Ξ£ Ξ” Ξ“ : 𝐢𝑑π‘₯} (Οƒ : 𝑆𝑒𝑏 Ξ” Ξ“) (Ο„ : 𝑆𝑒𝑏 Ξ£ Ξ”) (ΞΌ : 𝑆𝑒𝑏 Ξ© Ξ£) β†’ π‘π‘œπ‘šπ‘ Οƒ (π‘π‘œπ‘šπ‘ Ο„ ΞΌ) ≑ π‘π‘œπ‘šπ‘ (π‘π‘œπ‘šπ‘ Οƒ Ο„) ΞΌ
isSet-𝐢𝑑π‘₯ : isSet 𝐢𝑑π‘₯
isSet-𝑆𝑒𝑏 : {Ξ” Ξ“ : 𝐢𝑑π‘₯} β†’ isSet (𝑆𝑒𝑏 Ξ” Ξ“)
record Fibrant (π’ž : Category) : Type₁ where
open Category π’ž
field
𝑇𝑦 : (Ξ“ : 𝐢𝑑π‘₯) β†’ Type
𝑓𝑒𝑛-𝑇𝑦 : {Ξ” Ξ“ : 𝐢𝑑π‘₯} (Οƒ : 𝑆𝑒𝑏 Ξ” Ξ“) β†’ 𝑇𝑦 Ξ“ β†’ 𝑇𝑦 Ξ”
𝑖𝑑-𝑓𝑒𝑛-𝑇𝑦 : {Ξ“ : 𝐢𝑑π‘₯} (A : 𝑇𝑦 Ξ“) β†’ 𝑓𝑒𝑛-𝑇𝑦 (𝑖𝑑) A ≑ A
π‘π‘œπ‘šπ‘-𝑓𝑒𝑛-𝑇𝑦 : {Ξ£ Ξ” Ξ“ : 𝐢𝑑π‘₯} (Οƒ : 𝑆𝑒𝑏 Ξ£ Ξ”) (Ο„ : 𝑆𝑒𝑏 Ξ” Ξ“) (A : 𝑇𝑦 Ξ“) β†’ 𝑓𝑒𝑛-𝑇𝑦 Οƒ (𝑓𝑒𝑛-𝑇𝑦 Ο„ A) ≑ 𝑓𝑒𝑛-𝑇𝑦 (π‘π‘œπ‘šπ‘ Ο„ Οƒ) A
π‘‡π‘š : (Ξ“ : 𝐢𝑑π‘₯) (A : 𝑇𝑦 Ξ“) β†’ Type
𝑓𝑒𝑛-π‘‡π‘š : {Ξ” Ξ“ : 𝐢𝑑π‘₯} (Οƒ : 𝑆𝑒𝑏 Ξ” Ξ“) {A : 𝑇𝑦 Ξ“} (t : π‘‡π‘š Ξ“ A) β†’ π‘‡π‘š Ξ” (𝑓𝑒𝑛-𝑇𝑦 Οƒ A)
𝑖𝑑-𝑓𝑒𝑛-π‘‡π‘š : {Ξ“ : 𝐢𝑑π‘₯} {A : 𝑇𝑦 Ξ“} (t : π‘‡π‘š Ξ“ A) β†’ PathP (Ξ» i β†’ π‘‡π‘š Ξ“ (𝑖𝑑-𝑓𝑒𝑛-𝑇𝑦 A i)) (𝑓𝑒𝑛-π‘‡π‘š (𝑖𝑑) t) t
π‘π‘œπ‘šπ‘-𝑓𝑒𝑛-π‘‡π‘š : {Ξ£ Ξ” Ξ“ : 𝐢𝑑π‘₯} (Οƒ : 𝑆𝑒𝑏 Ξ£ Ξ”) (Ο„ : 𝑆𝑒𝑏 Ξ” Ξ“) {A : 𝑇𝑦 Ξ“} (t : π‘‡π‘š Ξ“ A) β†’
PathP (Ξ» i β†’ π‘‡π‘š Ξ£ (π‘π‘œπ‘šπ‘-𝑓𝑒𝑛-𝑇𝑦 Οƒ Ο„ A i)) (𝑓𝑒𝑛-π‘‡π‘š Οƒ (𝑓𝑒𝑛-π‘‡π‘š Ο„ t)) (𝑓𝑒𝑛-π‘‡π‘š (π‘π‘œπ‘šπ‘ Ο„ Οƒ) t)
𝑒π‘₯-𝑇𝑦 : (Ξ“ : 𝐢𝑑π‘₯) (A : 𝑇𝑦 Ξ“) β†’ 𝐢𝑑π‘₯
𝑝𝑑 : (Ξ“ : 𝐢𝑑π‘₯) (A : 𝑇𝑦 Ξ“) β†’ 𝑆𝑒𝑏 (𝑒π‘₯-𝑇𝑦 Ξ“ A) Ξ“
𝑧𝑣 : (Ξ“ : 𝐢𝑑π‘₯) (A : 𝑇𝑦 Ξ“) β†’ π‘‡π‘š (𝑒π‘₯-𝑇𝑦 Ξ“ A) (𝑓𝑒𝑛-𝑇𝑦 (𝑝𝑑 Ξ“ A) A)
𝑒π‘₯-π‘‡π‘š : {Ξ” Ξ“ : 𝐢𝑑π‘₯} {A : 𝑇𝑦 Ξ“} (Οƒ : 𝑆𝑒𝑏 Ξ” Ξ“) (t : π‘‡π‘š Ξ” (𝑓𝑒𝑛-𝑇𝑦 Οƒ A)) β†’ 𝑆𝑒𝑏 Ξ” (𝑒π‘₯-𝑇𝑦 Ξ“ A)
π‘™π‘Žπ‘€β‚ : {Ξ” Ξ“ : 𝐢𝑑π‘₯} (Οƒ : 𝑆𝑒𝑏 Ξ” Ξ“) {A : 𝑇𝑦 Ξ“} (t : π‘‡π‘š Ξ” (𝑓𝑒𝑛-𝑇𝑦 Οƒ A)) β†’ π‘π‘œπ‘šπ‘ (𝑝𝑑 Ξ“ A) (𝑒π‘₯-π‘‡π‘š Οƒ t) ≑ Οƒ
π‘™π‘Žπ‘€β‚‚ : {Ξ” Ξ“ : 𝐢𝑑π‘₯} (Οƒ : 𝑆𝑒𝑏 Ξ” Ξ“) {A : 𝑇𝑦 Ξ“} (t : π‘‡π‘š Ξ” (𝑓𝑒𝑛-𝑇𝑦 Οƒ A)) β†’
PathP (Ξ» i β†’ (ap (Ξ» B β†’ π‘‡π‘š Ξ” B) (π‘π‘œπ‘šπ‘-𝑓𝑒𝑛-𝑇𝑦 (𝑒π‘₯-π‘‡π‘š Οƒ t) (𝑝𝑑 Ξ“ A) A) βˆ™ ap (Ξ» Ο„ β†’ π‘‡π‘š Ξ” (𝑓𝑒𝑛-𝑇𝑦 Ο„ A)) (π‘™π‘Žπ‘€β‚ Οƒ t)) i)
(𝑓𝑒𝑛-π‘‡π‘š (𝑒π‘₯-π‘‡π‘š Οƒ t) (𝑧𝑣 Ξ“ A)) t
π‘™π‘Žπ‘€β‚ƒ : {Ξ” Ξ“ : 𝐢𝑑π‘₯} {A : 𝑇𝑦 Ξ“} (Οƒ : 𝑆𝑒𝑏 Ξ” (𝑒π‘₯-𝑇𝑦 Ξ“ A)) β†’
𝑒π‘₯-π‘‡π‘š (π‘π‘œπ‘šπ‘ (𝑝𝑑 Ξ“ A) Οƒ) (subst (π‘‡π‘š Ξ”) (π‘π‘œπ‘šπ‘-𝑓𝑒𝑛-𝑇𝑦 Οƒ (𝑝𝑑 Ξ“ A) A) (𝑓𝑒𝑛-π‘‡π‘š Οƒ (𝑧𝑣 Ξ“ A))) ≑ Οƒ
isSet-𝑇𝑦 : {Ξ“ : 𝐢𝑑π‘₯} β†’ isSet (𝑇𝑦 Ξ“)
isSet-π‘‡π‘š : {Ξ“ : 𝐢𝑑π‘₯} {A : 𝑇𝑦 Ξ“} β†’ isSet (π‘‡π‘š Ξ“ A)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment