Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- module Id where
- open import Relation.Binary.PropositionalEquality.Core
- open import Function
- data Id : Set → Set where
- Itself : ∀{A} → A → Id A
- fmap : ∀{A B} → (A → B) → Id A → Id B
- fmap f (Itself x) = Itself (f x)
- pure : ∀{A} → A -> Id A
- pure x = Itself x
- infixr 5 _>>=_
- _>>=_ : ∀{A B} → Id A → (A -> Id B) -> Id B
- Itself x >>= f = f x
- functorIdentity : ∀{A} → (x : Id A) → fmap id x ≡ x
- functorIdentity (Itself x) = refl
- functorComposition : ∀{A B C}
- → (x : Id A) → (g : A → B) → (f : B → C)
- → fmap (f ∘ g) x ≡ fmap f (fmap g x)
- functorComposition (Itself x) g f = refl
- pureBind : ∀{A B} → (x : A) → (f : A → Id B) → pure x >>= f ≡ f x
- pureBind x f = refl
- bindPure : ∀{A} → (x : Id A) → x >>= pure ≡ x
- bindPure (Itself x) = refl
- bindAssoc : ∀{A B C} → (m : Id A) → (f : A → Id B) → (g : B → Id C)
- → m >>= (λ x → f x >>= g) ≡ (m >>= f) >>= g
- bindAssoc (Itself x) f g = refl
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement