blob: 08b65e342e1cfb88af259cec3bf089978c7c0f4a (
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
36
37
38
39
40
41
42
43
44
45
46
47
|
{-# OPTIONS --without-K --safe #-}
module Functor.Free.Instance.InducedSetoid where
-- The induced setoid of a (primitive) preorder
open import Categories.Category.Instance.Setoids using (Setoids)
open import Categories.Functor using (Functor)
open import Category.Instance.Preorders.Primitive using (Preorders)
open import Function using (Func)
open import Level using (Level)
open import Preorder.Primitive using (Preorder; module Isomorphism)
open import Preorder.Primitive.MonotoneMap using (MonotoneMap)
open import Relation.Binary using (Setoid)
module _ {c ℓ : Level} where
module _ (P : Preorder c ℓ) where
open Preorder P
open Isomorphism P using (_≅_; ≅-isEquivalence)
≅-setoid : Setoid c ℓ
≅-setoid = record
{ Carrier = Carrier
; _≈_ = _≅_
; isEquivalence = ≅-isEquivalence
}
func : {A B : Preorder c ℓ} → MonotoneMap A B → Func (≅-setoid A) (≅-setoid B)
func {A} {B} f = let open MonotoneMap f in record
{ to = map
; cong = map-resp-≅
}
open Isomorphism using (module ≅)
InducedSetoid : Functor (Preorders c ℓ) (Setoids c ℓ)
InducedSetoid = record
{ F₀ = ≅-setoid
; F₁ = func
; identity = λ {P} → ≅.refl P
; homomorphism = λ {Z = Z} → ≅.refl Z
; F-resp-≈ = λ f≃g {x} → f≃g x
}
module InducedSetoid = Functor InducedSetoid
|
