diff options
| -rw-r--r-- | Category/Instance/Preorders/Primitive.agda | 4 | ||||
| -rw-r--r-- | Functor/Forgetful/Instance/Preorder.agda | 25 | ||||
| -rw-r--r-- | Functor/Free/Instance/InducedSetoid.agda | 47 | ||||
| -rw-r--r-- | Functor/Free/Instance/Preorder.agda | 68 | ||||
| -rw-r--r-- | Preorder/Primitive/MonotoneMap.agda | 23 |
5 files changed, 153 insertions, 14 deletions
diff --git a/Category/Instance/Preorders/Primitive.agda b/Category/Instance/Preorders/Primitive.agda index 49b687f..9c36d03 100644 --- a/Category/Instance/Preorders/Primitive.agda +++ b/Category/Instance/Preorders/Primitive.agda @@ -7,7 +7,7 @@ open import Categories.Category.Helper using (categoryHelper) open import Function using (id; _∘_) open import Level using (Level; _⊔_; suc) open import Preorder.Primitive using (Preorder; module Isomorphism) -open import Preorder.Primitive.MonotoneMap using (MonotoneMap; _≃_; ≃-isEquivalence; module ≃; map-resp-≅) +open import Preorder.Primitive.MonotoneMap using (MonotoneMap; _≃_; ≃-isEquivalence; module ≃) -- The category of primitive preorders and monotone maps @@ -39,7 +39,7 @@ private → compose f g ≃ compose h i compose-resp-≃ {C = C} {h = h} {g} f≃h g≃i x = ≅.trans (f≃h (map g x)) (map-resp-≅ h (g≃i x)) where - open MonotoneMap using (map; mono) + open MonotoneMap using (map; mono; map-resp-≅) open Preorder C open Isomorphism C diff --git a/Functor/Forgetful/Instance/Preorder.agda b/Functor/Forgetful/Instance/Preorder.agda new file mode 100644 index 0000000..e6957d2 --- /dev/null +++ b/Functor/Forgetful/Instance/Preorder.agda @@ -0,0 +1,25 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Forgetful.Instance.Preorder where + +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Functor using (Functor) +open import Category.Instance.Preorders using (Preorders) +open import Level using (Level) +open import Relation.Binary.Bundles using (Preorder) +open import Relation.Binary.Morphism using (PreorderHomomorphism) + +-- Get the underlying setoid of a preorder. +-- This is not the same thing as the setoid induced by _≲_. + +Forget : {c ℓ e : Level} → Functor (Preorders c ℓ e) (Setoids c ℓ) +Forget = let open Preorder.Eq in record + { F₀ = setoid + ; F₁ = λ F → let open PreorderHomomorphism F in record + { to = ⟦_⟧ + ; cong = cong + } + ; identity = λ {A} → refl A + ; homomorphism = λ {_ _ Z} → refl Z + ; F-resp-≈ = λ f≗g → f≗g + } diff --git a/Functor/Free/Instance/InducedSetoid.agda b/Functor/Free/Instance/InducedSetoid.agda new file mode 100644 index 0000000..08b65e3 --- /dev/null +++ b/Functor/Free/Instance/InducedSetoid.agda @@ -0,0 +1,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 diff --git a/Functor/Free/Instance/Preorder.agda b/Functor/Free/Instance/Preorder.agda new file mode 100644 index 0000000..27be24e --- /dev/null +++ b/Functor/Free/Instance/Preorder.agda @@ -0,0 +1,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}) diff --git a/Preorder/Primitive/MonotoneMap.agda b/Preorder/Primitive/MonotoneMap.agda index 6a2224b..aad8f0f 100644 --- a/Preorder/Primitive/MonotoneMap.agda +++ b/Preorder/Primitive/MonotoneMap.agda @@ -18,14 +18,22 @@ record MonotoneMap {c₁ c₂ ℓ₁ ℓ₂ : Level} (P : Preorder c₁ ℓ₁) map : P.Carrier → Q.Carrier mono : {x y : P.Carrier} → x P.≲ y → map x Q.≲ map y + private + module P′ = Isomorphism P + module Q′ = Isomorphism Q + + map-resp-≅ : {x y : P.Carrier} → x P′.≅ y → map x Q′.≅ map y + map-resp-≅ x≅y = let open P′._≅_ x≅y in record + { from = mono from + ; to = mono to + } + -- Pointwise isomorphism of monotone maps module _ {c₁ c₂ ℓ₁ ℓ₂ : Level} {P : Preorder c₁ ℓ₁} {Q : Preorder c₂ ℓ₂} where private - module P where - open Preorder P public - open Isomorphism P public + module P = Preorder P module Q = Isomorphism Q open MonotoneMap using (map) @@ -54,12 +62,3 @@ module _ {c₁ c₂ ℓ₁ ℓ₂ : Level} {P : Preorder c₁ ℓ₁} {Q : Preor } module ≃ = IsEquivalence ≃-isEquivalence - - map-resp-≅ : (f : MonotoneMap P Q) {x y : P.Carrier} → x P.≅ y → map f x Q.≅ map f y - map-resp-≅ f x≅y = record - { from = mono from - ; to = mono to - } - where - open P._≅_ x≅y - open MonotoneMap f |