mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
work on examples
This commit is contained in:
parent
1a4b9135fc
commit
d0e11e8142
SSH key fingerprint:
SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
2 changed files with 142 additions and 2 deletions
142
src/Monad/Instance/K/Instance/Delay.lagda.md
Normal file
142
src/Monad/Instance/K/Instance/Delay.lagda.md
Normal file
|
|
@ -0,0 +1,142 @@
|
||||||
|
<!--
|
||||||
|
```agda
|
||||||
|
{-# OPTIONS --allow-unsolved-metas --guardedness #-}
|
||||||
|
|
||||||
|
open import Level
|
||||||
|
open import Category.Ambient using (Ambient)
|
||||||
|
open import Categories.Category
|
||||||
|
open import Categories.Category.Instance.Setoids
|
||||||
|
open import Categories.Monad
|
||||||
|
open import Categories.Category.Monoidal.Instance.Setoids
|
||||||
|
open import Categories.Category.Cocartesian
|
||||||
|
open import Categories.Object.Terminal
|
||||||
|
open import Function.Equality as SΠ renaming (id to idₛ)
|
||||||
|
import Categories.Morphism.Reasoning as MR
|
||||||
|
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 Data.Unit.Polymorphic using (tt; ⊤)
|
||||||
|
open import Data.Empty.Polymorphic using (⊥)
|
||||||
|
open import Categories.NaturalTransformation using (ntHelper)
|
||||||
|
open import Function.Base using (id)
|
||||||
|
import Relation.Binary.PropositionalEquality as Eq
|
||||||
|
open Eq using (_≡_)
|
||||||
|
open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
|
||||||
|
```
|
||||||
|
-->
|
||||||
|
|
||||||
|
```agda
|
||||||
|
module Monad.Instance.K.Instance.Delay {c ℓ} where
|
||||||
|
```
|
||||||
|
|
||||||
|
# Capretta's Delay Monad is an Instance of K in the Category of Setoids
|
||||||
|
|
||||||
|
```agda
|
||||||
|
record Delay (A : Set c) : Set c where
|
||||||
|
coinductive
|
||||||
|
field
|
||||||
|
node : A ⊎ Delay A
|
||||||
|
|
||||||
|
open Delay
|
||||||
|
|
||||||
|
now : ∀ {A : Set c} → A → Delay A
|
||||||
|
node (now {A} a) = inj₁ a
|
||||||
|
|
||||||
|
later : ∀ {A : Set c} → Delay A → Delay A
|
||||||
|
node (later {A} a) = inj₂ a
|
||||||
|
|
||||||
|
never : ∀ {A : Set c} → Delay A
|
||||||
|
node (never {A}) = inj₂ never
|
||||||
|
|
||||||
|
-- first try
|
||||||
|
delay-eq-strong : ∀ (A : Setoid c ℓ) → Delay (Setoid.Carrier A) → Delay (Setoid.Carrier A) → Set ℓ
|
||||||
|
delay-eq-strong A x y with node x | node y
|
||||||
|
... | inj₁ a | inj₁ b = Setoid._≈_ A a b
|
||||||
|
... | inj₁ a | inj₂ b = ⊥
|
||||||
|
... | inj₂ a | inj₁ b = ⊥
|
||||||
|
... | inj₂ a | inj₂ b = {! !}
|
||||||
|
|
||||||
|
-- second try
|
||||||
|
record eq-strong (A : Setoid c ℓ) (x : Delay (Setoid.Carrier A)) (y : Delay (Setoid.Carrier A)) : Set c where
|
||||||
|
field
|
||||||
|
node-eq₁ : (node x) ≡ (node y)
|
||||||
|
|
||||||
|
-- third try
|
||||||
|
mutual
|
||||||
|
node-eq : (A : Setoid c ℓ) (x y : Setoid.Carrier A ⊎ Delay (Setoid.Carrier A)) → Set ℓ
|
||||||
|
node-eq A (inj₁ x) (inj₁ y) = Setoid._≈_ A x y
|
||||||
|
node-eq A (inj₁ x) (inj₂ y) = ⊥
|
||||||
|
node-eq A (inj₂ x) (inj₁ y) = ⊥
|
||||||
|
node-eq A (inj₂ x) (inj₂ y) = delay-eq-strong' A x y
|
||||||
|
delay-eq-strong' : ∀ (A : Setoid c ℓ) → Delay (Setoid.Carrier A) → Delay (Setoid.Carrier A) → Set ℓ
|
||||||
|
delay-eq-strong' A x y = node-eq A {! !} {! !}
|
||||||
|
|
||||||
|
Delay-setoid : Setoid c ℓ → Setoid c ℓ
|
||||||
|
Delay-setoid A = record { Carrier = Delay A.Carrier ; _≈_ = {! !} ; isEquivalence = {! !} }
|
||||||
|
where
|
||||||
|
module A = Setoid A
|
||||||
|
|
||||||
|
|
||||||
|
-- finally this should work
|
||||||
|
mutual
|
||||||
|
record eq-strong' (A : Setoid c ℓ) (x : Delay (Setoid.Carrier A)) (y : Delay (Setoid.Carrier A)) : Set ℓ where
|
||||||
|
coinductive
|
||||||
|
field
|
||||||
|
eq : eq-strong'' A (node x) (node y)
|
||||||
|
eq-strong'' : (A : Setoid c ℓ) → (Setoid.Carrier A ⊎ Delay (Setoid.Carrier A)) → (Setoid.Carrier A ⊎ Delay (Setoid.Carrier A)) → Set ℓ
|
||||||
|
eq-strong'' A (inj₁ x) (inj₁ y) = Setoid._≈_ A x y
|
||||||
|
eq-strong'' A (inj₁ x) (inj₂ y) = ⊥
|
||||||
|
eq-strong'' A (inj₂ x) (inj₁ y) = ⊥
|
||||||
|
eq-strong'' A (inj₂ x) (inj₂ y) = eq-strong' A x y
|
||||||
|
|
||||||
|
|
||||||
|
-- this should also work
|
||||||
|
mutual
|
||||||
|
record eq-weak (A : Setoid c ℓ) (x : Delay (Setoid.Carrier A)) (y : Delay (Setoid.Carrier A)) : Set ℓ where
|
||||||
|
coinductive
|
||||||
|
field
|
||||||
|
eq : eq-weak' A (node x) (node y)
|
||||||
|
eq-weak' : (A : Setoid c ℓ) → (Setoid.Carrier A ⊎ Delay (Setoid.Carrier A)) → (Setoid.Carrier A ⊎ Delay (Setoid.Carrier A)) → Set ℓ
|
||||||
|
eq-weak' A (inj₁ x) (inj₁ y) = Setoid._≈_ A x y
|
||||||
|
eq-weak' A (inj₁ x) (inj₂ y) = eq-weak A (now x) y
|
||||||
|
eq-weak' A (inj₂ x) (inj₁ y) = eq-weak A x (now y)
|
||||||
|
eq-weak' A (inj₂ x) (inj₂ y) = eq-weak A x y
|
||||||
|
open eq-weak
|
||||||
|
|
||||||
|
now-cong : ∀ {A : Setoid c ℓ} {a b : Setoid.Carrier A} → Setoid._≈_ A a b → eq-weak A (now a) (now b)
|
||||||
|
eq (now-cong {A} {a} {b} a≈b) = a≈b
|
||||||
|
|
||||||
|
now-inj : ∀ {A : Setoid c ℓ} {a b : Setoid.Carrier A} → eq-weak A (now a) (now b) → Setoid._≈_ A a b
|
||||||
|
now-inj {A} {a} {b} na≈nb with (eq na≈nb)
|
||||||
|
... | a≈b = a≈b
|
||||||
|
|
||||||
|
now-weak-eq : ∀ {A : Setoid c ℓ} {a : Setoid.Carrier A} {b : Delay (Setoid.Carrier A)} → eq-weak A (now a) b → Σ (Setoid.Carrier A) (λ c → Setoid._≈_ A a c)
|
||||||
|
now-weak-eq {A} {a} {b} na≈b with node b | eq na≈b
|
||||||
|
... | inj₁ x | a≈b = x , a≈b
|
||||||
|
... | inj₂ x | a≈b = {! !}
|
||||||
|
|
||||||
|
weak-setoid : Setoid c ℓ → Setoid c ℓ
|
||||||
|
weak-setoid A = record { Carrier = Delay (Setoid.Carrier A) ; _≈_ = eq-weak A ; isEquivalence = record { refl = refl' ; sym = sym' ; trans = trans' } }
|
||||||
|
where
|
||||||
|
refl' : Reflexive (eq-weak A)
|
||||||
|
eq (refl' {a}) with node a
|
||||||
|
... | inj₁ x = IsEquivalence.refl (Setoid.isEquivalence A)
|
||||||
|
... | inj₂ x = refl'
|
||||||
|
sym' : Symmetric (eq-weak A)
|
||||||
|
eq (sym' {a} {b} a≈b) with node a | node b | eq a≈b
|
||||||
|
... | inj₁ x | inj₁ y | z = IsEquivalence.sym (Setoid.isEquivalence A) z
|
||||||
|
... | inj₂ x | inj₁ y | z = sym' z
|
||||||
|
... | inj₁ x | inj₂ y | z = sym' z
|
||||||
|
... | inj₂ x | inj₂ y | z = sym' z
|
||||||
|
trans' : Transitive (eq-weak A)
|
||||||
|
eq (trans' {a} {b} {c} a≈b b≈c) with node a | node b | node c | eq a≈b | eq b≈c
|
||||||
|
... | inj₂ x | inj₂ y | inj₂ z | eq₁ | eq₂ = trans' eq₁ eq₂
|
||||||
|
... | inj₁ x | inj₂ y | inj₂ z | eq₁ | eq₂ = trans' eq₁ eq₂
|
||||||
|
... | inj₂ x | inj₁ y | inj₂ z | eq₁ | eq₂ = trans' eq₁ eq₂
|
||||||
|
... | inj₁ x | inj₁ y | inj₂ z | eq₁ | eq₂ = trans' (now-cong eq₁) eq₂ -- trans' (now-cong eq₁) eq₂
|
||||||
|
... | inj₂ x | inj₂ y | inj₁ z | eq₁ | eq₂ = trans' eq₁ eq₂
|
||||||
|
... | inj₁ x | inj₂ y | inj₁ z | eq₁ | eq₂ = {! trans' eq₁ eq₂ !} -- now-inj {A} {x} {z} (trans' eq₁ eq₂)
|
||||||
|
... | inj₂ x | inj₁ y | inj₁ z | eq₁ | eq₂ = trans' eq₁ (now-cong eq₂)
|
||||||
|
... | inj₁ x | inj₁ y | inj₁ z | eq₁ | eq₂ = IsEquivalence.trans (Setoid.isEquivalence A) eq₁ eq₂
|
||||||
|
```
|
||||||
|
|
@ -147,6 +147,4 @@ Assuming the axiom of choice, the maybe monad is an instance of K in the categor
|
||||||
; identityˡ = λ {A} {i} {j} → identityˡ {A} {i} {j}
|
; identityˡ = λ {A} {i} {j} → identityˡ {A} {i} {j}
|
||||||
; identityʳ = λ {A} {i} {j} → identityʳ {A} {i} {j}
|
; identityʳ = λ {A} {i} {j} → identityʳ {A} {i} {j}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
```
|
```
|
||||||
Loading…
Reference in a new issue