mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
✨ Show that Setoids is an instance of our ambient category
This commit is contained in:
parent
a0ba49ff2e
commit
1a4b9135fc
SSH key fingerprint:
SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
2 changed files with 117 additions and 10 deletions
|
|
@ -1,3 +1,111 @@
|
|||
<!--
|
||||
```agda
|
||||
module Category.Ambient.Setoid where
|
||||
```
|
||||
open import Level using (lift; Lift) renaming (suc to ℓ-suc)
|
||||
open import Category.Ambient
|
||||
open import Categories.Category.Instance.Setoids
|
||||
open import Categories.Category.Instance.Properties.Setoids.Extensive
|
||||
open import Categories.Category.Instance.Properties.Setoids.CCC
|
||||
open import Categories.Category.Monoidal.Instance.Setoids
|
||||
open import Categories.Category.Instance.SingletonSet
|
||||
open import Categories.Object.NaturalNumbers
|
||||
open import Relation.Binary
|
||||
open import Data.Unit.Polymorphic using (tt; ⊤)
|
||||
open import Data.Empty.Polymorphic using (⊥)
|
||||
open import Function.Equality as SΠ renaming (id to idₛ)
|
||||
open import Categories.Object.NaturalNumbers.Properties.Parametrized
|
||||
open import Categories.Category.Cocartesian
|
||||
import Relation.Binary.Reasoning.Setoid as SetoidR
|
||||
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_)
|
||||
```
|
||||
-->
|
||||
|
||||
# The category of Setoids can be used as instance for ambient category
|
||||
|
||||
Most of the required properties are already proven in the agda-categories library, we are only left to construct the natural numbers object.
|
||||
|
||||
```agda
|
||||
module Category.Ambient.Setoid {ℓ} where
|
||||
-- equality on setoid functions
|
||||
_≋_ : ∀ {A B : Setoid ℓ ℓ} → A ⟶ B → A ⟶ B → Set ℓ
|
||||
_≋_ {A} {B} f g = Setoid._≈_ (A ⇨ B) f g
|
||||
≋-sym : ∀ {A B : Setoid ℓ ℓ} {f g : A ⟶ B} → f ≋ g → g ≋ f
|
||||
≋-sym {A} {B} {f} {g} = IsEquivalence.sym (Setoid.isEquivalence (A ⇨ B)) {f} {g}
|
||||
≋-trans : ∀ {A B : Setoid ℓ ℓ} {f g h : A ⟶ B} → f ≋ g → g ≋ h → f ≋ h
|
||||
≋-trans {A} {B} {f} {g} {h} = IsEquivalence.trans (Setoid.isEquivalence (A ⇨ B)) {f} {g} {h}
|
||||
|
||||
-- we define ℕ ourselves, instead of importing it, to avoid lifting the universe lifting (builtin Nats are defined on Set₀)
|
||||
data ℕ : Set ℓ where
|
||||
zero : ℕ
|
||||
suc : ℕ → ℕ
|
||||
|
||||
suc-cong : ∀ {n m} → n ≡ m → suc n ≡ suc m
|
||||
suc-cong n≡m rewrite n≡m = Eq.refl
|
||||
|
||||
suc-inj : ∀ {n m} → suc n ≡ suc m → n ≡ m
|
||||
suc-inj Eq.refl = Eq.refl
|
||||
|
||||
ℕ-eq : Rel ℕ ℓ
|
||||
ℕ-eq zero zero = ⊤
|
||||
ℕ-eq zero (suc m) = ⊥
|
||||
ℕ-eq (suc n) zero = ⊥
|
||||
ℕ-eq (suc n) (suc m) = ℕ-eq n m
|
||||
|
||||
⊤-setoid : Setoid ℓ ℓ
|
||||
⊤-setoid = record { Carrier = ⊤ ; _≈_ = _≡_ ; isEquivalence = Eq.isEquivalence }
|
||||
|
||||
ℕ-setoid : Setoid ℓ ℓ
|
||||
ℕ-setoid = record
|
||||
{ Carrier = ℕ
|
||||
; _≈_ = _≡_ -- ℕ-eq
|
||||
; isEquivalence = Eq.isEquivalence
|
||||
}
|
||||
|
||||
zero⟶ : SingletonSetoid {ℓ} {ℓ} ⟶ ℕ-setoid
|
||||
zero⟶ = record { _⟨$⟩_ = λ _ → zero ; cong = λ x → Eq.refl }
|
||||
suc⟶ : ℕ-setoid ⟶ ℕ-setoid
|
||||
suc⟶ = record { _⟨$⟩_ = suc ; cong = suc-cong }
|
||||
|
||||
ℕ-universal : ∀ {A : Setoid ℓ ℓ} → SingletonSetoid {ℓ} {ℓ} ⟶ A → A ⟶ A → ℕ-setoid ⟶ A
|
||||
ℕ-universal {A} z s = record { _⟨$⟩_ = app ; cong = cong' }
|
||||
where
|
||||
app : ℕ → Setoid.Carrier A
|
||||
app zero = z ⟨$⟩ tt
|
||||
app (suc n) = s ⟨$⟩ (app n)
|
||||
cong' : ∀ {n m : ℕ} → n ≡ m → Setoid._≈_ A (app n) (app m)
|
||||
cong' Eq.refl = IsEquivalence.refl (Setoid.isEquivalence A)
|
||||
|
||||
ℕ-z-commute : ∀ {A : Setoid ℓ ℓ} {q : SingletonSetoid {ℓ} {ℓ} ⟶ A} {f : A ⟶ A} → q ≋ (ℕ-universal q f ∘ zero⟶)
|
||||
ℕ-z-commute {A} {q} {f} {lift tt} _ = IsEquivalence.refl (Setoid.isEquivalence A)
|
||||
|
||||
ℕ-s-commute : ∀ {A : Setoid ℓ ℓ} {q : SingletonSetoid {ℓ} {ℓ} ⟶ A} {f : A ⟶ A} → (f ∘ (ℕ-universal q f)) ≋ (ℕ-universal q f ∘ suc⟶)
|
||||
ℕ-s-commute {A} {q} {f} {n} {m} n≡m rewrite n≡m = IsEquivalence.refl (Setoid.isEquivalence A)
|
||||
|
||||
ℕ-unique : ∀ {A : Setoid ℓ ℓ} {q : SingletonSetoid {ℓ} {ℓ} ⟶ A} {f : A ⟶ A} {u : ℕ-setoid ⟶ A} → q ≋ (u ∘ zero⟶) → (f ∘ u) ≋ (u ∘ suc⟶) → u ≋ ℕ-universal q f
|
||||
ℕ-unique {A} {q} {f} {u} qz fs {zero} {zero} Eq.refl = (≋-sym {SingletonSetoid} {A} {q} {u ∘ zero⟶} qz) tt
|
||||
ℕ-unique {A} {q} {f} {u} qz fs {suc n} {suc m} Eq.refl = AR.begin
|
||||
u ⟨$⟩ suc n AR.≈⟨ ≋-sym {ℕ-setoid} {A} {f ∘ u} {u ∘ suc⟶} fs Eq.refl ⟩
|
||||
f ∘ u ⟨$⟩ m AR.≈⟨ cong f (ℕ-unique {A} {q} {f} {u} qz fs {n} {m} Eq.refl) ⟩
|
||||
f ∘ ℕ-universal q f ⟨$⟩ n AR.≈⟨ ℕ-s-commute {A} {q} {f} {n} Eq.refl ⟩
|
||||
ℕ-universal q f ⟨$⟩ suc m AR.∎
|
||||
where module AR = SetoidR A
|
||||
|
||||
setoidNNO : NNO (Setoids ℓ ℓ) SingletonSetoid-⊤
|
||||
setoidNNO = record
|
||||
{ N = ℕ-setoid
|
||||
; isNNO = record
|
||||
{ z = zero⟶
|
||||
; s = suc⟶
|
||||
; universal = ℕ-universal
|
||||
; z-commute = λ {A} {q} {f} → ℕ-z-commute {A} {q} {f}
|
||||
; s-commute = λ {A} {q} {f} → ℕ-s-commute {A} {q} {f}
|
||||
; unique = λ {A} {q} {f} {u} qz fs → ℕ-unique {A} {q} {f} {u} qz fs
|
||||
}
|
||||
}
|
||||
|
||||
-- TODO might need explicit PNNO definition if we later have to work with them
|
||||
|
||||
setoidAmbient : Ambient (ℓ-suc ℓ) ℓ ℓ
|
||||
setoidAmbient = record { C = Setoids ℓ ℓ ; extensive = Setoids-Extensive ℓ ; cartesian = Setoids-Cartesian ; ℕ = NNO×CCC⇒PNNO (record { U = Setoids ℓ ℓ ; cartesianClosed = Setoids-CCC ℓ }) (Cocartesian.coproducts (Setoids-Cocartesian {ℓ} {ℓ})) setoidNNO }
|
||||
```
|
||||
|
|
@ -16,9 +16,8 @@ open import Relation.Binary
|
|||
open import Data.Sum using (_⊎_; inj₁; inj₂)
|
||||
open import Data.Sum.Function.Setoid
|
||||
open import Data.Sum.Relation.Binary.Pointwise
|
||||
open import Agda.Builtin.Unit using (tt)
|
||||
open import Data.Unit.Polymorphic using () renaming (⊤ to ⊤ₚ)
|
||||
open import Data.Empty.Polymorphic using () renaming (⊥ to ⊥ₚ)
|
||||
open import Data.Unit.Polymorphic using (tt; ⊤)
|
||||
open import Data.Empty.Polymorphic using (⊥)
|
||||
open import Categories.NaturalTransformation using (ntHelper)
|
||||
open import Function.Base using (id)
|
||||
```
|
||||
|
|
@ -37,9 +36,9 @@ Assuming the axiom of choice, the maybe monad is an instance of K in the categor
|
|||
just : A → Maybe A
|
||||
|
||||
maybe-eq : ∀ (A : Setoid c ℓ) → Maybe (Setoid.Carrier A) → Maybe (Setoid.Carrier A) → Set ℓ
|
||||
maybe-eq _ nothing nothing = ⊤ₚ
|
||||
maybe-eq _ nothing (just y) = ⊥ₚ
|
||||
maybe-eq _ (just x) nothing = ⊥ₚ
|
||||
maybe-eq _ nothing nothing = ⊤
|
||||
maybe-eq _ nothing (just y) = ⊥
|
||||
maybe-eq _ (just x) nothing = ⊥
|
||||
maybe-eq A (just x) (just y) = Setoid._≈_ A x y
|
||||
|
||||
maybeSetoid : Setoid c ℓ → Setoid c ℓ
|
||||
|
|
@ -47,7 +46,7 @@ Assuming the axiom of choice, the maybe monad is an instance of K in the categor
|
|||
where
|
||||
module A = Setoid A
|
||||
refl' : Reflexive (maybe-eq A)
|
||||
refl' {nothing} = lift tt
|
||||
refl' {nothing} = tt
|
||||
refl' {just x} = IsEquivalence.refl A.isEquivalence
|
||||
sym' : Symmetric (maybe-eq A)
|
||||
sym' {nothing} {nothing} = id
|
||||
|
|
@ -57,7 +56,7 @@ Assuming the axiom of choice, the maybe monad is an instance of K in the categor
|
|||
trans' : Transitive (maybe-eq A)
|
||||
trans' {nothing} {nothing} {nothing} = λ _ → id
|
||||
trans' {nothing} {nothing} {just z} = λ _ → id
|
||||
trans' {nothing} {just y} {nothing} = λ _ _ → lift tt
|
||||
trans' {nothing} {just y} {nothing} = λ _ _ → tt
|
||||
trans' {nothing} {just y} {just z} = λ ()
|
||||
trans' {just x} {nothing} {nothing} = λ ()
|
||||
trans' {just x} {nothing} {just z} = λ ()
|
||||
|
|
|
|||
Loading…
Reference in a new issue