diff --git a/src/Categories/Category/Dagger/Instance/Rels.agda b/src/Categories/Category/Dagger/Instance/Rels.agda index 0d3a54dcf..03528ba54 100644 --- a/src/Categories/Category/Dagger/Instance/Rels.agda +++ b/src/Categories/Category/Dagger/Instance/Rels.agda @@ -1,24 +1,37 @@ -{-# OPTIONS --without-K --safe #-} -module Categories.Category.Dagger.Instance.Rels where +{-# OPTIONS --safe --without-K #-} -open import Data.Product -open import Function -open import Relation.Binary.PropositionalEquality -open import Level +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 - { _† = flip - ; †-identity = (lift ∘ sym ∘ lower) , (lift ∘ sym ∘ lower) - ; †-homomorphism = (map₂ swap) , (map₂ swap) - ; †-resp-≈ = λ p → (proj₁ p) , (proj₂ p) -- it's the implicits that need flipped + { _† = λ 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 ℓ → DaggerCategory (suc (o ⊔ ℓ)) (suc (o ⊔ ℓ)) (o ⊔ ℓ) RelsDagger o ℓ = record { C = Rels o ℓ ; hasDagger = RelsHasDagger diff --git a/src/Categories/Category/Dagger/Instance/StrictRels.agda b/src/Categories/Category/Dagger/Instance/StrictRels.agda new file mode 100644 index 000000000..0d0377149 --- /dev/null +++ b/src/Categories/Category/Dagger/Instance/StrictRels.agda @@ -0,0 +1,25 @@ +{-# OPTIONS --without-K --safe #-} +module Categories.Category.Dagger.Instance.StrictRels where + +open import Data.Product +open import Function +open import Relation.Binary.PropositionalEquality +open import Level + +open import Categories.Category.Dagger +open import Categories.Category.Instance.StrictRels + +StrictRelsHasDagger : ∀ {o ℓ} → HasDagger (StrictRels o ℓ) +StrictRelsHasDagger = record + { _† = flip + ; †-identity = (lift ∘ sym ∘ lower) , (lift ∘ sym ∘ lower) + ; †-homomorphism = (map₂ swap) , (map₂ swap) + ; †-resp-≈ = λ p → (proj₁ p) , (proj₂ p) -- it's the implicits that need flipped + ; †-involutive = λ _ → id , id + } + +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/Rels.agda index 667d1f788..5fe263e37 100644 --- a/src/Categories/Category/Instance/Rels.agda +++ b/src/Categories/Category/Instance/Rels.agda @@ -1,36 +1,60 @@ -{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --safe --without-K #-} + module Categories.Category.Instance.Rels where +open import Categories.Category open import Data.Product -open import Function hiding (_⇔_) +open import Function.Base open import Level open import Relation.Binary open import Relation.Binary.Construct.Composition -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 - { Obj = Set o - ; _⇒_ = λ A B → REL A B (o ⊔ ℓ) - ; _≈_ = λ L R → L ⇔ R - ; id = λ x y → Lift ℓ (x ≡ y) - ; _∘_ = λ L R → R ; L - ; assoc = (λ { (b , fxb , c , gbc , hcy) → c , ((b , (fxb , gbc)) , hcy)}) - , λ { (c , (b , fxb , gbc) , hcy) → b , fxb , c , gbc , hcy} - ; sym-assoc = (λ { (c , (b , fxb , gbc) , hcy) → b , fxb , c , gbc , hcy}) - , (λ { (b , fxb , c , gbc , hcy) → c , ((b , (fxb , gbc)) , hcy)}) - ; identityˡ = (λ { (b , fxb , lift refl) → fxb}) , λ {_} {y} fxy → y , fxy , lift refl - ; identityʳ = (λ { (a , lift refl , fxy) → fxy}) , λ {x} {_} fxy → x , lift refl , fxy - ; identity² = (λ { (_ , lift p , lift q) → lift (trans p q)}) , λ { (lift refl) → _ , lift refl , lift refl } +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₂} + ; 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 } } - ; ∘-resp-≈ = λ f⇔h g⇔i → - (λ { (b , gxb , fky) → b , proj₁ g⇔i gxb , proj₁ f⇔h fky }) , - λ { (b , ixb , hby) → b , proj₂ g⇔i ixb , proj₂ f⇔h hby } } diff --git a/src/Categories/Category/Instance/StrictRels.agda b/src/Categories/Category/Instance/StrictRels.agda new file mode 100644 index 000000000..cce135c37 --- /dev/null +++ b/src/Categories/Category/Instance/StrictRels.agda @@ -0,0 +1,36 @@ +{-# OPTIONS --without-K --safe #-} +module Categories.Category.Instance.StrictRels where + +open import Data.Product +open import Function hiding (_⇔_) +open import Level +open import Relation.Binary +open import Relation.Binary.Construct.Composition +open import Relation.Binary.PropositionalEquality + +open import Categories.Category.Core + +-- the category whose objects are sets and whose morphisms are binary relations. +StrictRels : ∀ o ℓ → Category (suc o) (suc (o ⊔ ℓ)) (o ⊔ ℓ) +StrictRels o ℓ = record + { Obj = Set o + ; _⇒_ = λ A B → REL A B (o ⊔ ℓ) + ; _≈_ = λ L R → L ⇔ R + ; id = λ x y → Lift ℓ (x ≡ y) + ; _∘_ = λ L R → R ; L + ; assoc = (λ { (b , fxb , c , gbc , hcy) → c , ((b , (fxb , gbc)) , hcy)}) + , λ { (c , (b , fxb , gbc) , hcy) → b , fxb , c , gbc , hcy} + ; sym-assoc = (λ { (c , (b , fxb , gbc) , hcy) → b , fxb , c , gbc , hcy}) + , (λ { (b , fxb , c , gbc , hcy) → c , ((b , (fxb , gbc)) , hcy)}) + ; identityˡ = (λ { (b , fxb , lift refl) → fxb}) , λ {_} {y} fxy → y , fxy , lift refl + ; identityʳ = (λ { (a , lift refl , fxy) → fxy}) , λ {x} {_} fxy → x , lift refl , fxy + ; identity² = (λ { (_ , lift p , lift q) → lift (trans p q)}) , λ { (lift refl) → _ , lift refl , lift refl } + ; equiv = record + { refl = id , id + ; sym = swap + ; trans = λ { (p₁ , p₂) (q₁ , q₂) → (q₁ ∘′ p₁) , p₂ ∘′ q₂} + } + ; ∘-resp-≈ = λ f⇔h g⇔i → + (λ { (b , gxb , fky) → b , proj₁ g⇔i gxb , proj₁ f⇔h fky }) , + λ { (b , ixb , hby) → b , proj₂ g⇔i ixb , proj₂ f⇔h hby } + } diff --git a/src/Categories/Category/Monoidal/Instance/Rels.agda b/src/Categories/Category/Monoidal/Instance/Rels.agda index 3f5a7a04e..ae149f44f 100644 --- a/src/Categories/Category/Monoidal/Instance/Rels.agda +++ b/src/Categories/Category/Monoidal/Instance/Rels.agda @@ -1,85 +1,96 @@ -{-# OPTIONS --without-K --safe #-} -module Categories.Category.Monoidal.Instance.Rels 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 --- like Sets, the product acts on objects as the disjoint union. --- It also exhibits another monoidality, based on cartesian products of sets, --- which is symmetric and closed. +{-# OPTIONS --safe --without-K #-} -open import Data.Empty.Polymorphic using (⊥; ⊥-elim) -import Data.Product as × -open × using (_,_) -open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′) -open import Data.Unit.Polymorphic using (⊤) -open import Function using (case_of_; flip) -open import Level using (Lift; lift) -open import Relation.Binary.PropositionalEquality using (_≡_; refl) +module Categories.Category.Monoidal.Instance.Rels where 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.Monoidal using (Monoidal; monoidalHelper) +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 ℓ) + Rels-Cartesian : Cartesian (Rels o (o ⊔ ℓ)) Rels-Cartesian = record { terminal = record - { ⊤ = ⊥ + { ⊤ = record + { Carrier = ⊥ + ; _≈_ = λ _ _ → ⊤ + } ; ⊤-is-terminal = record - { ! = λ { _ (lift ()) } - ; !-unique = λ _ → (λ { {_} {lift ()} }) , (λ { {_} {lift ()} }) + { ! = λ {A} → record + { fst = λ { _ () } + ; snd = record + { fst = λ { {()} } + ; snd = λ { {_} {()} } + } + } + ; !-unique = λ {A} f → record + { fst = λ { {_} {()} } + ; snd = λ { {_} {()} } + } } } ; products = record { product = λ {A} {B} → record - { A×B = A ⊎ B - ; π₁ = [ (λ x y → Lift ℓ (x ≡ y) ) , (λ _ _ → ⊥) ]′ - ; π₂ = [ (λ _ _ → ⊥) , (λ x y → Lift ℓ (x ≡ y)) ]′ - ; ⟨_,_⟩ = λ L R c → [ L c , R c ]′ - ; project₁ = (λ { (inj₁ x , r , lift refl) → r}) - , λ r → inj₁ _ , r , lift refl - ; project₂ = (λ { (inj₂ _ , r , lift refl) → r }) - , (λ r → inj₂ _ , r , lift refl) - ; unique = - λ { (p , q) (p′ , q′) → (λ { {_} {inj₁ a} r → case (q {_} {a} r) of λ { (inj₁ .a , s , lift refl) → s} - ; {_} {inj₂ b} r → case (q′ {_} {b} r) of λ { (inj₂ .b , s , lift refl) → s} }) - , λ { {_} {inj₁ a} hxa → p (inj₁ a , hxa , lift refl) - ; {_} {inj₂ b} hxb → p′ (inj₂ b , hxb , lift refl) } } - } - } - } - - -- 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 - { initial = record - { ⊥ = ⊥ - ; ⊥-is-initial = record - { ! = λ () - ; !-unique = λ _ → (λ { {()} }) , (λ { {()} }) - } - } - ; coproducts = record - { coproduct = λ {A} {B} → record - { A+B = A ⊎ B - ; i₁ = λ a → [ (λ a′ → Lift ℓ (a ≡ a′)) , (λ _ → ⊥) ]′ - ; i₂ = λ b → [ (λ _ → ⊥) , (λ b′ → Lift ℓ (b ≡ b′)) ]′ - ; [_,_] = λ L R a+b c → [ flip L c , flip R c ]′ a+b - ; inject₁ = (λ { (inj₁ x , lift refl , fxy) → fxy}) - , λ r → inj₁ _ , lift refl , r - ; inject₂ = (λ { (inj₂ _ , lift refl , r) → r }) - , (λ r → inj₂ _ , lift refl , r) - ; unique = λ { (p , q) (p′ , q′) → (λ { {inj₁ a} r → case (q {a} r) of λ { (inj₁ .a , lift refl , s) → s} - ; {inj₂ b} r → case (q′ {b} r) of λ { (inj₂ .b , lift refl , s) → s} }) - , λ { {inj₁ a} hxa → p (inj₁ a , lift refl , hxa) - ; {inj₂ b} hxb → p′ (inj₂ b , lift refl , hxb) } } + { 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) + } + } + } } } } @@ -87,118 +98,187 @@ module _ {o ℓ} where Rels-Monoidal : Monoidal (Rels o ℓ) Rels-Monoidal = monoidalHelper _ record { ⊗ = record - { F₀ = λ { (A , B) → A ×.× B } - ; F₁ = λ {(R , S) (a , b) (c , d) → R a c ×.× S b d} + { 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 refl , lift refl) → lift refl } - ; snd = λ { (lift refl) → lift refl , lift refl } + { 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-≈ = λ - { ((R⇒T , T⇒R) , (S⇒U , U⇒S)) → record - { fst = λ { (aRb , xSy) → R⇒T aRb , S⇒U xSy } - ; snd = λ { (aTb , xUy) → T⇒R aTb , U⇒S xUy } + { {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 = ⊤ - ; unitorˡ = record - { from = λ { (_ , x) y → Lift ℓ (x ≡ y) } - ; to = λ { x (_ , y) → Lift ℓ (x ≡ y) } + ; 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 refl , lift refl)) → lift refl } - ; snd = λ { (lift refl) → _ , (lift refl , lift refl) } + { 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 refl , lift refl)) → lift refl } - ; snd = λ { (lift refl) → (_ , (lift refl , lift refl)) } + { 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ʳ = record - { from = λ { (x , _) y → Lift ℓ (x ≡ y) } - ; to = λ { x (y , _) → Lift ℓ (x ≡ y) } + ; 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 refl , lift refl)) → lift refl } - ; snd = λ { (lift refl) → _ , (lift refl , lift refl) } + { 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 refl , lift refl)) → lift refl } - ; snd = λ { (lift refl) → _ , (lift refl , lift refl) } + { 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 = record - { from = λ { ((x₁ , y₁) , z₁) (x₂ , (y₂ , z₂)) → Lift ℓ (x₁ ≡ x₂) ×.× Lift ℓ (y₁ ≡ y₂) ×.× Lift ℓ (z₁ ≡ z₂) } - ; to = λ { (x₁ , (y₁ , z₁)) ((x₂ , y₂) , z₂) → Lift ℓ (x₁ ≡ x₂) ×.× Lift ℓ (y₁ ≡ y₂) ×.× Lift ℓ (z₁ ≡ z₂) } + ; 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 refl , lift refl , lift refl) , (lift refl , lift refl , lift refl))) → lift refl } - ; snd = λ { (lift refl) → _ , ((lift refl , lift refl , lift refl) , (lift refl , lift refl , lift refl)) } + { 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 refl , lift refl , lift refl) , (lift refl , lift refl , lift refl))) → lift refl } - ; snd = λ { (lift refl) → _ , ((lift refl , lift refl , lift refl) , (lift refl , lift refl , lift refl)) } + { 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 = record - { fst = λ { (_ , ((lift refl , x) , lift refl)) → _ , (lift refl , x) } - ; snd = λ { (_ , (lift refl , x)) → _ , ((lift refl , x) , lift refl) } + ; 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 = record - { fst = λ { (_ , ((x , lift refl) , lift refl)) → _ , (lift refl , x) } - ; snd = λ { (_ , (lift refl , x)) → _ , ((x , lift refl) , lift refl) } + ; 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 = record - { fst = λ { (_ , ((a , b) , c) , (lift refl , lift refl , lift refl)) → _ , (lift refl , lift refl , lift refl) , (a , (b , c)) } - ; snd = λ { (_ , (lift refl , lift refl , lift refl) , (a , (b , c))) → _ , ((a , b) , c) , (lift refl , lift refl , lift refl) } + ; 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 = record - { fst = λ { (_ , ((lift refl , lift refl , lift refl) , (lift refl , lift refl))) → lift refl , lift refl } - ; snd = λ { (lift refl , lift refl) → _ , ((lift refl , lift refl , lift refl) , (lift refl , lift refl)) } + ; 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 = record - { fst = λ { (_ , ((_ , (((lift refl , lift refl , lift refl) , lift refl) , (lift refl , lift refl , lift refl))) , (lift refl , (lift refl , lift refl , lift refl)))) → _ , (lift refl , lift refl , lift refl) , (lift refl , lift refl , lift refl) } - ; snd = λ { (_ , (lift refl , lift refl , lift refl) , (lift refl , lift refl , lift refl)) → _ , ((_ , (((lift refl , lift refl , lift refl) , lift refl) , (lift refl , lift refl , lift refl))) , (lift refl , (lift refl , lift refl , lift refl))) } + ; 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) (x₁ , y₁) (y₂ , x₂) → Lift ℓ (x₁ ≡ x₂) ×.× Lift ℓ (y₁ ≡ y₂) } - ; η⁻¹ = λ { (X , Y) (y₁ , x₁) (x₂ , y₂) → Lift ℓ (x₁ ≡ x₂) ×.× Lift ℓ (y₁ ≡ y₂) } + { η = λ + { (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 = λ - { (R , S) → record - { fst = λ { (_ , (r , s) , (lift refl , lift refl)) → _ , (lift refl , lift refl) , (s , r) } - ; snd = λ { (_ , (lift refl , lift refl) , (s , r)) → _ , (r , s) , (lift refl , lift refl) } + { {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 refl , lift refl) , (lift refl , lift refl)) → lift refl } - ; snd = λ { (lift refl) → _ , (lift refl , lift refl) , (lift refl , lift refl) } + { 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 refl , lift refl) , (lift refl , lift refl)) → lift refl } - ; snd = λ { (lift refl) → _ , (lift refl , lift refl) , (lift refl , lift refl) } + { 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 = record - { fst = λ { (_ , (lift refl , lift refl) , (lift refl , lift refl)) → lift refl } - ; snd = λ { (lift refl) → _ , (lift refl , lift refl) , (lift refl , lift refl) } + ; 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 = record - { fst = λ { (_ , (_ , ((lift refl , lift refl) , lift refl) , (lift refl , (lift refl , lift refl))) , (lift refl , lift refl , lift refl)) → _ , (_ , (lift refl , lift refl , lift refl) , (lift refl , lift refl)) , lift refl , lift refl , lift refl } - ; snd = λ { (_ , (_ , (lift refl , lift refl , lift refl) , lift refl , lift refl) , lift refl , lift refl , lift refl) → _ , (_ , ((lift refl , lift refl) , lift refl) , lift refl , lift refl , lift refl) , lift refl , lift refl , lift refl } + ; 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₂)) } } } diff --git a/src/Categories/Category/Monoidal/Instance/StrictRels.agda b/src/Categories/Category/Monoidal/Instance/StrictRels.agda new file mode 100644 index 000000000..2d9229e51 --- /dev/null +++ b/src/Categories/Category/Monoidal/Instance/StrictRels.agda @@ -0,0 +1,204 @@ +{-# OPTIONS --without-K --safe #-} +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 +-- like Sets, the product acts on objects as the disjoint union. +-- It also exhibits another monoidality, based on cartesian products of sets, +-- which is symmetric and closed. + +open import Data.Empty.Polymorphic using (⊥; ⊥-elim) +import Data.Product as × +open × using (_,_) +open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′) +open import Data.Unit.Polymorphic using (⊤) +open import Function using (case_of_; flip) +open import Level using (Lift; lift) +open import Relation.Binary.PropositionalEquality using (_≡_; refl) + +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.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 + + StrictRels-Cartesian : Cartesian (StrictRels o ℓ) + StrictRels-Cartesian = record + { terminal = record + { ⊤ = ⊥ + ; ⊤-is-terminal = record + { ! = λ { _ (lift ()) } + ; !-unique = λ _ → (λ { {_} {lift ()} }) , (λ { {_} {lift ()} }) + } + } + ; products = record + { product = λ {A} {B} → record + { A×B = A ⊎ B + ; π₁ = [ (λ x y → Lift ℓ (x ≡ y) ) , (λ _ _ → ⊥) ]′ + ; π₂ = [ (λ _ _ → ⊥) , (λ x y → Lift ℓ (x ≡ y)) ]′ + ; ⟨_,_⟩ = λ L R c → [ L c , R c ]′ + ; project₁ = (λ { (inj₁ x , r , lift refl) → r}) + , λ r → inj₁ _ , r , lift refl + ; project₂ = (λ { (inj₂ _ , r , lift refl) → r }) + , (λ r → inj₂ _ , r , lift refl) + ; unique = + λ { (p , q) (p′ , q′) → (λ { {_} {inj₁ a} r → case (q {_} {a} r) of λ { (inj₁ .a , s , lift refl) → s} + ; {_} {inj₂ b} r → case (q′ {_} {b} r) of λ { (inj₂ .b , s , lift refl) → s} }) + , λ { {_} {inj₁ a} hxa → p (inj₁ a , hxa , lift refl) + ; {_} {inj₂ b} hxb → p′ (inj₂ b , hxb , lift refl) } } + } + } + } + + -- 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. + StrictRels-Cocartesian : Cocartesian (StrictRels o ℓ) + StrictRels-Cocartesian = record + { initial = record + { ⊥ = ⊥ + ; ⊥-is-initial = record + { ! = λ () + ; !-unique = λ _ → (λ { {()} }) , (λ { {()} }) + } + } + ; coproducts = record + { coproduct = λ {A} {B} → record + { A+B = A ⊎ B + ; i₁ = λ a → [ (λ a′ → Lift ℓ (a ≡ a′)) , (λ _ → ⊥) ]′ + ; i₂ = λ b → [ (λ _ → ⊥) , (λ b′ → Lift ℓ (b ≡ b′)) ]′ + ; [_,_] = λ L R a+b c → [ flip L c , flip R c ]′ a+b + ; inject₁ = (λ { (inj₁ x , lift refl , fxy) → fxy}) + , λ r → inj₁ _ , lift refl , r + ; inject₂ = (λ { (inj₂ _ , lift refl , r) → r }) + , (λ r → inj₂ _ , lift refl , r) + ; unique = λ { (p , q) (p′ , q′) → (λ { {inj₁ a} r → case (q {a} r) of λ { (inj₁ .a , lift refl , s) → s} + ; {inj₂ b} r → case (q′ {b} r) of λ { (inj₂ .b , lift refl , s) → s} }) + , λ { {inj₁ a} hxa → p (inj₁ a , lift refl , hxa) + ; {inj₂ b} hxb → p′ (inj₂ b , lift refl , hxb) } } + } + } + } + + 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} + ; identity = record + { fst = λ { (lift refl , lift refl) → lift refl } + ; snd = λ { (lift refl) → lift refl , lift refl } + } + ; 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-≈ = λ + { ((R⇒T , T⇒R) , (S⇒U , U⇒S)) → record + { fst = λ { (aRb , xSy) → R⇒T aRb , S⇒U xSy } + ; snd = λ { (aTb , xUy) → T⇒R aTb , U⇒S xUy } + } + } + } + ; unit = ⊤ + ; unitorˡ = record + { from = λ { (_ , x) y → Lift ℓ (x ≡ y) } + ; to = λ { x (_ , y) → Lift ℓ (x ≡ y) } + ; iso = record + { isoˡ = record + { fst = λ { (_ , (lift refl , lift refl)) → lift refl } + ; snd = λ { (lift refl) → _ , (lift refl , lift refl) } + } + ; isoʳ = record + { fst = λ { (_ , (lift refl , lift refl)) → lift refl } + ; snd = λ { (lift refl) → (_ , (lift refl , lift refl)) } + } + } + } + ; unitorʳ = record + { from = λ { (x , _) y → Lift ℓ (x ≡ y) } + ; to = λ { x (y , _) → Lift ℓ (x ≡ y) } + ; iso = record + { isoˡ = record + { fst = λ { (_ , (lift refl , lift refl)) → lift refl } + ; snd = λ { (lift refl) → _ , (lift refl , lift refl) } + } + ; isoʳ = record + { fst = λ { (_ , (lift refl , lift refl)) → lift refl } + ; snd = λ { (lift refl) → _ , (lift refl , lift refl) } + } + } + } + ; associator = record + { from = λ { ((x₁ , y₁) , z₁) (x₂ , (y₂ , z₂)) → Lift ℓ (x₁ ≡ x₂) ×.× Lift ℓ (y₁ ≡ y₂) ×.× Lift ℓ (z₁ ≡ z₂) } + ; to = λ { (x₁ , (y₁ , z₁)) ((x₂ , y₂) , z₂) → Lift ℓ (x₁ ≡ x₂) ×.× Lift ℓ (y₁ ≡ y₂) ×.× Lift ℓ (z₁ ≡ z₂) } + ; iso = record + { isoˡ = record + { fst = λ { (_ , ((lift refl , lift refl , lift refl) , (lift refl , lift refl , lift refl))) → lift refl } + ; snd = λ { (lift refl) → _ , ((lift refl , lift refl , lift refl) , (lift refl , lift refl , lift refl)) } + } + ; isoʳ = record + { fst = λ { (_ , ((lift refl , lift refl , lift refl) , (lift refl , lift refl , lift refl))) → lift refl } + ; snd = λ { (lift refl) → _ , ((lift refl , lift refl , lift refl) , (lift refl , lift refl , lift refl)) } + } + } + } + ; unitorˡ-commute = record + { fst = λ { (_ , ((lift refl , x) , lift refl)) → _ , (lift refl , x) } + ; snd = λ { (_ , (lift refl , x)) → _ , ((lift refl , x) , lift refl) } + } + ; unitorʳ-commute = record + { fst = λ { (_ , ((x , lift refl) , lift refl)) → _ , (lift refl , x) } + ; snd = λ { (_ , (lift refl , x)) → _ , ((x , lift refl) , lift refl) } + } + ; assoc-commute = record + { fst = λ { (_ , ((a , b) , c) , (lift refl , lift refl , lift refl)) → _ , (lift refl , lift refl , lift refl) , (a , (b , c)) } + ; snd = λ { (_ , (lift refl , lift refl , lift refl) , (a , (b , c))) → _ , ((a , b) , c) , (lift refl , lift refl , lift refl) } + } + ; triangle = record + { fst = λ { (_ , ((lift refl , lift refl , lift refl) , (lift refl , lift refl))) → lift refl , lift refl } + ; snd = λ { (lift refl , lift refl) → _ , ((lift refl , lift refl , lift refl) , (lift refl , lift refl)) } + } + ; pentagon = record + { fst = λ { (_ , ((_ , (((lift refl , lift refl , lift refl) , lift refl) , (lift refl , lift refl , lift refl))) , (lift refl , (lift refl , lift refl , lift refl)))) → _ , (lift refl , lift refl , lift refl) , (lift refl , lift refl , lift refl) } + ; snd = λ { (_ , (lift refl , lift refl , lift refl) , (lift refl , lift refl , lift refl)) → _ , ((_ , (((lift refl , lift refl , lift refl) , lift refl) , (lift refl , lift refl , lift refl))) , (lift refl , (lift refl , lift refl , lift refl))) } + } + } + + 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₂) } + ; commute = λ + { (R , S) → record + { fst = λ { (_ , (r , s) , (lift refl , lift refl)) → _ , (lift refl , lift refl) , (s , r) } + ; snd = λ { (_ , (lift refl , lift refl) , (s , r)) → _ , (r , s) , (lift refl , lift refl) } + } + } + ; iso = λ + { (X , Y) → record + { isoˡ = record + { fst = λ { (_ , (lift refl , lift refl) , (lift refl , lift refl)) → lift refl } + ; snd = λ { (lift refl) → _ , (lift refl , lift refl) , (lift refl , lift refl) } + } + ; isoʳ = record + { fst = λ { (_ , (lift refl , lift refl) , (lift refl , lift refl)) → lift refl } + ; snd = λ { (lift refl) → _ , (lift refl , lift refl) , (lift refl , lift refl) } + } + } + } + } + ; commutative = record + { fst = λ { (_ , (lift refl , lift refl) , (lift refl , lift refl)) → lift refl } + ; snd = λ { (lift refl) → _ , (lift refl , lift refl) , (lift refl , lift refl) } + } + ; hexagon = record + { fst = λ { (_ , (_ , ((lift refl , lift refl) , lift refl) , (lift refl , (lift refl , lift refl))) , (lift refl , lift refl , lift refl)) → _ , (_ , (lift refl , lift refl , lift refl) , (lift refl , lift refl)) , lift refl , lift refl , lift refl } + ; snd = λ { (_ , (_ , (lift refl , lift refl , lift refl) , lift refl , lift refl) , lift refl , lift refl , lift refl) → _ , (_ , ((lift refl , lift refl) , lift refl) , lift refl , lift refl , lift refl) , lift refl , lift refl , lift refl } + } + }