sym result of lemma-lookupM-{i,checkI}nsert-other
[~helmut/bidiragda.git] / 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 open import Data.Nat using (ℕ)
7 open import Data.Product using (_×_ ; _,_ ; proj₁ ; proj₂)
8 open import Data.Vec using (Vec)
9 import Data.Vec.Equality
10 open Data.Vec.Equality.PropositionalEquality using () renaming (to-≡ to VecEq-to-≡)
11 open import Function using (_∘_ ; id)
12 open import Relation.Binary using (Setoid ; module Setoid)
13 open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid)
14 open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≗_ ; module ≡-Reasoning)
15
16 open Setoid using () renaming (_≈_ to _∋_≈_)
17
18 open import Generic using (VecISetoid)
19 open import Structures using (Functor ; Shaped ; module Shaped)
20
21 MaybeFunctor : Functor Maybe
22 MaybeFunctor = record
23   { rawfunctor = M.functor
24   ; isFunctor = record
25     { cong = cong
26     ; identity = identity
27     ; composition = composition
28     } }
29   where _<$>_ : {α β : Set} → (α → β) → Maybe α → Maybe β
30         _<$>_ = RawFunctor._<$>_ M.functor
31
32         cong : {α β : Set} {g h : α → β} → g ≗ h → _<$>_ g ≗ _<$>_ h
33         cong g≗h (M.just x) = P.cong M.just (g≗h x)
34         cong g≗h M.nothing  = P.refl
35
36         identity : {α : Set} → _<$>_ {α} id ≗ id
37         identity (M.just x) = P.refl
38         identity M.nothing  = P.refl
39
40         composition : {α β γ : Set} → (g : β → γ) → (h : α → β) → _<$>_ (g ∘ h) ≗ _<$>_ g ∘ _<$>_ h
41         composition g h (M.just x) = P.refl
42         composition g h M.nothing  = P.refl
43
44 VecShaped : Shaped ℕ Vec
45 VecShaped = record
46   { arity = id
47   ; content = id
48   ; fill = λ _ → id
49   ; isShaped = record
50     { content-fill = λ _ → P.refl
51     ; fill-content = λ _ _ → P.refl
52     } }
53
54 ShapedISetoid : (S : Setoid ℓ₀ ℓ₀) {C : Set → (Setoid.Carrier S) → Set} → Shaped (Setoid.Carrier S) C → Setoid ℓ₀ ℓ₀ → ISetoid (Setoid.Carrier S) ℓ₀ ℓ₀
55 ShapedISetoid S {C} ShapeT α = record
56   { Carrier = C (Setoid.Carrier α)
57   ; _≈_ = λ {s₁} {s₂} c₁ c₂ → S ∋ s₁ ≈ s₂ × ISetoid._≈_ (VecISetoid α) (content c₁) (content c₂)
58   ; isEquivalence = record
59     { refl = Setoid.refl S , ISetoid.refl (VecISetoid α)
60     ; sym = λ p → Setoid.sym S (proj₁ p) , ISetoid.sym (VecISetoid α) (proj₂ p)
61     ; trans = λ p q → Setoid.trans S (proj₁ p) (proj₁ q) , ISetoid.trans (VecISetoid α) (proj₂ p) (proj₂ q)
62     } } where open Shaped ShapeT
63
64 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
65 Shaped≈-to-≡ ShapeT α {s} {x} {y} (shape≈ , content≈) = begin
66   x
67     ≡⟨ P.sym (content-fill x) ⟩
68   fill s (content x)
69     ≡⟨ P.cong (fill s) (VecEq-to-≡ content≈) ⟩
70   fill s (content y)
71     ≡⟨ content-fill y ⟩
72   y ∎
73   where open ≡-Reasoning
74         open Shaped ShapeT