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