From 01844796609246ca24179359e8eae37edd2eaebc Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sat, 5 Nov 2022 09:12:15 +0100 Subject: [PATCH 1/2] Rename Rels to StrictRels Because it's very strict and I'm defining a non-strict version more in keeping with the conventions of the library --- .../Instance/{Rels.agda => StrictRels.agda} | 16 +++++++-------- .../Instance/{Rels.agda => StrictRels.agda} | 6 +++--- .../Instance/{Rels.agda => StrictRels.agda} | 20 +++++++++---------- 3 files changed, 21 insertions(+), 21 deletions(-) rename src/Categories/Category/Dagger/Instance/{Rels.agda => StrictRels.agda} (54%) rename src/Categories/Category/Instance/{Rels.agda => StrictRels.agda} (90%) rename src/Categories/Category/Monoidal/Instance/{Rels.agda => StrictRels.agda} (95%) diff --git a/src/Categories/Category/Dagger/Instance/Rels.agda b/src/Categories/Category/Dagger/Instance/StrictRels.agda similarity index 54% rename from src/Categories/Category/Dagger/Instance/Rels.agda rename to src/Categories/Category/Dagger/Instance/StrictRels.agda index 0d3a54dcf..0d0377149 100644 --- a/src/Categories/Category/Dagger/Instance/Rels.agda +++ b/src/Categories/Category/Dagger/Instance/StrictRels.agda @@ -1,5 +1,5 @@ {-# OPTIONS --without-K --safe #-} -module Categories.Category.Dagger.Instance.Rels where +module Categories.Category.Dagger.Instance.StrictRels where open import Data.Product open import Function @@ -7,10 +7,10 @@ open import Relation.Binary.PropositionalEquality open import Level open import Categories.Category.Dagger -open import Categories.Category.Instance.Rels +open import Categories.Category.Instance.StrictRels -RelsHasDagger : ∀ {o ℓ} → HasDagger (Rels o ℓ) -RelsHasDagger = record +StrictRelsHasDagger : ∀ {o ℓ} → HasDagger (StrictRels o ℓ) +StrictRelsHasDagger = record { _† = flip ; †-identity = (lift ∘ sym ∘ lower) , (lift ∘ sym ∘ lower) ; †-homomorphism = (map₂ swap) , (map₂ swap) @@ -18,8 +18,8 @@ RelsHasDagger = record ; †-involutive = λ _ → id , id } -RelsDagger : ∀ o ℓ → DaggerCategory (suc o) (suc (o ⊔ ℓ)) (o ⊔ ℓ) -RelsDagger o ℓ = record - { C = Rels o ℓ - ; hasDagger = RelsHasDagger +StrictRelsDagger : ∀ o ℓ → DaggerCategory (suc o) (suc (o ⊔ ℓ)) (o ⊔ ℓ) +StrictRelsDagger o ℓ = record + { C = StrictRels o ℓ + ; hasDagger = StrictRelsHasDagger } diff --git a/src/Categories/Category/Instance/Rels.agda b/src/Categories/Category/Instance/StrictRels.agda similarity index 90% rename from src/Categories/Category/Instance/Rels.agda rename to src/Categories/Category/Instance/StrictRels.agda index 667d1f788..cce135c37 100644 --- a/src/Categories/Category/Instance/Rels.agda +++ b/src/Categories/Category/Instance/StrictRels.agda @@ -1,5 +1,5 @@ {-# OPTIONS --without-K --safe #-} -module Categories.Category.Instance.Rels where +module Categories.Category.Instance.StrictRels where open import Data.Product open import Function hiding (_⇔_) @@ -11,8 +11,8 @@ open import Relation.Binary.PropositionalEquality open import Categories.Category.Core -- the category whose objects are sets and whose morphisms are binary relations. -Rels : ∀ o ℓ → Category (suc o) (suc (o ⊔ ℓ)) (o ⊔ ℓ) -Rels o ℓ = record +StrictRels : ∀ o ℓ → Category (suc o) (suc (o ⊔ ℓ)) (o ⊔ ℓ) +StrictRels o ℓ = record { Obj = Set o ; _⇒_ = λ A B → REL A B (o ⊔ ℓ) ; _≈_ = λ L R → L ⇔ R diff --git a/src/Categories/Category/Monoidal/Instance/Rels.agda b/src/Categories/Category/Monoidal/Instance/StrictRels.agda similarity index 95% rename from src/Categories/Category/Monoidal/Instance/Rels.agda rename to src/Categories/Category/Monoidal/Instance/StrictRels.agda index 3f5a7a04e..2d9229e51 100644 --- a/src/Categories/Category/Monoidal/Instance/Rels.agda +++ b/src/Categories/Category/Monoidal/Instance/StrictRels.agda @@ -1,5 +1,5 @@ {-# OPTIONS --without-K --safe #-} -module Categories.Category.Monoidal.Instance.Rels where +module Categories.Category.Monoidal.Instance.StrictRels where -- The category of relations is cartesian and (by self-duality) co-cartesian. -- Perhaps slightly counter-intuitively if you're used to categories which act @@ -20,15 +20,15 @@ open import Categories.Category.Cartesian using (Cartesian) open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal) open import Categories.Category.Core using (Category) open import Categories.Category.Cocartesian using (Cocartesian) -open import Categories.Category.Instance.Rels using (Rels) +open import Categories.Category.Instance.StrictRels using (StrictRels) open import Categories.Category.Monoidal using (Monoidal; monoidalHelper) open import Categories.Category.Monoidal.Symmetric using (Symmetric; symmetricHelper) open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper) module _ {o ℓ} where - Rels-Cartesian : Cartesian (Rels o ℓ) - Rels-Cartesian = record + StrictRels-Cartesian : Cartesian (StrictRels o ℓ) + StrictRels-Cartesian = record { terminal = record { ⊤ = ⊥ ; ⊤-is-terminal = record @@ -57,8 +57,8 @@ module _ {o ℓ} where -- because Rels is dual to itself, the proof that it is cocartesian resembles the proof that it's cartesian -- Rels is not self-dual 'on the nose', so we can't use duality proper. - Rels-Cocartesian : Cocartesian (Rels o ℓ) - Rels-Cocartesian = record + StrictRels-Cocartesian : Cocartesian (StrictRels o ℓ) + StrictRels-Cocartesian = record { initial = record { ⊥ = ⊥ ; ⊥-is-initial = record @@ -84,8 +84,8 @@ module _ {o ℓ} where } } - Rels-Monoidal : Monoidal (Rels o ℓ) - Rels-Monoidal = monoidalHelper _ record + StrictRels-Monoidal : Monoidal (StrictRels o ℓ) + StrictRels-Monoidal = monoidalHelper _ record { ⊗ = record { F₀ = λ { (A , B) → A ×.× B } ; F₁ = λ {(R , S) (a , b) (c , d) → R a c ×.× S b d} @@ -169,8 +169,8 @@ module _ {o ℓ} where } } - Rels-Symmetric : Symmetric Rels-Monoidal - Rels-Symmetric = symmetricHelper _ record + StrictRels-Symmetric : Symmetric StrictRels-Monoidal + StrictRels-Symmetric = symmetricHelper _ record { braiding = niHelper record { η = λ { (X , Y) (x₁ , y₁) (y₂ , x₂) → Lift ℓ (x₁ ≡ x₂) ×.× Lift ℓ (y₁ ≡ y₂) } ; η⁻¹ = λ { (X , Y) (y₁ , x₁) (x₂ , y₂) → Lift ℓ (x₁ ≡ x₂) ×.× Lift ℓ (y₁ ≡ y₂) } From a304ed9e4f7988a4c06f6b53150a21f98eb7b3b6 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Tue, 20 Dec 2022 12:55:26 +0100 Subject: [PATCH 2/2] Add a non-strict version of Rels --- .../Category/Dagger/Instance/Rels.agda | 38 +++ src/Categories/Category/Instance/Rels.agda | 60 ++++ .../Category/Monoidal/Instance/Rels.agda | 284 ++++++++++++++++++ 3 files changed, 382 insertions(+) create mode 100644 src/Categories/Category/Dagger/Instance/Rels.agda create mode 100644 src/Categories/Category/Instance/Rels.agda create mode 100644 src/Categories/Category/Monoidal/Instance/Rels.agda diff --git a/src/Categories/Category/Dagger/Instance/Rels.agda b/src/Categories/Category/Dagger/Instance/Rels.agda new file mode 100644 index 000000000..03528ba54 --- /dev/null +++ b/src/Categories/Category/Dagger/Instance/Rels.agda @@ -0,0 +1,38 @@ +{-# OPTIONS --safe --without-K #-} + +module Categories.Category.Dagger.Instance.Rels where + +open import Categories.Category.Dagger +open import Categories.Category.Instance.Rels + +open import Data.Product +open import Function.Base +open import Level +open import Relation.Binary + +RelsHasDagger : ∀ {o ℓ} → HasDagger (Rels o ℓ) +RelsHasDagger = record + { _† = λ R → record + { fst = flip (proj₁ R) + ; snd = swap (proj₂ R) + } + ; †-identity = λ {A} → record + { fst = λ y≈x → lift (Setoid.sym A (lower y≈x)) + ; snd = λ x≈y → lift (Setoid.sym A (lower x≈y)) + } + ; †-homomorphism = record + { fst = λ { (b , afb , bgc) → b , bgc , afb } + ; snd = λ { (b , bgc , afb) → b , afb , bgc } + } + ; †-resp-≈ = λ f⇔g → record + { fst = proj₁ f⇔g + ; snd = proj₂ f⇔g + } + ; †-involutive = λ _ → id , id + } + +RelsDagger : ∀ o ℓ → DaggerCategory (suc (o ⊔ ℓ)) (suc (o ⊔ ℓ)) (o ⊔ ℓ) +RelsDagger o ℓ = record + { C = Rels o ℓ + ; hasDagger = RelsHasDagger + } diff --git a/src/Categories/Category/Instance/Rels.agda b/src/Categories/Category/Instance/Rels.agda new file mode 100644 index 000000000..5fe263e37 --- /dev/null +++ b/src/Categories/Category/Instance/Rels.agda @@ -0,0 +1,60 @@ +{-# OPTIONS --safe --without-K #-} + +module Categories.Category.Instance.Rels where + +open import Categories.Category +open import Data.Product +open import Function.Base +open import Level +open import Relation.Binary +open import Relation.Binary.Construct.Composition + +Rels : ∀ o ℓ → Category (suc (o ⊔ ℓ)) (suc (o ⊔ ℓ)) (o ⊔ ℓ) +Rels o ℓ = record + { Obj = Setoid o ℓ + ; _⇒_ = λ A B → Σ[ _R_ ∈ REL (Setoid.Carrier A) (Setoid.Carrier B) (o ⊔ ℓ) ] (_R_ Respectsˡ Setoid._≈_ A × _R_ Respectsʳ Setoid._≈_ B) + ; _≈_ = λ f g → proj₁ f ⇔ proj₁ g + ; id = λ {A} → let open Setoid A in record + { fst = λ x y → Lift o (x ≈ y) + ; snd = record + { fst = λ x≈z y≈z → lift (trans (sym x≈z) (lower y≈z)) + ; snd = λ x≈z y≈x → lift (trans (lower y≈x) x≈z) + } + } + ; _∘_ = λ f g → record + { fst = proj₁ g ; proj₁ f + ; snd = record + { fst = λ y≈z y[g;f]x → proj₁ y[g;f]x , proj₁ (proj₂ g) y≈z (proj₁ (proj₂ y[g;f]x)) , proj₂ (proj₂ y[g;f]x) + ; snd = λ y≈z x[g;f]y → proj₁ x[g;f]y , proj₁ (proj₂ x[g;f]y) , proj₂ (proj₂ f) y≈z (proj₂ (proj₂ x[g;f]y)) + } + } + ; assoc = record + { fst = λ { (b , xfb , c , bgc , chy) → c , (b , xfb , bgc) , chy } + ; snd = λ { (c , (b , xfb , bgc) , chy) → b , xfb , c , bgc , chy } + } + ; sym-assoc = record + { fst = λ { (c , (b , xfb , bgc) , chy) → b , xfb , c , bgc , chy } + ; snd = λ { (b , xfb , c , bgc , chy) → c , (b , xfb , bgc) , chy } + } + ; identityˡ = λ {A} {B} {f} → record + { fst = λ af;≈b → proj₂ (proj₂ f) (lower (proj₂ (proj₂ af;≈b))) (proj₁ (proj₂ af;≈b)) + ; snd = λ afb → _ , afb , lift (Setoid.refl B) + } + ; identityʳ = λ {A} {B} {f} → record + { fst = λ a≈;fb → proj₁ (proj₂ f) (Setoid.sym A (lower (proj₁ (proj₂ a≈;fb)))) (proj₂ (proj₂ a≈;fb)) + ; snd = λ afb → _ , lift (Setoid.refl A) , afb + } + ; identity² = λ {A} → record + { fst = λ x≈;≈y → lift (Setoid.trans A (lower (proj₁ (proj₂ x≈;≈y))) (lower (proj₂ (proj₂ x≈;≈y)))) + ; snd = λ x≈y → _ , lift (Setoid.refl A) , x≈y + } + ; equiv = record + { refl = id , id + ; sym = swap + ; trans = λ { (p₁ , p₂) (q₁ , q₂) → (q₁ ∘′ p₁) , (p₂ ∘′ q₂) } + } + ; ∘-resp-≈ = λ f⇔h g⇔i → record + { fst = λ { (b , xgb , bfy) → b , proj₁ g⇔i xgb , proj₁ f⇔h bfy } + ; snd = λ { (b , xib , bhy) → b , proj₂ g⇔i xib , proj₂ f⇔h bhy } + } + } diff --git a/src/Categories/Category/Monoidal/Instance/Rels.agda b/src/Categories/Category/Monoidal/Instance/Rels.agda new file mode 100644 index 000000000..ae149f44f --- /dev/null +++ b/src/Categories/Category/Monoidal/Instance/Rels.agda @@ -0,0 +1,284 @@ +{-# OPTIONS --safe --without-K #-} + +module Categories.Category.Monoidal.Instance.Rels where + +open import Categories.Category.Cartesian using (Cartesian) +open import Categories.Category.Instance.Rels +open import Categories.Category.Monoidal.Core +open import Categories.Category.Monoidal.Symmetric using (Symmetric; symmetricHelper) +open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper) + +open import Data.Empty.Polymorphic using (⊥) +open import Data.Product using (_×_; _,_; proj₁; proj₂) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (×-setoid) +open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′) +open import Data.Sum.Relation.Binary.Pointwise using (⊎-setoid; inj₁; inj₂) +open import Data.Unit.Polymorphic using (⊤) +open import Function.Base using (case_of_) +open import Level using (_⊔_; Lift; lift) +open import Relation.Binary.Bundles using (Setoid) + +module _ {o ℓ} where + + Rels-Cartesian : Cartesian (Rels o (o ⊔ ℓ)) + Rels-Cartesian = record + { terminal = record + { ⊤ = record + { Carrier = ⊥ + ; _≈_ = λ _ _ → ⊤ + } + ; ⊤-is-terminal = record + { ! = λ {A} → record + { fst = λ { _ () } + ; snd = record + { fst = λ { {()} } + ; snd = λ { {_} {()} } + } + } + ; !-unique = λ {A} f → record + { fst = λ { {_} {()} } + ; snd = λ { {_} {()} } + } + } + } + ; products = record + { product = λ {A} {B} → record + { A×B = ⊎-setoid A B + ; π₁ = record + { fst = [ Setoid._≈_ A , (λ _ _ → ⊥) ]′ + ; snd = record + { fst = λ { (inj₁ p) q → Setoid.trans A (Setoid.sym A p) q } + ; snd = λ { {inj₁ _} p q → Setoid.trans A q p } + } + } + ; π₂ = record + { fst = [ (λ _ _ → ⊥) , Setoid._≈_ B ]′ + ; snd = record + { fst = λ { (inj₂ p) q → Setoid.trans B (Setoid.sym B p) q } + ; snd = λ { {inj₂ _} p q → Setoid.trans B q p } + } + } + ; ⟨_,_⟩ = λ L R → record + { fst = λ c → [ proj₁ L c , proj₁ R c ]′ + ; snd = record + { fst = λ + { {inj₁ _} → proj₁ (proj₂ L) + ; {inj₂ _} → proj₁ (proj₂ R) + } + ; snd = λ + { (inj₁ p) → proj₂ (proj₂ L) p + ; (inj₂ p) → proj₂ (proj₂ R) p + } + } + } + ; project₁ = λ {_} {h} {i} → record + { fst = λ { (inj₁ _ , xha , a≈y) → proj₂ (proj₂ h) a≈y xha } + ; snd = λ xhy → inj₁ _ , xhy , Setoid.refl A + } + ; project₂ = λ {C} {h} {i} → record + { fst = λ { (inj₂ a , xia , a≈y) → proj₂ (proj₂ i) a≈y xia } + ; snd = λ xiy → inj₂ _ , xiy , Setoid.refl B + } + ; unique = λ {C} {h} {i} {j} → λ + { (h;π₁⇒i , i⇒h;π₁) (h;π₂⇒j , j⇒h;π₂) → record + { fst = λ + { {x} {inj₁ y} xiy → case i⇒h;π₁ xiy of λ { (inj₁ _ , xhm , m≈y) → proj₂ (proj₂ h) (inj₁ m≈y) xhm } + ; {x} {inj₂ y} xjy → case j⇒h;π₂ xjy of λ { (inj₂ _ , xhm , m≈y) → proj₂ (proj₂ h) (inj₂ m≈y) xhm } + } + ; snd = λ + { {x} {inj₁ y} xhy → h;π₁⇒i (_ , xhy , Setoid.refl A) + ; {x} {inj₂ y} xhy → h;π₂⇒j (_ , xhy , Setoid.refl B) + } + } + } + } + } + } + + Rels-Monoidal : Monoidal (Rels o ℓ) + Rels-Monoidal = monoidalHelper _ record + { ⊗ = record + { F₀ = λ { (A , B) → ×-setoid A B } + ; F₁ = λ + { (R , S) → record + { fst = λ { (a , b) (c , d) → proj₁ R a c × proj₁ S b d } + ; snd = record + { fst = λ { (b≈c , y≈z) (bRa , ySx) → proj₁ (proj₂ R) b≈c bRa , proj₁ (proj₂ S) y≈z ySx } + ; snd = λ { (b≈c , y≈z) (aRb , xSy) → proj₂ (proj₂ R) b≈c aRb , proj₂ (proj₂ S) y≈z xSy } + } + } + } + ; identity = record + { fst = λ { (lift a≈b , lift x≈y) → lift (a≈b , x≈y) } + ; snd = λ { (lift (a≈b , x≈y)) → lift a≈b , lift x≈y } + } + ; homomorphism = record + { fst = λ { ((b , aRb , bTc) , (y , xSy , yUz)) → (b , y) , (aRb , xSy) , (bTc , yUz) } + ; snd = λ { ((b , y) , (aRb , xSy) , (bTc , yUz)) → (b , aRb , bTc) , (y , xSy , yUz) } + } + ; F-resp-≈ = λ + { {A , X} {B , Y} {f , g} {h , i} (f⇔h , g⇔i) → record + { fst = λ { (afb , xgy) → proj₁ f⇔h afb , proj₁ g⇔i xgy } + ; snd = λ { (ahb , xiy) → proj₂ f⇔h ahb , proj₂ g⇔i xiy } + } + } + } + ; unit = record + { Carrier = ⊤ + ; _≈_ = λ _ _ → ⊤ + } + ; unitorˡ = λ {X} → record + { from = record + { fst = λ { (_ , x) y → Lift o (Setoid._≈_ X x y) } + ; snd = record + { fst = λ { (_ , y≈z) (lift y≈x) → lift (Setoid.trans X (Setoid.sym X y≈z) y≈x) } + ; snd = λ { y≈z (lift x≈y) → lift (Setoid.trans X x≈y y≈z) } + } + } + ; to = record + { fst = λ { x (_ , y) → Lift o (Setoid._≈_ X x y) } + ; snd = record + { fst = λ { y≈z (lift y≈x) → lift (Setoid.trans X (Setoid.sym X y≈z) y≈x) } + ; snd = λ { (_ , y≈z) (lift x≈y) → lift (Setoid.trans X x≈y y≈z) } + } + } + ; iso = record + { isoˡ = record + { fst = λ { (_ , lift x≈z , lift z≈y) → lift (_ , Setoid.trans X x≈z z≈y) } + ; snd = λ { (lift (_ , x≈y)) → _ , lift x≈y , lift (Setoid.refl X) } + } + ; isoʳ = record + { fst = λ { (_ , (lift x≈z , lift z≈y)) → lift (Setoid.trans X x≈z z≈y) } + ; snd = λ { (lift x≈y) → _ , lift x≈y , lift (Setoid.refl X) } + } + } + } + ; unitorʳ = λ {X} → record + { from = record + { fst = λ { (x , _) y → Lift o (Setoid._≈_ X x y) } + ; snd = record + { fst = λ { (y≈z , _) (lift y≈x) → lift (Setoid.trans X (Setoid.sym X y≈z) y≈x) } + ; snd = λ { y≈z (lift x≈y) → lift (Setoid.trans X x≈y y≈z) } + } + } + ; to = record + { fst = λ { x (y , _) → Lift o (Setoid._≈_ X x y) } + ; snd = record + { fst = λ { y≈z (lift y≈x) → lift (Setoid.trans X (Setoid.sym X y≈z) y≈x) } + ; snd = λ { (y≈z , _) (lift x≈y) → lift (Setoid.trans X x≈y y≈z) } + } + } + ; iso = record + { isoˡ = record + { fst = λ { (_ , lift x≈z , lift z≈y) → lift (Setoid.trans X x≈z z≈y , _) } + ; snd = λ { (lift (x≈y , _)) → _ , lift x≈y , lift (Setoid.refl X) } + } + ; isoʳ = record + { fst = λ { (_ , lift x≈z , lift z≈y) → lift (Setoid.trans X x≈z z≈y) } + ; snd = λ { (lift x≈y) → _ , lift x≈y , lift (Setoid.refl X) } + } + } + } + ; associator = λ {X} {Y} {Z} → record + { from = record + { fst = λ { ((x , y) , z) (x′ , (y′ , z′)) → Lift o (Setoid._≈_ X x x′ × Setoid._≈_ Y y y′ × Setoid._≈_ Z z z′) } + ; snd = record + { fst = λ { ((x≈x′ , y≈y′) , z≈z′) (lift (x≈x″ , y≈y″ , z≈z″)) → lift (Setoid.trans X (Setoid.sym X x≈x′) x≈x″ , Setoid.trans Y (Setoid.sym Y y≈y′) y≈y″ , Setoid.trans Z (Setoid.sym Z z≈z′) z≈z″) } + ; snd = λ { (x′≈x″ , (y′≈y″ , z′≈z″)) (lift (x≈x′ , y≈y′ , z≈z′)) → lift (Setoid.trans X x≈x′ x′≈x″ , Setoid.trans Y y≈y′ y′≈y″ , Setoid.trans Z z≈z′ z′≈z″) } + } + } + ; to = record + { fst = λ { (x , (y , z)) ((x′ , y′) , z′) → Lift o (Setoid._≈_ X x x′ × Setoid._≈_ Y y y′ × Setoid._≈_ Z z z′) } + ; snd = record + { fst = λ { (x′≈x″ , (y′≈y″ , z′≈z″)) (lift (x′≈x , y′≈y , z′≈z)) → lift (Setoid.trans X (Setoid.sym X x′≈x″) x′≈x , Setoid.trans Y (Setoid.sym Y y′≈y″) y′≈y , Setoid.trans Z (Setoid.sym Z z′≈z″) z′≈z) } + ; snd = λ {xyz} {xyz′} {xyz″} → λ { ((x′≈x″ , y′≈y″) , z′≈z″) (lift (x≈x′ , y≈y′ , z≈z′)) → lift (Setoid.trans X x≈x′ x′≈x″ , Setoid.trans Y y≈y′ y′≈y″ , Setoid.trans Z z≈z′ z′≈z″) } + } + } + ; iso = record + { isoˡ = record + { fst = λ { (_ , (lift (p , q , r) , lift (p′ , q′ , r′))) → lift ((Setoid.trans X p p′ , Setoid.trans Y q q′) , Setoid.trans Z r r′) } + ; snd = λ { (lift ((p , q) , r)) → _ , lift (p , q , r) , lift (Setoid.refl X , Setoid.refl Y , Setoid.refl Z) } + } + ; isoʳ = record + { fst = λ { (_ , (lift (p , q , r) , lift (p′ , q′ , r′))) → lift (Setoid.trans X p p′ , (Setoid.trans Y q q′ , Setoid.trans Z r r′)) } + ; snd = λ { (lift (p , (q , r))) → _ , lift (p , q , r) , lift (Setoid.refl X , Setoid.refl Y , Setoid.refl Z ) } + } + } + } + ; unitorˡ-commute = λ {X} {Y} {R} → record + { fst = λ { (_ , (_ , xRy′) , lift y′≈y) → _ , lift (Setoid.refl X) , proj₂ (proj₂ R) y′≈y xRy′ } + ; snd = λ { (_ , lift x≈x′ , x′Ry) → _ , (_ , proj₁ (proj₂ R) (Setoid.sym X x≈x′) x′Ry) , lift (Setoid.refl Y) } + } + ; unitorʳ-commute = λ {X} {Y} {R} → record + { fst = λ { (_ , (xRy′ , _) , lift y′≈y) → _ , lift (Setoid.refl X) , proj₂ (proj₂ R) y′≈y xRy′ } + ; snd = λ { (_ , lift x≈x′ , x′Ry) → _ , (proj₁ (proj₂ R) (Setoid.sym X x≈x′) x′Ry , _) , lift (Setoid.refl Y) } + } + ; assoc-commute = λ {U} {V} {R} {W} {X} {S} {Y} {Z} {T} → record + { fst = λ { (_ , (((uRv′ , wSx′) , yTz′) , lift (v′≈v , x′≈x , z′≈z))) → _ , lift (Setoid.refl U , Setoid.refl W , Setoid.refl Y) , (proj₂ (proj₂ R) v′≈v uRv′ , (proj₂ (proj₂ S) x′≈x wSx′ , proj₂ (proj₂ T) z′≈z yTz′)) } + ; snd = λ { (_ , lift (u≈u′ , w≈w′ , y≈y′) , (u′Rv , (w′Sx , y′Tz))) → _ , ((proj₁ (proj₂ R) (Setoid.sym U u≈u′) u′Rv , proj₁ (proj₂ S) (Setoid.sym W w≈w′) w′Sx) , proj₁ (proj₂ T) (Setoid.sym Y y≈y′) y′Tz) , lift (Setoid.refl V , Setoid.refl X , Setoid.refl Z) } + } + ; triangle = λ {X} {Y} → record + { fst = λ { (_ , lift (x≈x″ , _ , y≈y″) , lift x″≈x′ , lift y″≈y′) → lift (Setoid.trans X x≈x″ x″≈x′) , lift (Setoid.trans Y y≈y″ y″≈y′) } + ; snd = λ { {(x , _) , y} {x′ , y′} (lift x≈x′ , lift y≈y′) → _ , lift (x≈x′ , _ , y≈y′) , lift (Setoid.refl X) , lift (Setoid.refl Y) } + } + ; pentagon = λ {W} {X} {Y} {Z} → record + { fst = λ + { (_ , (_ , ((lift (w≈w‴ , (x≈x‴ , y≈y‴)) , lift z≈z‴) , lift (w‴≈w″ , ((x‴≈x″ , y‴≈y″) , z‴≈z″)))) , lift w″≈w′ , lift (x″≈x′ , y″≈y′ , z″≈z′)) + → _ , lift ((w≈w‴ , x≈x‴) , (y≈y‴ , z≈z‴)) , lift (Setoid.trans W w‴≈w″ w″≈w′ , (Setoid.trans X x‴≈x″ x″≈x′ , (Setoid.trans Y y‴≈y″ y″≈y′ , Setoid.trans Z z‴≈z″ z″≈z′))) + } + ; snd = λ + { (_ , (lift ((w≈w″ , x≈x″) , (y≈y″ , z≈z″)) , lift (w″≈w′ , (x″≈x′ , (y″≈y′ , z″≈z′))))) + → _ , (_ , ((lift (w≈w″ , x≈x″ , y≈y″) , lift z≈z″) , lift (w″≈w′ , (x″≈x′ , y″≈y′) , z″≈z′))) , lift (Setoid.refl W) , lift (Setoid.refl X , Setoid.refl Y , Setoid.refl Z) + } + } + } + + Rels-Symmetric : Symmetric Rels-Monoidal + Rels-Symmetric = symmetricHelper _ record + { braiding = niHelper record + { η = λ + { (X , Y) → record + { fst = λ { (x₁ , y₁) (y₂ , x₂) → Lift o (Setoid._≈_ X x₁ x₂ × Setoid._≈_ Y y₁ y₂) } + ; snd = record + { fst = λ { (x₂≈x₃ , y₂≈y₃) (lift (x₂≈x₁ , y₂≈y₁)) → lift (Setoid.trans X (Setoid.sym X x₂≈x₃) x₂≈x₁ , Setoid.trans Y (Setoid.sym Y y₂≈y₃) y₂≈y₁) } + ; snd = λ { (y₂≈y₃ , x₂≈x₃) (lift (x₁≈x₂ , y₁≈y₂)) → lift (Setoid.trans X x₁≈x₂ x₂≈x₃ , Setoid.trans Y y₁≈y₂ y₂≈y₃) } + } + } + } + ; η⁻¹ = λ + { (X , Y) → record + { fst = λ { (y₁ , x₁) (x₂ , y₂) → Lift o (Setoid._≈_ X x₁ x₂ × Setoid._≈_ Y y₁ y₂) } + ; snd = record + { fst = λ { (y₂≈y₃ , x₂≈x₃) (lift (x₂≈x₁ , y₂≈y₁)) → lift (Setoid.trans X (Setoid.sym X x₂≈x₃) x₂≈x₁ , Setoid.trans Y (Setoid.sym Y y₂≈y₃) y₂≈y₁) } + ; snd = λ { {y₁ , x₁} {x₂ , y₂} {x₃ , y₃} (x₂≈x₃ , y₂≈y₃) (lift (x₁≈x₂ , y₁≈y₂)) → lift (Setoid.trans X x₁≈x₂ x₂≈x₃ , Setoid.trans Y y₁≈y₂ y₂≈y₃) } + } + } + } + ; commute = λ + { {W , X} {Y , Z} ((R , R-resp-≈) , (S , S-resp-≈)) → record + { fst = λ { ((y₂ , z₂) , (wRy₂ , xSz₂) , lift (y₂≈y₁ , z₂≈z₁)) → _ , lift (Setoid.refl W , Setoid.refl X) , (proj₂ S-resp-≈ z₂≈z₁ xSz₂ , proj₂ R-resp-≈ y₂≈y₁ wRy₂) } + ; snd = λ { ((x₂ , w₂) , lift (w₁≈w₂ , x₁≈x₂) , (x₂Sz , w₂Ry)) → _ , (proj₁ R-resp-≈ (Setoid.sym W w₁≈w₂) w₂Ry , proj₁ S-resp-≈ (Setoid.sym X x₁≈x₂) x₂Sz) , lift (Setoid.refl Y , Setoid.refl Z) } + } + } + ; iso = λ + { (X , Y) → record + { isoˡ = record + { fst = λ { (_ , lift (x₁≈x₃ , y₁≈y₃) , lift (x₃≈x₂ , y₃≈y₂)) → lift (Setoid.trans X x₁≈x₃ x₃≈x₂ , Setoid.trans Y y₁≈y₃ y₃≈y₂) } + ; snd = λ { (lift (x₁≈x₂ , y₁≈y₂)) → _ , lift (x₁≈x₂ , y₁≈y₂) , lift (Setoid.refl X , Setoid.refl Y) } + } + ; isoʳ = record + { fst = λ { (_ , lift (x₁≈x₃ , y₁≈y₃) , lift (x₃≈x₂ , y₃≈y₂)) → lift (Setoid.trans Y y₁≈y₃ y₃≈y₂ , Setoid.trans X x₁≈x₃ x₃≈x₂) } + ; snd = λ { (lift (y₁≈y₂ , x₁≈x₂)) → _ , lift (x₁≈x₂ , y₁≈y₂) , lift (Setoid.refl X , Setoid.refl Y) } + } + } + } + } + ; commutative = λ {X} {Y} → record + { fst = λ { (_ , (lift (y₁≈y₃ , x₁≈x₃) , lift (x₃≈x₂ , y₃≈y₂))) → lift (Setoid.trans Y y₁≈y₃ y₃≈y₂ , Setoid.trans X x₁≈x₃ x₃≈x₂) } + ; snd = λ { (lift (y₁≈y₂ , x₁≈x₂)) → _ , lift (y₁≈y₂ , x₁≈x₂) , lift (Setoid.refl X , Setoid.refl Y) } + } + ; hexagon = λ {X} {Y} {Z} → record + { fst = λ { (_ , (_ , (lift (x₁≈x₄ , y₁≈y₄) , lift z₁≈z₄) , lift (y₄≈y₃ , (x₄≈x₃ , z₄≈z₃))) , (lift y₃≈y₂ , lift (x₃≈x₂ , z₃≈z₂))) → _ , (_ , lift (x₁≈x₄ , (y₁≈y₄ , z₁≈z₄)) , lift (x₄≈x₃ , (y₄≈y₃ , z₄≈z₃))) , lift (y₃≈y₂ , (z₃≈z₂ , x₃≈x₂)) } + ; snd = λ { (_ , (_ , lift (x₁≈x₄ , (y₁≈y₄ , z₁≈z₄)) , lift (x₄≈x₃ , (y₄≈y₃ , z₄≈z₃))) , lift (y₃≈y₂ , (z₃≈z₂ , x₃≈x₂))) → _ , ((_ , ((lift (x₁≈x₄ , y₁≈y₄) , lift z₁≈z₄)) , lift (y₄≈y₃ , (x₄≈x₃ , z₄≈z₃)))) , (lift y₃≈y₂ , lift (x₃≈x₂ , z₃≈z₂)) } + } + }