f1fd85b6ec13dc2343c42bc0a98d63320a5be034
[~helmut/bidiragda.git] / Structures.agda
1 module Structures where
2
3 open import Category.Functor using (RawFunctor ; module RawFunctor)
4 open import Function using (_∘_ ; id)
5 open import Function.Equality using (_⟶_ ; _⇨_ ; _⟨$⟩_)
6 open import Relation.Binary using (_Preserves_⟶_)
7 open import Relation.Binary.PropositionalEquality as P using (_≗_ ; _≡_ ; refl)
8
9 record IsFunctor (F : Set → Set) (f : {α β : Set} → (α →  β) → F α → F β) : Set₁ where
10   field
11     cong : {α β : Set} → f {α} {β} Preserves _≗_ ⟶ _≗_
12     identity : {α : Set} → f {α} id ≗ id
13     composition : {α β γ : Set} → (g : β → γ) → (h : α → β) →
14                   f (g ∘ h) ≗ f g ∘ f h
15
16   isCongruence : {α β : Set} → (P.setoid α ⇨ P.setoid β) ⟶ P.setoid (F α) ⇨ P.setoid (F β)
17   isCongruence {α} {β} = record
18     { _⟨$⟩_ = λ g → record
19       { _⟨$⟩_ = f (_⟨$⟩_ g)
20       ; cong = P.cong (f (_⟨$⟩_ g))
21       }
22     ; cong = λ {g} {h} g≗h {x} x≡y → P.subst (λ z → f (_⟨$⟩_ g) x ≡ f (_⟨$⟩_ h) z) x≡y (cong (λ _ → g≗h refl) x)
23     }
24
25 record Functor (f : Set → Set) : Set₁ where
26   field
27     rawfunctor : RawFunctor f
28     isFunctor : IsFunctor f (RawFunctor._<$>_ rawfunctor)
29
30   open RawFunctor rawfunctor public
31   open IsFunctor isFunctor public