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

minor

Browse source
This commit is contained in:
Leon Vatthauer 2023-12-01 14:46:36 +01:00
parent 11107c67b8
commit 7be2f41196
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -83,6 +83,10 @@ module _ {c ℓ : Level} where
maybeFun-id {A} {nothing} {nothing} i≈j = i≈j
maybeFun-id {A} {just _} {just _} i≈j = i≈j
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)
η : ∀ (A : Setoid c ℓ) → A ⟶ maybeSetoid A
η A = record { _⟨$⟩_ = just ; cong = id }
@ -103,7 +107,7 @@ module _ {c ℓ : Level} where
{ F₀ = maybeSetoid
; F₁ = maybeFun
; identity = λ {A} {x} {y} → maybeFun-id {A = A} {x} {y}
; homomorphism = {! !}
; homomorphism = λ {A} {B} {C} {f} {g} {i} {j} → maybeFun-comp {A} {B} {C} f g {i} {j}
; F-resp-≈ = {! !}
}
; η = ntHelper (record