From 7cf428e05c124aeb9d695c83c4bb6522f517a2d2 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Thu, 30 Nov 2023 16:40:30 +0100 Subject: [PATCH] minor --- src/Monad/Instance/K/Instance/Maybe.lagda.md | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/src/Monad/Instance/K/Instance/Maybe.lagda.md b/src/Monad/Instance/K/Instance/Maybe.lagda.md index 77bebf3..5ca50cf 100644 --- a/src/Monad/Instance/K/Instance/Maybe.lagda.md +++ b/src/Monad/Instance/K/Instance/Maybe.lagda.md @@ -48,16 +48,12 @@ module _ {c ℓ' : Level} where open Equiv -- open Setoid - private - variable - a : Level - - data Maybe (A : Set a) : Set a where + data Maybe {a} (A : Set a) : Set a where nothing : Maybe A just : A → Maybe A - maybeSetoid : ∀ (A : Set a) → Setoid' a a - maybeSetoid A = record { Carrier = Maybe A ; _≈_ = eq ; isEquivalence = record { refl = refl' ; sym = sym' ; trans = trans' } } + maybeSetoid : ∀ {a} (A : Set a) → Setoid' a a + maybeSetoid {a} A = record { Carrier = Maybe A ; _≈_ = eq ; isEquivalence = record { refl = refl' ; sym = sym' ; trans = trans' } } where eq : Maybe A → Maybe A → Set a eq nothing nothing = ⊤ₚ @@ -83,6 +79,8 @@ module _ {c ℓ' : Level} where trans' {just x} {just y} {just z} = trans-≡ -- maybe-η : + lift-maybe : ∀ {a} (A : Set a) (x : A) → Maybe A + lift-maybe {a} A x = just x -- TODO this is completely wrong... maybe : Monad Setoids