leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

Work on maybe

Browse source
This commit is contained in:
Leon Vatthauer 2023-12-01 15:34:21 +01:00
parent 7be2f41196
commit b63d5455be
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 16 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/Monad/Instance/K/Instance/Maybe.lagda.md
View file

@ -25,8 +25,8 @@ open import Function.Base using (id)
-->
```agda
module Monad.Instance.K.Instance.Maybe {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient using ()
-- TODO arguments c ℓ here!
module Monad.Instance.K.Instance.Maybe {o ℓ e} where
```
# The Maybe Monad as instance of K
@ -85,12 +85,18 @@ module _ {c ℓ : Level} where
maybeFun-comp : ∀ {A B C : Setoid c ℓ} (f : A ⟶ B) (g : B ⟶ C) → maybeFun (g ∘ f) ≋ ((maybeFun g) ∘ (maybeFun f))
maybeFun-comp {A} {B} {C} f g {nothing} {nothing} i≈j = i≈j
maybeFun-comp {A} {B} {C} f g {just i} {just j} i≈j = cong g (cong f i≈j)
maybeFun-comp {A} {B} {C} f g {just _} {just _} i≈j = cong g (cong f i≈j)
maybeFun-resp-≈ : ∀ {A B : Setoid c ℓ} {f g : A ⟶ B} → f ≋ g → maybeFun f ≋ maybeFun g
maybeFun-resp-≈ {A} {B} {f} {g} f≈g {nothing} {nothing} i≈j = i≈j
maybeFun-resp-≈ {A} {B} {f} {g} f≈g {just _} {just _} i≈j = f≈g i≈j
η : ∀ (A : Setoid c ℓ) → A ⟶ maybeSetoid A
η A = record { _⟨$⟩_ = just ; cong = id }
η-natural : ∀ {A B : Setoid c ℓ} (f : A ⟶ B) → (η B ∘ f) ≋ (maybeFun f ∘ η A)
η-natural {A} {B} f {i} {j} i≈j = cong f i≈j
μ : ∀ (A : Setoid c ℓ) → maybeSetoid (maybeSetoid A) ⟶ maybeSetoid A
μ A = record { _⟨$⟩_ = app ; cong = λ {i} {j} → cong' i j }
where
@ -100,6 +106,10 @@ module _ {c ℓ : Level} where
cong' : ∀ (i j : Maybe (Maybe (Setoid.Carrier A))) → maybe-eq (maybeSetoid A) i j → maybe-eq A (app i) (app j)
cong' nothing nothing i≈j = i≈j
cong' (just i) (just j) i≈j = i≈j
μ-natural : ∀ {A B : Setoid c ℓ} (f : A ⟶ B) → (μ B ∘ maybeFun (maybeFun f)) ≋ (maybeFun f ∘ μ A)
μ-natural {A} {B} f {nothing} {nothing} i≈j = i≈j
μ-natural {A} {B} f {just i} {just j} i≈j = cong (maybeFun f) {i} {j} i≈j
maybeMonad : Monad (Setoids c ℓ)
maybeMonad = record
@ -108,15 +118,15 @@ module _ {c ℓ : Level} where
; F₁ = maybeFun
; identity = λ {A} {x} {y} → maybeFun-id {A = A} {x} {y}
; homomorphism = λ {A} {B} {C} {f} {g} {i} {j} → maybeFun-comp {A} {B} {C} f g {i} {j}
; F-resp-≈ = {! !}
; F-resp-≈ = maybeFun-resp-≈
}
; η = ntHelper (record
{ η = η
; commute = {! !}
; commute = η-natural
})
; μ = ntHelper (record
{ η = μ
; commute = {! !}
; commute = μ-natural
})
; assoc = {! !}
; sym-assoc = {! !}