diff options
| -rw-r--r-- | Category/Cartesian/Instance/Preorders/Primitive.agda | 68 | ||||
| -rw-r--r-- | Functor/Cartesian/Instance/InducedSetoid.agda | 54 | ||||
| -rw-r--r-- | Functor/Free/Instance/InducedMonoid.agda | 107 |
3 files changed, 229 insertions, 0 deletions
diff --git a/Category/Cartesian/Instance/Preorders/Primitive.agda b/Category/Cartesian/Instance/Preorders/Primitive.agda new file mode 100644 index 0000000..d366722 --- /dev/null +++ b/Category/Cartesian/Instance/Preorders/Primitive.agda @@ -0,0 +1,68 @@ +{-# OPTIONS --without-K --safe #-} + +module Category.Cartesian.Instance.Preorders.Primitive where + +open import Categories.Category.Cartesian using (Cartesian) +open import Level using (Level; suc; _⊔_) +open import Categories.Category.Cartesian.Bundle using (CartesianCategory) +open import Category.Instance.Preorder.Primitive.Preorders using (Preorders) +open import Preorder.Primitive using (Preorder; module Isomorphism) +open import Preorder.Primitive.MonotoneMap using (MonotoneMap; _≃_; module ≃) +open import Preorder.Primitive.Monoidal using (_×ₚ_) +open import Data.Unit.Polymorphic using (⊤) +open import Data.Product using (proj₁; proj₂; <_,_>; _,_) + + +module _ (c ℓ : Level) where + + private module _ (A B : Preorder c ℓ) where + + π₁ : MonotoneMap (A ×ₚ B) A + π₁ = record + { map = proj₁ + ; mono = proj₁ + } + + π₂ : MonotoneMap (A ×ₚ B) B + π₂ = record + { map = proj₂ + ; mono = proj₂ + } + + pair + : {C : Preorder c ℓ} + → MonotoneMap C A + → MonotoneMap C B + → MonotoneMap C (A ×ₚ B) + pair f g = let open MonotoneMap in record + { map = < map f , map g > + ; mono = < mono f , mono g > + } + + ⊤ₚ : Preorder c ℓ + ⊤ₚ = record + { Carrier = ⊤ + ; _≲_ = λ _ _ → ⊤ + } + + Preorders-Cartesian : Cartesian (Preorders c ℓ) + Preorders-Cartesian = record + { terminal = record { ⊤ = ⊤ₚ } + ; products = record + { product = λ {A} {B} → record + { A×B = A ×ₚ B + ; π₁ = π₁ A B + ; π₂ = π₂ A B + ; ⟨_,_⟩ = pair A B + ; project₁ = λ {h = h} → ≃.refl {x = h} + ; project₂ = λ {i = i} → ≃.refl {x = i} + ; unique = λ π₁∘j≃h π₂∘j≃i x → let open Isomorphism._≅_ in record + { from = to (π₁∘j≃h x) , to (π₂∘j≃i x) + ; to = from (π₁∘j≃h x) , from (π₂∘j≃i x) + } + } + } + } + + Preorders-CC : CartesianCategory (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ) + Preorders-CC = record { cartesian = Preorders-Cartesian } diff --git a/Functor/Cartesian/Instance/InducedSetoid.agda b/Functor/Cartesian/Instance/InducedSetoid.agda new file mode 100644 index 0000000..fa46290 --- /dev/null +++ b/Functor/Cartesian/Instance/InducedSetoid.agda @@ -0,0 +1,54 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Cartesian.Instance.InducedSetoid where + +-- The induced setoid functor is cartesian + +open import Categories.Category.BinaryProducts using (BinaryProducts) +open import Categories.Category.Cartesian.Bundle using (CartesianCategory) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-CartesianCategory) +open import Categories.Functor.Cartesian using (CartesianF) +open import Categories.Object.Product using (IsProduct) +open import Category.Cartesian.Instance.Preorders.Primitive using (Preorders-CC) +open import Data.Product using (<_,_>; _,_) +open import Function using (Func) +open import Functor.Free.Instance.InducedSetoid using () renaming (InducedSetoid to IS) +open import Level using (Level) +open import Preorder.Primitive using (Preorder; module Isomorphism) + +module _ {c ℓ : Level} where + + private + module Preorders-CC = CartesianCategory (Preorders-CC c ℓ) + module BP = BinaryProducts (Preorders-CC.products) + + IS-resp-× + : {A B : Preorder c ℓ} + → IsProduct (Setoids c ℓ) (IS.₁ {B = A} (BP.π₁ {B = B})) (IS.₁ BP.π₂) + IS-resp-× {A} {B} = record + { ⟨_,_⟩ = λ {S} S⟶ₛIS₀A S⟶ₛIS₀B → let open Func in record + { to = < to S⟶ₛIS₀A , to S⟶ₛIS₀B > + ; cong = λ x≈y → let open Isomorphism._≅_ in record + { from = from (cong S⟶ₛIS₀A x≈y) , from (cong S⟶ₛIS₀B x≈y) + ; to = to (cong S⟶ₛIS₀A x≈y) , to (cong S⟶ₛIS₀B x≈y) + } + } + ; project₁ = Isomorphism.≅.refl A + ; project₂ = Isomorphism.≅.refl B + ; unique = λ {S} {h} {i} {j} π₁∙h≈i π₂∙h≈j {x} → let open Isomorphism._≅_ in record + { from = to (π₁∙h≈i {x}) , to (π₂∙h≈j {x}) + ; to = from (π₁∙h≈i {x}) , from (π₂∙h≈j {x}) + } + } + + InducedSetoid : CartesianF (Preorders-CC c ℓ) (Setoids-CartesianCategory c ℓ) + InducedSetoid = record + { F = IS + ; isCartesian = record + { F-resp-⊤ = _ + ; F-resp-× = IS-resp-× + } + } + + module InducedSetoid = CartesianF InducedSetoid diff --git a/Functor/Free/Instance/InducedMonoid.agda b/Functor/Free/Instance/InducedMonoid.agda new file mode 100644 index 0000000..20cc6e7 --- /dev/null +++ b/Functor/Free/Instance/InducedMonoid.agda @@ -0,0 +1,107 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) + +module Functor.Free.Instance.InducedMonoid {c ℓ : Level} where + +-- The induced monoid of a monoidal preorder + +open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-monoidal′) +open import Categories.Object.Monoid Setoids-×.monoidal using (Monoid; Monoid⇒) +open import Categories.Category.Construction.Monoids Setoids-×.monoidal using (Monoids) +open import Categories.Functor using (Functor) +open import Category.Instance.Preorder.Primitive.Monoidals.Strong using (Monoidals) +open import Category.Cartesian.Instance.Preorders.Primitive using (Preorders-CC; ⊤ₚ) +open import Preorder.Primitive using (Preorder) +open import Preorder.Primitive.Monoidal using (MonoidalPreorder; _×ₚ_) +open import Preorder.Primitive.MonotoneMap.Monoidal.Strong using (MonoidalMonotone) +open import Preorder.Primitive using (module Isomorphism) +open import Data.Product using (_,_) +open import Functor.Cartesian.Instance.InducedSetoid using () renaming (module InducedSetoid to IS) +open import Function using (Func; _⟨$⟩_) +open import Function.Construct.Setoid using (_∙_) +open import Data.Setoid.Unit using (⊤ₛ) +open import Data.Setoid using (∣_∣) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Function.Construct.Constant using () renaming (function to Const) +open import Function.Construct.Identity using () renaming (function to Id) +open import Relation.Binary using (Setoid) + +open Setoids-× using (_⊗₀_; _⊗₁_; module unitorˡ; module unitorʳ; module associator; _≈_) + +module _ (P : MonoidalPreorder c ℓ) where + + open MonoidalPreorder P + open Isomorphism U using (module ≅; _≅_) + + M : Setoid c ℓ + M = IS.₀ U + + opaque + unfolding ×-monoidal′ + μ : Func (M ⊗₀ M) M + μ = IS.₁ tensor ∙ IS.×-iso.to U U + + η : Func Setoids-×.unit M + η = Const Setoids-×.unit M unit + + opaque + unfolding μ + assoc : μ ∙ μ ⊗₁ Id M ≈ μ ∙ Id M ⊗₁ μ ∙ associator.from + assoc {(x , y) , z} = associative x y z + + identityˡ : unitorˡ.from ≈ μ ∙ η ⊗₁ Id M + identityˡ {_ , x} = ≅.sym (unitaryˡ x) + + identityʳ : unitorʳ.from ≈ μ ∙ Id M ⊗₁ η + identityʳ {x , _} = ≅.sym (unitaryʳ x) + + ≅-monoid : Monoid + ≅-monoid = record + { Carrier = M + ; isMonoid = record + { μ = μ + ; η = Const Setoids-×.unit M unit + ; assoc = assoc + ; identityˡ = identityˡ + ; identityʳ = identityʳ + } + } + +module _ {A B : MonoidalPreorder c ℓ} (f : MonoidalMonotone A B) where + + private + module A = MonoidalPreorder A + module B = MonoidalPreorder B + + open Isomorphism B.U using (_≅_; module ≅) + open MonoidalMonotone f + + opaque + unfolding μ + preserves-μ + : {x : ∣ IS.₀ A.U ⊗₀ IS.₀ A.U ∣} + → map (μ A ⟨$⟩ x) + ≅ μ B ⟨$⟩ (IS.₁ F ⊗₁ IS.₁ F ⟨$⟩ x) + preserves-μ {x , y} = ≅.sym (⊗-homo x y) + + monoid⇒ : Monoid⇒ (≅-monoid A) (≅-monoid B) + monoid⇒ = record + { arr = IS.₁ F + ; preserves-μ = preserves-μ + ; preserves-η = ≅.sym ε + } + +InducedMonoid : Functor (Monoidals c ℓ) Monoids +InducedMonoid = record + { F₀ = ≅-monoid + ; F₁ = monoid⇒ + ; identity = λ {A} {x} → ≅.refl (U A) + ; homomorphism = λ {Z = Z} → ≅.refl (U Z) + ; F-resp-≈ = λ f≃g {x} → f≃g x + } + where + open MonoidalPreorder using (U) + open Isomorphism using (module ≅) + +module InducedMonoid = Functor InducedMonoid |