port theorem-{1,2} to PartialShapeVec
[~helmut/bidiragda.git] / Instances.agda
index faff6f8..b41b0a2 100644 (file)
@@ -1,11 +1,35 @@
 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 using (refl)
+open import Function using (_∘_ ; id)
+open import Relation.Binary.PropositionalEquality as P using (_≗_ ; refl)
 
-open import Structures using (Shaped)
+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