99 lines
3 KiB
Agda
99 lines
3 KiB
Agda
|
module TotalOrder where
|
|||
|
|
|
|||
|
|
open import Level
|
|||
|
|
open import Relation.Binary using (Poset; TotalOrder)
|
|||
|
|
open import Categories.Monad
|
|||
|
|
open import Categories.Monad.Strong
|
|||
|
|
open import Categories.Category
|
|||
|
|
open import Categories.Category.Construction.Thin
|
|||
|
|
open import Categories.Category.Cartesian
|
|||
|
|
open import Categories.Category.BinaryProducts
|
|||
|
|
open import Categories.Object.Product
|
|||
|
|
open import Categories.Object.Terminal
|
|||
|
|
open import Categories.Functor renaming (id to Id)
|
|||
|
|
open import Categories.NaturalTransformation
|
|||
|
|
open import Categories.Category.Monoidal
|
|||
|
|
open import Data.Product renaming (_×_ to _∧_)
|
|||
|
|
open import Agda.Builtin.Unit
|
|||
|
|
open import Poset
|
|||
|
|
open import Data.Sum
|
|||
|
|
open import Relation.Nullary
|
|||
|
|
|
|||
|
|
private
|
|||
|
|
variable
|
|||
|
|
o ℓ₁ ℓ₂ e : Level
|
|||
|
|
|
|||
|
|
Closure→Cartesian : ∀ {𝑃 : Poset o ℓ₁ ℓ₂} → (Closure 𝑃) → Cartesian (Thin _ 𝑃)
|
|||
|
|
Closure→Cartesian {𝑃} Clo = record
|
|||
|
|
{ terminal = record
|
|||
|
|
{ ⊤ = _
|
|||
|
|
; ⊤-is-terminal = _
|
|||
|
|
}
|
|||
|
|
; products = _
|
|||
|
|
}
|
|||
|
|
where
|
|||
|
|
open Closure Clo
|
|||
|
|
|
|||
|
|
module _ (𝑇 : TotalOrder o ℓ₁ ℓ₂) where
|
|||
|
|
-- Closure on total order
|
|||
|
|
open TotalOrder 𝑇 renaming (poset to 𝑃)
|
|||
|
|
TClosure : Set (o ⊔ ℓ₁ ⊔ ℓ₂)
|
|||
|
|
TClosure = Closure 𝑃
|
|||
|
|
|
|||
|
|
postulate
|
|||
|
|
em : ∀ {A : Set ℓ₂} → A ⊎ ¬ A
|
|||
|
|
|
|||
|
|
T-Product : ∀ (Clo : Closure 𝑃) (X Y : Carrier) → Product (Thin e 𝑃) X Y
|
|||
|
|
T-Product Clo X Y with em {X ≤ Y} in eq
|
|||
|
|
... | inj₁ x = {! !}
|
|||
|
|
... | inj₂ x = {! !}
|
|||
|
|
where
|
|||
|
|
open Closure Clo
|
|||
|
|
|
|||
|
|
|
|||
|
|
-- TODO remove once certain that no prove needed
|
|||
|
|
Thin-Monoidal : Monoidal (Thin e 𝑃)
|
|||
|
|
Thin-Monoidal = monoidalHelper (Thin _ 𝑃) record
|
|||
|
|
{ ⊗ = record
|
|||
|
|
{ F₀ = λ p → {! !}
|
|||
|
|
; F₁ = _
|
|||
|
|
; identity = _
|
|||
|
|
; homomorphism = _
|
|||
|
|
; F-resp-≈ = _
|
|||
|
|
}
|
|||
|
|
; unit = _
|
|||
|
|
; unitorˡ = _
|
|||
|
|
; unitorʳ = _
|
|||
|
|
; associator = _
|
|||
|
|
; unitorˡ-commute = _
|
|||
|
|
; unitorʳ-commute = _
|
|||
|
|
; assoc-commute = _
|
|||
|
|
; triangle = _
|
|||
|
|
; pentagon = _
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
module _ (c : Cartesian (Thin e 𝑃)) where
|
|||
|
|
AllMonadsStrong : Cartesian (Thin e 𝑃) → Monad (Thin e 𝑃) → (H : Monoidal (Thin e 𝑃)) → StrongMonad {C = (Thin e 𝑃)} H
|
|||
|
|
AllMonadsStrong Cart 𝑀 Mon = record
|
|||
|
|
{ M = 𝑀
|
|||
|
|
; strength = record
|
|||
|
|
{ strengthen = ntHelper record
|
|||
|
|
{ η = λ X → {! !}
|
|||
|
|
; commute = _
|
|||
|
|
}
|
|||
|
|
; identityˡ = _
|
|||
|
|
; η-comm = _
|
|||
|
|
; μ-η-comm = _
|
|||
|
|
; strength-assoc = _
|
|||
|
|
}
|
|||
|
|
}
|
|||
|
|
where
|
|||
|
|
open Cartesian Cart
|
|||
|
|
open BinaryProducts products
|
|||
|
|
open Category (Thin _ 𝑃)
|
|||
|
|
open Equiv
|
|||
|
|
open Monad 𝑀
|
|||
|
|
open Functor F
|
|||
|
|
t : ∀ X Y → F₀ X × F₀ Y ⇒ F₀ (X × Y)
|
|||
|
|
t = _
|