blob: b41b0a2bb7f8d639fc9ef7797494f7f372d4a344 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
|
module Instances where
open import Category.Functor using (RawFunctor)
open import Data.Maybe as M using (Maybe)
open import Data.Nat using (ℕ)
open import Data.Vec using (Vec)
open import Function using (_∘_ ; id)
open import Relation.Binary.PropositionalEquality as P using (_≗_ ; refl)
open import Structures using (Functor ; Shaped)
MaybeFunctor : Functor Maybe
MaybeFunctor = record
{ rawfunctor = M.functor
; isFunctor = record
{ cong = cong
; identity = identity
; composition = composition
} }
where _<$>_ = RawFunctor._<$>_ M.functor
cong : {α β : Set} {g h : α → β} → g ≗ h → _<$>_ g ≗ _<$>_ h
cong g≗h (M.just x) = P.cong M.just (g≗h x)
cong g≗h M.nothing = refl
identity : {α : Set} → _<$>_ {α} id ≗ id
identity (M.just x) = refl
identity M.nothing = refl
composition : {α β γ : Set} → (g : β → γ) → (h : α → β) → _<$>_ (g ∘ h) ≗ _<$>_ g ∘ _<$>_ h
composition g h (M.just x) = refl
composition g h M.nothing = refl
VecShaped : Shaped ℕ Vec
VecShaped = record
{ arity = id
; content = id
; fill = λ _ → id
; isShaped = record
{ content-fill = λ _ → refl
; fill-content = λ _ _ → refl
} }
|
