diff --git a/src/Category/Ambient/Setoid.lagda.md b/src/Category/Ambient/Setoid.lagda.md index e2a40b0..ba3aa7e 100644 --- a/src/Category/Ambient/Setoid.lagda.md +++ b/src/Category/Ambient/Setoid.lagda.md @@ -1,3 +1,111 @@ + + +# 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 } +``` \ No newline at end of file diff --git a/src/Monad/Instance/K/Instance/Maybe.lagda.md b/src/Monad/Instance/K/Instance/Maybe.lagda.md index aaad51f..32d1627 100644 --- a/src/Monad/Instance/K/Instance/Maybe.lagda.md +++ b/src/Monad/Instance/K/Instance/Maybe.lagda.md @@ -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} = λ ()