blob: 27be24e6fb8d945d2f96f372193412db721c324d (
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
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
{-# OPTIONS --without-K --safe #-}
module Functor.Free.Instance.Preorder where
open import Categories.Category using (Category)
open import Categories.Category.Instance.Cats using (Cats)
open import Function using (flip)
open import Categories.Functor using (Functor; _∘F_)
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)
open import Category.Instance.Preorders.Primitive using (Preorders)
open import Level using (Level; _⊔_; suc)
open import Preorder.Primitive using (Preorder; module Isomorphism)
open import Preorder.Primitive.MonotoneMap using (MonotoneMap; _≃_; module ≃)
-- The "free preorder" of a category
-- i.e. (0,1)-truncation
-- In this setting, a category is a proof-relevant preorder,
-- i.e. each proof of A ≤ B is a distinct morphism.
-- To get a preorder from a category,
-- we ignore this distinction,
-- making all morphisms A ⇒ B "the same".
-- Identity and composition become reflexivity and transitivity.
-- Likewise, we can get a monotone map from a functor,
-- and a pointwise isomorphism of monotone maps from
-- a natural isomorphism of functors, simply by
-- forgetting morphism equalities.
module _ {o ℓ e : Level} where
preorder : Category o ℓ e → Preorder o ℓ
preorder C = let open Category C in record
{ Carrier = Obj
; _≲_ = _⇒_
; refl = id
; trans = flip _∘_
}
module _ {A B : Category o ℓ e} where
monotoneMap : Functor A B → MonotoneMap (preorder A) (preorder B)
monotoneMap F = let open Functor F in record
{ map = F₀
; mono = F₁
}
open NaturalIsomorphism using (module ⇒; module ⇐)
pointwiseIsomorphism : {F G : Functor A B} → NaturalIsomorphism F G → monotoneMap F ≃ monotoneMap G
pointwiseIsomorphism F≃G X = record
{ from = ⇒.η F≃G X
; to = ⇐.η F≃G X
}
Free : {o ℓ e : Level} → Functor (Cats o ℓ e) (Preorders o ℓ)
Free = record
{ F₀ = preorder
; F₁ = monotoneMap
; identity = ≃.refl {x = id}
; homomorphism = λ {f = f} {h} → ≃.refl {x = monotoneMap (h ∘F f)}
; F-resp-≈ = pointwiseIsomorphism
}
where
open Category (Preorders _ _) using (id)
module Free {o ℓ e} = Functor (Free {o} {ℓ} {e})
|
