blob: 703f3be69ee2ee1eb7c61d9813556ecf25ed0ad7 (
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
|
{-# OPTIONS --without-K --safe #-}
module Preorder.Primitive.MonotoneMap.Monoidal.Lax where
open import Level using (Level; _⊔_)
open import Preorder.Primitive.Monoidal using (MonoidalPreorder; SymmetricMonoidalPreorder)
open import Preorder.Primitive.MonotoneMap using (MonotoneMap)
record MonoidalMonotone
{c₁ c₂ ℓ₁ ℓ₂ : Level}
(P : MonoidalPreorder c₁ ℓ₁)
(Q : MonoidalPreorder c₂ ℓ₂)
: Set (c₁ ⊔ c₂ ⊔ ℓ₁ ⊔ ℓ₂) where
private
module P = MonoidalPreorder P
module Q = MonoidalPreorder Q
field
F : MonotoneMap P.U Q.U
open MonotoneMap F public
field
ε : Q.unit Q.≲ map P.unit
⊗-homo : (p₁ p₂ : P.Carrier) → map p₁ Q.⊗ map p₂ Q.≲ map (p₁ P.⊗ p₂)
record SymmetricMonoidalMonotone
{c₁ c₂ ℓ₁ ℓ₂ : Level}
(P : SymmetricMonoidalPreorder c₁ ℓ₁)
(Q : SymmetricMonoidalPreorder c₂ ℓ₂)
: Set (c₁ ⊔ c₂ ⊔ ℓ₁ ⊔ ℓ₂) where
private
module P = SymmetricMonoidalPreorder P
module Q = SymmetricMonoidalPreorder Q
field
monoidalMonotone : MonoidalMonotone P.monoidalPreorder Q.monoidalPreorder
open MonoidalMonotone monoidalMonotone public
|
