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-11-30 16:40:30 +01:00
parent af3b6ee7c3
commit 7cf428e05c
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 5 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -48,16 +48,12 @@ module _ {c ℓ' : Level} where
open Equiv open Equiv
-- open Setoid -- open Setoid
private data Maybe {a} (A : Set a) : Set a where
variable
a : Level
data Maybe (A : Set a) : Set a where
nothing : Maybe A nothing : Maybe A
just : A → Maybe A just : A → Maybe A
maybeSetoid : ∀ (A : Set a) → Setoid' a a maybeSetoid : ∀ {a} (A : Set a) → Setoid' a a
maybeSetoid A = record { Carrier = Maybe A ; _≈_ = eq ; isEquivalence = record { refl = refl' ; sym = sym' ; trans = trans' } } maybeSetoid {a} A = record { Carrier = Maybe A ; _≈_ = eq ; isEquivalence = record { refl = refl' ; sym = sym' ; trans = trans' } }
where where
eq : Maybe A → Maybe A → Set a eq : Maybe A → Maybe A → Set a
eq nothing nothing = ⊤ₚ eq nothing nothing = ⊤ₚ
@ -83,6 +79,8 @@ module _ {c ℓ' : Level} where
trans' {just x} {just y} {just z} = trans-≡ trans' {just x} {just y} {just z} = trans-≡
-- maybe-η : -- maybe-η :
lift-maybe : ∀ {a} (A : Set a) (x : A) → Maybe A
lift-maybe {a} A x = just x
-- TODO this is completely wrong... -- TODO this is completely wrong...
maybe : Monad Setoids maybe : Monad Setoids