Instances.agda

   1 module Instances where
   2
   3 open import Level using () renaming (zero to ℓ₀)
   4 open import Category.Functor using (RawFunctor)
   5 open import Data.Maybe as M using (Maybe)
   6 import Data.Maybe.Categorical
   7 open import Data.Nat using (ℕ)
   8 open import Data.Product using (_×_ ; _,_ ; proj₁ ; proj₂)
   9 open import Data.Vec using (Vec)
  10 open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise-≡⇒≡)
  11 open import Function using (_∘_ ; id)
  12 open import Relation.Binary using (Setoid ; module Setoid)
  13 open import Relation.Binary.Indexed.Heterogeneous using () renaming (IndexedSetoid to ISetoid)
  14 open import Relation.Binary.Indexed.Heterogeneous.Construct.At using (_atₛ_)
  15 open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≗_ ; module ≡-Reasoning)
  16
  17 open Setoid using () renaming (_≈_ to _∋_≈_)
  18
  19 open import Generic using (VecISetoid)
  20 open import Structures using (Functor ; Shaped ; module Shaped)
  21
  22 MaybeFunctor : Functor Maybe
  23 MaybeFunctor = record
  24   { rawfunctor = Data.Maybe.Categorical.functor
  25   ; isFunctor = record
  26     { cong = cong
  27     ; identity = identity
  28     ; composition = composition
  29     } }
  30   where _<$>_ : {α β : Set} → (α → β) → Maybe α → Maybe β
  31         _<$>_ = RawFunctor._<$>_ Data.Maybe.Categorical.functor
  32
  33         cong : {α β : Set} {g h : α → β} → g ≗ h → _<$>_ g ≗ _<$>_ h
  34         cong g≗h (M.just x) = P.cong M.just (g≗h x)
  35         cong g≗h M.nothing  = P.refl
  36
  37         identity : {α : Set} → _<$>_ {α} id ≗ id
  38         identity (M.just x) = P.refl
  39         identity M.nothing  = P.refl
  40
  41         composition : {α β γ : Set} → (g : β → γ) → (h : α → β) → _<$>_ (g ∘ h) ≗ _<$>_ g ∘ _<$>_ h
  42         composition g h (M.just x) = P.refl
  43         composition g h M.nothing  = P.refl
  44
  45 VecShaped : Shaped ℕ Vec
  46 VecShaped = record
  47   { arity = id
  48   ; content = id
  49   ; fill = λ _ → id
  50   ; isShaped = record
  51     { content-fill = λ _ → P.refl
  52     ; fill-content = λ _ _ → P.refl
  53     } }
  54
  55 ShapedISetoid : (S : Setoid ℓ₀ ℓ₀) {C : Set → (Setoid.Carrier S) → Set} → Shaped (Setoid.Carrier S) C → Setoid ℓ₀ ℓ₀ → ISetoid (Setoid.Carrier S) ℓ₀ ℓ₀
  56 ShapedISetoid S {C} ShapeT α = record
  57   { Carrier = C (Setoid.Carrier α)
  58   ; _≈_ = λ {s₁} {s₂} c₁ c₂ → S ∋ s₁ ≈ s₂ × ISetoid._≈_ (VecISetoid α) (content c₁) (content c₂)
  59   ; isEquivalence = record
  60     { refl = Setoid.refl S , ISetoid.refl (VecISetoid α)
  61     ; sym = λ p → Setoid.sym S (proj₁ p) , ISetoid.sym (VecISetoid α) (proj₂ p)
  62     ; trans = λ p q → Setoid.trans S (proj₁ p) (proj₁ q) , ISetoid.trans (VecISetoid α) (proj₂ p) (proj₂ q)
  63     } } where open Shaped ShapeT
  64
  65 Shaped≈-to-≡ : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (α : Set) → {s : S} {x y : C α s} → ShapedISetoid (P.setoid S) ShapeT (P.setoid α) atₛ s ∋ x ≈ y → x ≡ y
  66 Shaped≈-to-≡ ShapeT α {s} {x} {y} (shape≈ , content≈) = begin
  67   x
  68     ≡⟨ P.sym (content-fill x) ⟩
  69   fill s (content x)
  70     ≡⟨ P.cong (fill s) (Pointwise-≡⇒≡ content≈) ⟩
  71   fill s (content y)
  72     ≡⟨ content-fill y ⟩
  73   y ∎
  74   where open ≡-Reasoning
  75         open Shaped ShapeT