Make Rels less strict, add a StrictRels for the previous version

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

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
+  }

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 }
   }

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 }
+  }