Setoid instances

src/Felix/All.agda

@@ -20,4 +20,6 @@ import Felix.Construct.Comma
 import Felix.Construct.Arrow
 
 import Felix.Instances.Function
+import Felix.Instances.Function.Lift
 import Felix.Instances.Identity
+import Felix.Instances.Setoid

src/Felix/Instances/Function/Lift.agda

@@ -7,7 +7,7 @@ module Felix.Instances.Function.Lift (a b : Level) where
 open Lift
 open import Data.Product using (_,_)
 
-open import Felix.Homomorphism hiding (refl)
+open import Felix.Homomorphism
 open import Felix.Object
 
 private module F {ℓ} where open import Felix.Instances.Function ℓ public
@@ -17,8 +17,8 @@ private
   variable
     A : Set a
 
-lift₀ : ⦃ _ : Products (Set (a ⊔ b)) ⦄ → A → (⊤ F.⇾ Lift b A)
-lift₀ n tt = lift n
+lift₀ : A → (⊤ F.⇾ Lift b A)
+lift₀ a tt = lift a
 
 lift₁ : (A F.⇾ A) → (Lift b A F.⇾ Lift b A)
 lift₁ f (lift a) = lift (f a)

src/Felix/Instances/Setoid.agda

@@ -0,0 +1,5 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Felix.Instances.Setoid where
+
+open import Felix.Instances.Setoid.Laws public

src/Felix/Instances/Setoid/Laws.agda

@@ -0,0 +1,77 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Felix.Instances.Setoid.Laws where
+
+open import Data.Product using (_,_; <_,_>; curry; uncurry)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Data.Sum using (inj₁; inj₂)
+open import Data.Sum.Relation.Binary.Pointwise using (_⊎ₛ_)
+open import Data.Unit.Polymorphic using (tt)
+open import Function using (_∘_; _∘₂_; mk⇔)
+open import Level using (_⊔_)
+open import Relation.Binary using (Setoid)
+
+open import Felix.Equiv using (Equivalent)
+open import Felix.Raw as Raw
+  hiding (Category; Cartesian; CartesianClosed; Distributive; _∘_; curry; uncurry)
+open import Felix.Laws using (Category; Cartesian; CartesianClosed; Distributive)
+
+open import Felix.Instances.Setoid.Raw public
+
+module setoid-laws-instances where instance
+
+  category : ∀ {c ℓ} → Category {obj = Setoid c ℓ} _⟶_
+  category = record
+    { identityˡ = λ {_} {B} _ → Setoid.refl B
+    ; identityʳ = λ {_} {B} _ → Setoid.refl B
+    ; assoc = λ {_} {_} {_} {D} _ → Setoid.refl D
+    ; ∘≈ = λ { {_} {_} {C} {f = f} {k = k} h≈k f≈g x →
+      Setoid.trans C (h≈k (f ⟨$⟩ x)) (cong k (f≈g x)) }
+    }
+
+  cartesian : ∀ {c ℓ} → Cartesian {obj = Setoid c ℓ} _⟶_
+  cartesian {c} {ℓ} = record
+    -- ! in category of function and types
+    { ∀⊤ = λ _ → tt
+    ; ∀× = λ {A} {B} {C} → mk⇔
+      < cong (exl {a = B} {b = C}) ∘_
+      , cong (exr {a = B} {b = C}) ∘_
+      >
+      (uncurry <_,_>)
+    -- this is _▵_ in category of functions and types,
+    -- but I have trouble hinting to agda what Level it should use
+    ; ▵≈ = <_,_>
+    }
+
+  distributive :
+    ∀ {c ℓ} →
+    Distributive
+      ⦃ products {c} {c ⊔ ℓ} ⦄ ⦃ coproducts {c} {ℓ} ⦄
+      _⟶_
+      ⦃ raw = setoid-raw-instances.distributive {c} {ℓ} ⦄
+  distributive = record
+    { distribˡ∘distribˡ⁻¹ = λ where
+      {A} {B} {C} (_ , inj₁ _) → Setoid.refl (A ×ₛ (B ⊎ₛ C))
+      {A} {B} {C} (_ , inj₂ _) → Setoid.refl (A ×ₛ (B ⊎ₛ C))
+    ; distribˡ⁻¹∘distribˡ = λ where
+      {A} {B} {C} (inj₁ _) → Setoid.refl ((A ×ₛ B) ⊎ₛ (A ×ₛ C))
+      {A} {B} {C} (inj₂ _) → Setoid.refl ((A ×ₛ B) ⊎ₛ (A ×ₛ C))
+    ; distribʳ∘distribʳ⁻¹ = λ where
+      {A} {B} {C} (inj₁ _ , _) → Setoid.refl ((B ⊎ₛ C) ×ₛ A)
+      {A} {B} {C} (inj₂ _ , _) → Setoid.refl ((B ⊎ₛ C) ×ₛ A)
+    ; distribʳ⁻¹∘distribʳ = λ where
+      {A} {B} {C} (inj₁ _) → Setoid.refl ((B ×ₛ A) ⊎ₛ (C ×ₛ A))
+      {A} {B} {C} (inj₂ _) → Setoid.refl ((B ×ₛ A) ⊎ₛ (C ×ₛ A))
+    }
+
+  cartesianClosed :
+    ∀ {c ℓ} →
+    CartesianClosed
+      ⦃ products {c ⊔ ℓ} {c ⊔ ℓ} ⦄ ⦃ exponentials {c} {ℓ} ⦄ _⟶_
+      ⦃ raw = setoid-raw-instances.cartesianClosed {c} {ℓ} ⦄
+  cartesianClosed = record
+    { ∀⇛ = λ {_} {_} {C} → mk⇔
+      (λ g≈curry-f → Setoid.sym C ∘ uncurry g≈curry-f)
+      (λ f≈uncurry-g → Setoid.sym C ∘₂ curry f≈uncurry-g)
+    ; curry≈ = curry
+    }

