Compare commits

...

3 Commits

Author SHA1 Message Date
Nathan van Doorn 19d2e98ef0 Define initial object structure 2024-06-20 10:25:38 +02:00
Nathan van Doorn a0a743ac71 Show that it's unique 2024-06-20 09:31:14 +02:00
Nathan van Doorn 19141b121b Add thinning from empty list 2024-06-20 09:29:49 +02:00
3 changed files with 26 additions and 2 deletions

View File

@ -4,12 +4,19 @@ module Categories.Category.Instance.Thinnings where
open import Categories.Category.Core open import Categories.Category.Core
open import Categories.Category.Helper open import Categories.Category.Helper
open import Data.List.Base using (List) open import Categories.Object.Initial
open import Data.List.Base using (List; [])
open import Level using (Level)
open import Relation.Binary.PropositionalEquality open import Relation.Binary.PropositionalEquality
open import Thinning open import Thinning
open import Thinning.Properties open import Thinning.Properties
private
variable
a : Level
A : Set a
Thinnings : {a} (A : Set a) Category a a a Thinnings : {a} (A : Set a) Category a a a
Thinnings A = categoryHelper record Thinnings A = categoryHelper record
{ Obj = List A { Obj = List A
@ -23,3 +30,9 @@ Thinnings A = categoryHelper record
; equiv = isEquivalence ; equiv = isEquivalence
; ∘-resp-≈ = cong₂ _∘_ ; ∘-resp-≈ = cong₂ _∘_
} }
[]-isInitial : IsInitial (Thinnings A) []
[]-isInitial = record { !-unique = ¡-unique }
initial : Initial (Thinnings A)
initial = record { ⊥-is-initial = []-isInitial }

View File

@ -45,3 +45,9 @@ end ∘ end = end
include α include β = include (α β) include α include β = include (α β)
include α exclude β = exclude (α β) include α exclude β = exclude (α β)
exclude α β = exclude (α β) exclude α β = exclude (α β)
-- There is always a Thinning from the empty list to any list. Here we exclude
-- at every step.
¡ : Thinning A [] xs
¡ {xs = []} = end
¡ {xs = x xs} = exclude ¡

View File

@ -2,7 +2,7 @@
module Thinning.Properties where module Thinning.Properties where
open import Data.List.Base using (List) open import Data.List.Base using (List; [])
open import Level using (Level) open import Level using (Level)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
@ -48,3 +48,8 @@ assoc (exclude θ) (include φ) (include ψ) = cong exclude (assoc θ φ ψ)
assoc (exclude θ) (include φ) (exclude ψ) = cong exclude (assoc (exclude θ) (include φ) ψ) assoc (exclude θ) (include φ) (exclude ψ) = cong exclude (assoc (exclude θ) (include φ) ψ)
assoc (exclude θ) (exclude φ) (include ψ) = cong exclude (assoc (exclude θ) φ ψ) assoc (exclude θ) (exclude φ) (include ψ) = cong exclude (assoc (exclude θ) φ ψ)
assoc (exclude θ) (exclude φ) (exclude ψ) = cong exclude (assoc (exclude θ) (exclude φ) ψ) assoc (exclude θ) (exclude φ) (exclude ψ) = cong exclude (assoc (exclude θ) (exclude φ) ψ)
-- ¡ is the only Thinning from []
¡-unique : (θ : Thinning A [] xs) ¡ θ
¡-unique end = refl
¡-unique (exclude θ) = cong exclude (¡-unique θ)