blob: 0e069d20ec5b36042d59a709e8268b2e212e28b2 (
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
|
{-# OPTIONS --without-K --safe #-}
open import Level using (Level; _⊔_)
module NaturalTransformation.Instance.EmptyList {c ℓ : Level} where
open import Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to ⊤ₛ)
open import Categories.Functor using (Functor)
open import Categories.Functor.Construction.Constant using (const)
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
open import Data.Opaque.List using (Listₛ; []ₛ; mapₛ)
open import Data.Setoid using (_⇒ₛ_)
open import Function using (_⟶ₛ_)
open import Function.Construct.Constant using () renaming (function to Const)
open import Function.Construct.Setoid using (_∙_)
open import Functor.Instance.List {c} {ℓ} using (List)
open import Relation.Binary using (Setoid)
opaque
unfolding []ₛ
map-[]ₛ : {A B : Setoid c ℓ}
→ (f : A ⟶ₛ B)
→ (open Setoid (⊤ₛ ⇒ₛ Listₛ B))
→ []ₛ ≈ mapₛ f ∙ []ₛ
map-[]ₛ {_} {B} f = refl
where
open Setoid (List.₀ B)
⊤⇒[] : NaturalTransformation (const ⊤ₛ) List
⊤⇒[] = ntHelper record
{ η = λ X → []ₛ
; commute = map-[]ₛ
}
|
