blob: f1fd85b6ec13dc2343c42bc0a98d63320a5be034 (
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
|
module Structures where
open import Category.Functor using (RawFunctor ; module RawFunctor)
open import Function using (_∘_ ; id)
open import Function.Equality using (_⟶_ ; _⇨_ ; _⟨$⟩_)
open import Relation.Binary using (_Preserves_⟶_)
open import Relation.Binary.PropositionalEquality as P using (_≗_ ; _≡_ ; refl)
record IsFunctor (F : Set → Set) (f : {α β : Set} → (α → β) → F α → F β) : Set₁ where
field
cong : {α β : Set} → f {α} {β} Preserves _≗_ ⟶ _≗_
identity : {α : Set} → f {α} id ≗ id
composition : {α β γ : Set} → (g : β → γ) → (h : α → β) →
f (g ∘ h) ≗ f g ∘ f h
isCongruence : {α β : Set} → (P.setoid α ⇨ P.setoid β) ⟶ P.setoid (F α) ⇨ P.setoid (F β)
isCongruence {α} {β} = record
{ _⟨$⟩_ = λ g → record
{ _⟨$⟩_ = f (_⟨$⟩_ g)
; cong = P.cong (f (_⟨$⟩_ g))
}
; cong = λ {g} {h} g≗h {x} x≡y → P.subst (λ z → f (_⟨$⟩_ g) x ≡ f (_⟨$⟩_ h) z) x≡y (cong (λ _ → g≗h refl) x)
}
record Functor (f : Set → Set) : Set₁ where
field
rawfunctor : RawFunctor f
isFunctor : IsFunctor f (RawFunctor._<$>_ rawfunctor)
open RawFunctor rawfunctor public
open IsFunctor isFunctor public
|