src/Felix/Instances/Setoid/Raw.agda

@@ -0,0 +1,109 @@
+{-# OPTIONS --safe --without-K  #-}
+
+module Felix.Instances.Setoid.Raw where
+
+open import Data.Product using (_,_; _,′_; curry′; uncurry′; ∃₂; proj₁; proj₂)
+open import Data.Product.Function.NonDependent.Setoid using (<_,_>ₛ; proj₁ₛ; proj₂ₛ)
+open import Data.Sum using ([_,_]; inj₁; inj₂)
+open import Data.Sum.Function.Setoid using ([_,_]ₛ; inj₁ₛ; inj₂ₛ)
+open import Data.Sum.Relation.Binary.Pointwise using (inj₁; inj₂)
+open import Data.Unit.Polymorphic using (tt)
+open import Function using (Func) renaming (_∘_ to _∘ᵈ_)
+open import Function.Construct.Composition as Comp
+open import Function.Construct.Constant as Const
+open import Function.Construct.Identity as Id
+open import Level using (_⊔_; suc)
+open import Relation.Binary using (Setoid)
+
+open import Function.Construct.Setoid using (setoid)
+open import Felix.Equiv using (Equivalent)
+open import Felix.Raw
+open import Felix.Instances.Setoid.Type
+  using (module setoid-instances; _⟶_; cong; _⟨$⟩_) public
+
+import Felix.Instances.Function as Fun
+
+open setoid-instances public
+
+module setoid-raw-instances where instance
+
+  equivalent : ∀ {c ℓ} → Equivalent (c ⊔ ℓ) {obj = Setoid c ℓ} _⟶_
+  equivalent = record
+    { _≈_ = λ {From} {To} → Setoid._≈_ (setoid From To)
+    ; equiv = λ {From} {To} → Setoid.isEquivalence (setoid From To)
+    }
+
+  category : ∀ {c ℓ} → Category {obj = Setoid c ℓ} _⟶_
+  category = record
+    { id = Id.function _
+    -- flip′ Comp.function doesn't reduce in goals
+    ; _∘_ = λ g f → Comp.function f g
+    }
+
+  cartesian : ∀ {c ℓ} → Cartesian {obj = Setoid c ℓ} _⟶_
+  cartesian = record
+    { ! = Const.function _ ⊤ tt
+    ; _▵_ = <_,_>ₛ
+    ; exl = proj₁ₛ
+    ; exr = proj₂ₛ
+    }
+
+  cocartesian : ∀ {c ℓ} → Cocartesian ⦃ coproducts {c} {ℓ} ⦄ _⟶_
+  cocartesian = record
+    { ¡ = record
+      { to = λ { () }
+      ; cong = λ { {()} }
+      }
+    ; _▿_ = [_,_]ₛ
+    ; inl = inj₁ₛ
+    ; inr = inj₂ₛ
+    }
+
+  distributive :
+    ∀ {c ℓ} →
+    Distributive
+      ⦃ products {c} {c ⊔ ℓ} ⦄ ⦃ coproducts {c} {ℓ} ⦄
+      _⟶_
+      ⦃ category {c} {c ⊔ ℓ} ⦄ ⦃ cartesian {c} {c ⊔ ℓ} ⦄ ⦃ cocartesian {c} {ℓ} ⦄
+  distributive {c} {ℓ} = let open Fun c in record
+    { distribˡ⁻¹ = record
+      { to = distribˡ⁻¹
+      ; cong = λ where
+        (a₁≈a₂ , inj₁ b₁≈b₂) → inj₁ (a₁≈a₂ , b₁≈b₂)
+        (a₁≈a₂ , inj₂ c₁≈c₂) → inj₂ (a₁≈a₂ , c₁≈c₂)
+      }
+    ; distribʳ⁻¹ = record
+      { to = distribʳ⁻¹
+      ; cong = λ where
+        (inj₁ b₁≈b₂ , a₁≈a₂) → inj₁ (b₁≈b₂ , a₁≈a₂)
+        (inj₂ c₁≈c₂ , a₁≈a₂) → inj₂ (c₁≈c₂ , a₁≈a₂)
+      }
+    }
+
+  -- omit until I can be sure it's ok
+  -- traced : ∀ {c ℓ} → Traced {obj = Setoid (c ⊔ ℓ) (c ⊔ ℓ)} _⟶_
+  -- traced = record
+  --   { WF = λ {_} {s} {b} f →
+  --     let open Equivalent equivalent in
+  --     ∃₂ λ (y : ⊤ ⟶ b) (z : ⊤ ⟶ s) →
+  --     f ∘ constʳ z ≈ (y ⦂ z) ∘ !
+  --   ; trace = λ { f (y , z , eq) → exl ∘ f ∘ constʳ z }
+  --   }
+
+  cartesianClosed :
+    ∀ {c ℓ} →
+    CartesianClosed ⦃ products {c ⊔ ℓ} {c ⊔ ℓ} ⦄ ⦃ exponentials {c} {ℓ} ⦄ _⟶_
+  cartesianClosed = record
+    { curry = λ {A} {B} f → record
+      { to = λ a → record
+        { to = curry′ (f ⟨$⟩_) a
+        ; cong = curry′ (cong f) (Setoid.refl A)
+        }
+      ; cong = λ x≈y _ → cong f (x≈y , Setoid.refl B)
+      }
+    ; apply = λ {A} {B} → record
+      { to = uncurry′ _⟨$⟩_
+      ; cong = λ { {f , x} {g , y} (f≈g , x≈y) →
+        Setoid.trans B (f≈g x) (cong g x≈y) }
+      }
+    }

src/Felix/Instances/Setoid/Type.agda

@@ -0,0 +1,57 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Felix.Instances.Setoid.Type where
+
+open import Data.Empty.Polymorphic renaming (⊥ to ⊥′)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (×-setoid)
+open import Data.Sum.Relation.Binary.Pointwise using (⊎-setoid)
+open import Data.Unit.Polymorphic renaming (⊤ to ⊤′)
+open import Function using (Func)
+open import Function.Construct.Setoid renaming (setoid to ⟶-setoid)
+open import Level using (Level; _⊔_)
+open import Relation.Binary using (Setoid)
+
+private
+  variable
+    a b ℓ₁ ℓ₂ : Level
+
+infixr 0 _⟶_
+_⟶_ : Setoid a ℓ₁ → Setoid b ℓ₂ → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
+_⟶_ = Func
+
+open Func using (cong) public
+
+infixl 5 _⟨$⟩_
+_⟨$⟩_ : ∀ {c ℓ} → ∀ {A B : Setoid c ℓ} →
+  A ⟶ B → Setoid.Carrier A → Setoid.Carrier B
+_⟨$⟩_ = Func.to
+
+module setoid-instances {c ℓ} where
+  open import Felix.Object using (Coproducts; Exponentials; Products)
+
+  instance
+    products : Products (Setoid c ℓ)
+    products = record
+      { ⊤ = record
+        { Carrier = ⊤′
+        ; _≈_ = λ _ _ → ⊤′
+        }
+      ; _×_ = ×-setoid
+      }
+
+    coproducts : Coproducts (Setoid c (c ⊔ ℓ))
+    coproducts = record
+      { ⊥ = record
+        { Carrier = ⊥′
+        ; _≈_ = λ { () () }
+        ; isEquivalence = record
+          { refl = λ { {()} }
+          ; sym = λ { {()} {()} _ }
+          ; trans = λ { {()} {()} {()} _ _ }
+          }
+        }
+      ; _⊎_ = ⊎-setoid
+      }
+
+    exponentials : Exponentials (Setoid (c ⊔ ℓ) (c ⊔ ℓ))
+    exponentials = record { _⇛_ = ⟶-setoid }

src/Felix/Laws.agda

@@ -274,7 +274,7 @@ record Distributive
   (_⇨′_ : obj → obj → Set ℓ)
   {q} ⦃ _ : Equivalent q _⇨′_ ⦄
   ⦃ _ : R.Category _⇨′_ ⦄ ⦃ _ : R.Cartesian _⇨′_ ⦄ ⦃ _ : R.Cocartesian _⇨′_ ⦄
-  ⦃ _ : R.Distributive _⇨′_ ⦄
+  ⦃ raw : R.Distributive _⇨′_ ⦄
   ⦃ _ : Category _⇨′_ ⦄ ⦃ _ : Cartesian _⇨′_ ⦄
     : Set (o ⊔ ℓ ⊔ q) where
   field
@@ -291,7 +291,7 @@ record CartesianClosed {obj : Set o} ⦃ _ : Products obj ⦄
                        {q} ⦃ _ : Equivalent q _⇨′_ ⦄
                        ⦃ _ : R.Category _⇨′_ ⦄
                        ⦃ _ : R.Cartesian _⇨′_ ⦄
-                       ⦃ _ : R.CartesianClosed _⇨′_ ⦄
+                       ⦃ raw : R.CartesianClosed _⇨′_ ⦄
                        ⦃ lCat : Category _⇨′_ ⦄ ⦃ lCart : Cartesian _⇨′_ ⦄
        : Set (o ⊔ ℓ ⊔ q) where
   private infix 0 _⇨_; _⇨_ = _⇨′_

src/Function/Construct/Setoid.agda

@@ -0,0 +1,30 @@
+-- agda-categories says that it:
+-- was not ported from old function hierarchy, see:
+-- https://github.com/agda/agda-stdlib/pull/2240
+
+{-# OPTIONS --without-K --safe #-}
+
+module Function.Construct.Setoid where
+
+  open import Function.Bundles using (Func)
+  import Function.Construct.Composition as Comp
+  open import Level using (Level)
+  open import Relation.Binary.Bundles using (Setoid)
+
+
+  private
+    variable
+      a₁ a₂ b₁ b₂ c₁ c₂ : Level
+
+  setoid : Setoid a₁ a₂ → Setoid b₁ b₂ → Setoid _ _
+  setoid From To = record
+    { Carrier = Func From To
+    ; _≈_ = λ f g → ∀ x → Func.to f x To.≈ Func.to g x
+    ; isEquivalence = record
+      { refl = λ _ → To.refl
+      ; sym = λ f≈g x → To.sym (f≈g x)
+      ; trans = λ f≈g g≈h x → To.trans (f≈g x) (g≈h x)
+      }
+    }
+    where
+      module To = Setoid To