✨ Show that Setoids is an instance of our ambient category

src/Algebra/Elgot.lagda.md

@@ -1,10 +1,9 @@
 <!--
 ```agda
-{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Categories.Functor renaming (id to idF)
 open import Categories.Functor.Algebra
-open import Category.Instance.AmbientCategory using (Ambient)
+open import Category.Ambient using (Ambient)
 ```
 -->
 

src/Algebra/Elgot/Free.lagda.md

@@ -1,8 +1,7 @@
 <!--
 ```agda
-{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
-open import Category.Instance.AmbientCategory using (Ambient)
+open import Category.Ambient using (Ambient)
 open import Categories.FreeObjects.Free
 open import Categories.Functor.Core
 open import Categories.Functor.Algebra

src/Category/Ambient.lagda.md

@@ -36,14 +36,14 @@ We work in an ambient category that
 - has exponentials `X^ℕ`
 
 ```agda
-module Category.Instance.AmbientCategory where
+module Category.Ambient where
   record Ambient (o ℓ e : Level) : Set (suc o ⊔ suc ℓ ⊔ suc e) where
     field
       C : Category o ℓ e
       extensive : Extensive C
       cartesian : Cartesian C
       ℕ : ParametrizedNNO (record { U = C ; cartesian = cartesian })
-      _^ℕ : ∀ X → Exponential C (ParametrizedNNO.N ℕ) X
+      -- _^ℕ : ∀ X → Exponential C (ParametrizedNNO.N ℕ) X
 
     cartesianCategory : CartesianCategory o ℓ e
     cartesianCategory = record { U = C ; cartesian = cartesian }

src/Category/Ambient/Setoid.lagda.md

@@ -0,0 +1,111 @@
+<!--
+```agda
+open import Level using (lift; Lift) renaming (suc to ℓ-suc)
+open import Category.Ambient
+open import Categories.Category.Instance.Setoids
+open import Categories.Category.Instance.Properties.Setoids.Extensive
+open import Categories.Category.Instance.Properties.Setoids.CCC
+open import Categories.Category.Monoidal.Instance.Setoids
+open import Categories.Category.Instance.SingletonSet
+open import Categories.Object.NaturalNumbers
+open import Relation.Binary
+open import Data.Unit.Polymorphic using (tt; ⊤)
+open import Data.Empty.Polymorphic using (⊥)
+open import Function.Equality as SΠ renaming (id to idₛ)
+open import Categories.Object.NaturalNumbers.Properties.Parametrized
+open import Categories.Category.Cocartesian
+import Relation.Binary.Reasoning.Setoid as SetoidR
+
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_)
+```
+-->
+
+# The category of Setoids can be used as instance for ambient category
+
+Most of the required properties are already proven in the agda-categories library, we are only left to construct the natural numbers object.
+
+```agda
+module Category.Ambient.Setoid {ℓ} where
+  -- equality on setoid functions
+  _≋_ : ∀ {A B : Setoid ℓ ℓ} → A ⟶ B → A ⟶ B → Set ℓ
+  _≋_ {A} {B} f g = Setoid._≈_ (A ⇨ B) f g
+  ≋-sym : ∀ {A B : Setoid ℓ ℓ} {f g : A ⟶ B} → f ≋ g → g ≋ f
+  ≋-sym {A} {B} {f} {g} = IsEquivalence.sym (Setoid.isEquivalence (A ⇨ B)) {f} {g}
+  ≋-trans : ∀ {A B : Setoid ℓ ℓ} {f g h : A ⟶ B} → f ≋ g → g ≋ h → f ≋ h
+  ≋-trans {A} {B} {f} {g} {h} = IsEquivalence.trans (Setoid.isEquivalence (A ⇨ B)) {f} {g} {h}
+
+  -- we define ℕ ourselves, instead of importing it, to avoid lifting the universe lifting (builtin Nats are defined on Set₀)
+  data ℕ : Set ℓ where
+    zero : ℕ
+    suc : ℕ → ℕ
+
+  suc-cong : ∀ {n m} → n ≡ m → suc n ≡ suc m
+  suc-cong n≡m rewrite n≡m = Eq.refl
+
+  suc-inj : ∀ {n m} → suc n ≡ suc m → n ≡ m
+  suc-inj Eq.refl = Eq.refl
+
+  ℕ-eq : Rel ℕ ℓ
+  ℕ-eq zero zero = ⊤
+  ℕ-eq zero (suc m) = ⊥
+  ℕ-eq (suc n) zero = ⊥
+  ℕ-eq (suc n) (suc m) = ℕ-eq n m
+
+  ⊤-setoid : Setoid ℓ ℓ
+  ⊤-setoid = record { Carrier = ⊤ ; _≈_ = _≡_ ; isEquivalence = Eq.isEquivalence }
+
+  ℕ-setoid : Setoid ℓ ℓ
+  ℕ-setoid = record 
+    { Carrier = ℕ 
+    ; _≈_ = _≡_ -- ℕ-eq 
+    ; isEquivalence = Eq.isEquivalence 
+    }
+  
+  zero⟶ : SingletonSetoid {ℓ} {ℓ} ⟶ ℕ-setoid
+  zero⟶ = record { _⟨$⟩_ = λ _ → zero ; cong = λ x → Eq.refl } 
+  suc⟶ : ℕ-setoid ⟶ ℕ-setoid
+  suc⟶ = record { _⟨$⟩_ = suc ; cong = suc-cong }
+
+  ℕ-universal : ∀ {A : Setoid ℓ ℓ} → SingletonSetoid {ℓ} {ℓ} ⟶ A → A ⟶ A → ℕ-setoid ⟶ A
+  ℕ-universal {A} z s = record { _⟨$⟩_ = app ; cong = cong' }
+    where
+      app : ℕ → Setoid.Carrier A
+      app zero = z ⟨$⟩ tt
+      app (suc n) = s ⟨$⟩ (app n)
+      cong' : ∀ {n m : ℕ} → n ≡ m → Setoid._≈_ A (app n) (app m)
+      cong' Eq.refl = IsEquivalence.refl (Setoid.isEquivalence A)
+    
+  ℕ-z-commute : ∀ {A : Setoid ℓ ℓ} {q : SingletonSetoid {ℓ} {ℓ} ⟶ A} {f : A ⟶ A} → q ≋ (ℕ-universal q f ∘ zero⟶)
+  ℕ-z-commute {A} {q} {f} {lift tt} _ = IsEquivalence.refl (Setoid.isEquivalence A)
+
+  ℕ-s-commute : ∀ {A : Setoid ℓ ℓ} {q : SingletonSetoid {ℓ} {ℓ} ⟶ A} {f : A ⟶ A} → (f ∘ (ℕ-universal q f)) ≋ (ℕ-universal q f ∘ suc⟶)
+  ℕ-s-commute {A} {q} {f} {n} {m} n≡m rewrite n≡m = IsEquivalence.refl (Setoid.isEquivalence A)
+
+  ℕ-unique : ∀ {A : Setoid ℓ ℓ} {q : SingletonSetoid {ℓ} {ℓ} ⟶ A} {f : A ⟶ A} {u : ℕ-setoid ⟶ A} → q ≋ (u ∘ zero⟶) → (f ∘ u) ≋ (u ∘ suc⟶) → u ≋ ℕ-universal q f
+  ℕ-unique {A} {q} {f} {u} qz fs {zero} {zero} Eq.refl = (≋-sym {SingletonSetoid} {A} {q} {u ∘ zero⟶} qz) tt
+  ℕ-unique {A} {q} {f} {u} qz fs {suc n} {suc m} Eq.refl = AR.begin 
+    u ⟨$⟩ suc n                                            AR.≈⟨ ≋-sym {ℕ-setoid} {A} {f ∘ u} {u ∘ suc⟶} fs Eq.refl ⟩ 
+    f ∘ u ⟨$⟩ m                                            AR.≈⟨ cong f (ℕ-unique {A} {q} {f} {u} qz fs {n} {m} Eq.refl) ⟩ 
+    f ∘ ℕ-universal q f ⟨$⟩ n                              AR.≈⟨ ℕ-s-commute {A} {q} {f} {n} Eq.refl ⟩ 
+    ℕ-universal q f ⟨$⟩ suc m                              AR.∎
+    where module AR = SetoidR A
+
+  setoidNNO : NNO (Setoids ℓ ℓ) SingletonSetoid-⊤
+  setoidNNO = record 
+    { N = ℕ-setoid 
+    ; isNNO = record
+      { z = zero⟶
+      ; s = suc⟶
+      ; universal = ℕ-universal
+      ; z-commute = λ {A} {q} {f} → ℕ-z-commute {A} {q} {f}
+      ; s-commute = λ {A} {q} {f} → ℕ-s-commute {A} {q} {f}
+      ; unique = λ {A} {q} {f} {u} qz fs → ℕ-unique {A} {q} {f} {u} qz fs
+      }
+    }
+
+  -- TODO might need explicit PNNO definition if we later have to work with them
+
+  setoidAmbient : Ambient (ℓ-suc ℓ) ℓ ℓ
+  setoidAmbient = record { C = Setoids ℓ ℓ ; extensive = Setoids-Extensive ℓ ; cartesian = Setoids-Cartesian ; ℕ = NNO×CCC⇒PNNO (record { U = Setoids ℓ ℓ ; cartesianClosed = Setoids-CCC ℓ }) (Cocartesian.coproducts (Setoids-Cocartesian {ℓ} {ℓ})) setoidNNO }
+```

src/Category/Construction/ElgotAlgebras.lagda.md

@@ -1,6 +1,5 @@
 <!--
 ```agda
-{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Categories.Category.Cocartesian using (Cocartesian)
 open import Categories.Category.Cartesian using (Cartesian)
@@ -14,7 +13,7 @@ open import Categories.Category
 open import Categories.Category.Distributive
 open import Categories.Category.Extensive.Bundle
 open import Categories.Category.Extensive
-open import Category.Instance.AmbientCategory using (Ambient)
+open import Category.Ambient using (Ambient)
 ```
 -->
 
@@ -210,21 +209,21 @@ module Category.Construction.ElgotAlgebras {o ℓ e} (ambient : Ambient o ℓ e)
 ## Exponentials of Elgot Algebras TODO
 
 ```agda
-  -- if the carriers of the algebra form a exponential, so do the algebras
-  B^A-Helper : ∀ {EA : Elgot-Algebra} {X : Obj} → Exponential C X (Elgot-Algebra.A EA) → Elgot-Algebra
-  B^A-Helper {EA} {X} exp = record
-    { A = A^X
-    ; algebra = record
-      { _# = λ {Z} f → λg product (((((eval +₁ idC) ∘ (Categories.Object.Product.repack C product product' +₁ idC)) ∘ dstl) ∘ (f ⁂ idC)) #ᵃ) 
-      ; #-Fixpoint = {!   !}
-      ; #-Uniformity = {!   !}
-      ; #-Folding = {!   !}
-      ; #-resp-≈ = {!   !}
-      }
-    }
-    where
-    open Exponential exp renaming (B^A to A^X; product to product')
-    open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity; #-Folding to #ᵃ-Folding; #-resp-≈ to #ᵃ-resp-≈)
-    dstr = λ {X Y Z} → IsIso.inv (isIsoˡ {X} {Y} {Z})
-    dstl = λ {X Y Z} → IsIso.inv (isIsoʳ {X} {Y} {Z})
+  -- -- if the carriers of the algebra form a exponential, so do the algebras
+  -- B^A-Helper : ∀ {EA : Elgot-Algebra} {X : Obj} → Exponential C X (Elgot-Algebra.A EA) → Elgot-Algebra
+  -- B^A-Helper {EA} {X} exp = record
+  --   { A = A^X
+  --   ; algebra = record
+  --     { _# = λ {Z} f → λg product (((((eval +₁ idC) ∘ (Categories.Object.Product.repack C product product' +₁ idC)) ∘ dstl) ∘ (f ⁂ idC)) #ᵃ) 
+  --     ; #-Fixpoint = {!   !}
+  --     ; #-Uniformity = {!   !}
+  --     ; #-Folding = {!   !}
+  --     ; #-resp-≈ = {!   !}
+  --     }
+  --   }
+  --   where
+  --   open Exponential exp renaming (B^A to A^X; product to product')
+  --   open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity; #-Folding to #ᵃ-Folding; #-resp-≈ to #ᵃ-resp-≈)
+  --   dstr = λ {X Y Z} → IsIso.inv (isIsoˡ {X} {Y} {Z})
+  --   dstl = λ {X Y Z} → IsIso.inv (isIsoʳ {X} {Y} {Z})
 ```

src/Category/Construction/PreElgotMonads.lagda.md

@@ -1,7 +1,7 @@
 <!--
 ```agda
 open import Level
-open import Category.Instance.AmbientCategory
+open import Category.Ambient using (Ambient)
 open import Categories.NaturalTransformation
 open import Categories.NaturalTransformation.Equivalence
 open import Categories.Monad

src/Category/Construction/StrongPreElgotMonads.lagda.md

@@ -1,7 +1,7 @@
 <!--
 ```agda
 open import Level
-open import Category.Instance.AmbientCategory
+open import Category.Ambient using (Ambient)
 open import Categories.NaturalTransformation
 open import Categories.NaturalTransformation.Equivalence
 open import Categories.Monad

src/Monad/Instance/Delay.lagda.md

@@ -12,7 +12,7 @@ open import Categories.Functor.Algebra
 open import Categories.Monad.Construction.Kleisli
 open import Categories.Category.Construction.F-Coalgebras
 open import Categories.NaturalTransformation
-open import Category.Instance.AmbientCategory using (Ambient)
+open import Category.Ambient using (Ambient)
 open import Data.Product using (∃-syntax; _,_; Σ-syntax)
 ```
 -->

src/Monad/Instance/Delay/Commutative.lagda.md

@@ -1,13 +1,12 @@
 <!--
 ```agda
-{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 
 open import Data.Product using (_,_; proj₁; proj₂)
 open import Categories.Category.Core
 open import Categories.Functor
 open import Categories.Functor.Coalgebra
-open import Category.Instance.AmbientCategory
+open import Category.Ambient using (Ambient)
 open import Monad.Commutative
 open import Monad.Instance.Delay
 open import Categories.Monad

src/Monad/Instance/Delay/Quotienting.lagda.md

@@ -4,7 +4,7 @@
 open import Level
 
 open import Categories.Functor
-open import Category.Instance.AmbientCategory using (Ambient)
+open import Category.Ambient using (Ambient)
 open import Categories.Monad
 open import Categories.Monad.Construction.Kleisli
 open import Categories.Monad.Relative renaming (Monad to RMonad)

src/Monad/Instance/Delay/Strong.lagda.md

@@ -4,7 +4,7 @@ open import Level
 
 open import Data.Product using (_,_; proj₁; proj₂)
 open import Categories.Category
-open import Category.Instance.AmbientCategory
+open import Category.Ambient using (Ambient)
 open import Categories.Functor
 open import Categories.Functor.Coalgebra
 open import Monad.Instance.Delay

src/Monad/Instance/K.lagda.md

@@ -7,7 +7,7 @@ open import Categories.Adjoint using (_⊣_)
 open import Categories.Adjoint.Properties using (adjoint⇒monad)
 open import Categories.Monad using (Monad)
 open import Categories.Monad.Relative using () renaming (Monad to RMonad)
-open import Category.Instance.AmbientCategory using (Ambient)
+open import Category.Ambient using (Ambient)
 open import Categories.Monad.Construction.Kleisli
 ```
 -->

src/Monad/Instance/K/Commutative.lagda.md

@@ -1,8 +1,7 @@
 <!--
 ```agda
-{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
-open import Category.Instance.AmbientCategory
+open import Category.Ambient using (Ambient)
 open import Monad.Commutative
 open import Categories.Monad.Strong
 open import Data.Product using (_,_) renaming (_×_ to _×f_)

src/Monad/Instance/K/EquationalLifting.lagda.md

@@ -2,7 +2,7 @@
 ```agda
 {-# OPTIONS --allow-unsolved-metas #-}
 open import Level
-open import Category.Instance.AmbientCategory
+open import Category.Ambient using (Ambient)
 open import Data.Product using (_,_)
 open import Categories.FreeObjects.Free
 open import Categories.Category.Construction.Kleisli

src/Monad/Instance/K/Instance/Maybe.lagda.md

@@ -3,7 +3,7 @@
 {-# OPTIONS --allow-unsolved-metas #-}
 
 open import Level
-open import Category.Instance.AmbientCategory
+open import Category.Ambient using (Ambient)
 open import Categories.Category
 open import Categories.Category.Instance.Setoids
 open import Categories.Monad
@@ -16,32 +16,29 @@ open import Relation.Binary
 open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Data.Sum.Function.Setoid
 open import Data.Sum.Relation.Binary.Pointwise
-open import Agda.Builtin.Unit using (tt)
-open import Data.Unit.Polymorphic using () renaming (⊤ to ⊤ₚ)
-open import Data.Empty.Polymorphic using () renaming (⊥ to ⊥ₚ)
+open import Data.Unit.Polymorphic using (tt; ⊤)
+open import Data.Empty.Polymorphic using (⊥)
 open import Categories.NaturalTransformation using (ntHelper)
 open import Function.Base using (id)
 ```
 -->
 
 ```agda
-module Monad.Instance.K.Instance.Maybe {o ℓ e} (ambient : Ambient o ℓ e) where
-open Ambient ambient using ()
+module Monad.Instance.K.Instance.Maybe {c ℓ} where
 ```
 
 # The Maybe Monad as instance of K
 Assuming the axiom of choice, the maybe monad is an instance of K in the category of setoids.
 
 ```agda
-module _ {c ℓ : Level} where
   data Maybe (A : Set c) : Set c where
     nothing : Maybe A
     just : A → Maybe A
 
   maybe-eq : ∀ (A : Setoid c ℓ) → Maybe (Setoid.Carrier A) → Maybe (Setoid.Carrier A) → Set ℓ
-  maybe-eq _ nothing nothing = ⊤ₚ
-  maybe-eq _ nothing (just y) = ⊥ₚ
-  maybe-eq _ (just x) nothing = ⊥ₚ
+  maybe-eq _ nothing nothing = ⊤
+  maybe-eq _ nothing (just y) = ⊥
+  maybe-eq _ (just x) nothing = ⊥
   maybe-eq A (just x) (just y) = Setoid._≈_ A x y
   
   maybeSetoid : Setoid c ℓ → Setoid c ℓ
@@ -49,7 +46,7 @@ module _ {c ℓ : Level} where
     where
       module A = Setoid A
       refl' : Reflexive (maybe-eq A)
-      refl' {nothing} = lift tt
+      refl' {nothing} = tt
       refl' {just x} = IsEquivalence.refl A.isEquivalence
       sym' : Symmetric (maybe-eq A)
       sym' {nothing} {nothing} = id
@@ -59,7 +56,7 @@ module _ {c ℓ : Level} where
       trans' : Transitive (maybe-eq A)
       trans' {nothing} {nothing} {nothing} = λ _ → id
       trans' {nothing} {nothing} {just z} = λ _ → id
-      trans' {nothing} {just y} {nothing} = λ _ _ → lift tt
+      trans' {nothing} {just y} {nothing} = λ _ _ → tt
       trans' {nothing} {just y} {just z} = λ ()
       trans' {just x} {nothing} {nothing} = λ ()
       trans' {just x} {nothing} {just z} = λ ()
@@ -78,15 +75,27 @@ module _ {c ℓ : Level} where
 
   _≋_ : ∀ {A B : Setoid c ℓ} → A ⟶ B → A ⟶ B → Set (c ⊔ ℓ)
   _≋_ {A} {B} f g = Setoid._≈_ (A ⇨ B) f g
+  ≋-sym : ∀ {A B : Setoid c ℓ} {f g : A ⟶ B} → f ≋ g → g ≋ f
+  ≋-sym {A} {B} {f} {g} = IsEquivalence.sym (Setoid.isEquivalence (A ⇨ B)) {f} {g}
 
   maybeFun-id : ∀ {A : Setoid c ℓ} → (maybeFun idₛ) ≋ idₛ {A = maybeSetoid A}
   maybeFun-id {A} {nothing} {nothing} i≈j = i≈j
   maybeFun-id {A} {just _} {just _} i≈j = i≈j
 
+  maybeFun-comp : ∀ {A B C : Setoid c ℓ} (f : A ⟶ B) (g : B ⟶ C) → maybeFun (g ∘ f) ≋ ((maybeFun g) ∘ (maybeFun f))
+  maybeFun-comp {A} {B} {C} f g {nothing} {nothing} i≈j = i≈j
+  maybeFun-comp {A} {B} {C} f g {just _} {just _} i≈j = cong g (cong f i≈j)
+
+  maybeFun-resp-≈ : ∀ {A B : Setoid c ℓ} {f g : A ⟶ B} → f ≋ g → maybeFun f ≋ maybeFun g
+  maybeFun-resp-≈ {A} {B} {f} {g} f≈g {nothing} {nothing} i≈j = i≈j
+  maybeFun-resp-≈ {A} {B} {f} {g} f≈g {just _} {just _} i≈j = f≈g i≈j
 
   η : ∀ (A : Setoid c ℓ) → A ⟶ maybeSetoid A
   η A = record { _⟨$⟩_ = just ; cong = id }
 
+  η-natural : ∀ {A B : Setoid c ℓ} (f : A ⟶ B) → (η B ∘ f) ≋ (maybeFun f ∘ η A)
+  η-natural {A} {B} f {i} {j} i≈j = cong f i≈j
+
   μ : ∀ (A : Setoid c ℓ) → maybeSetoid (maybeSetoid A) ⟶ maybeSetoid A
   μ A = record { _⟨$⟩_ = app ; cong = λ {i} {j} → cong' i j }
     where
@@ -96,6 +105,25 @@ module _ {c ℓ : Level} where
       cong' : ∀ (i j : Maybe (Maybe (Setoid.Carrier A))) → maybe-eq (maybeSetoid A) i j → maybe-eq A (app i) (app j)
       cong' nothing nothing i≈j = i≈j
       cong' (just i) (just j) i≈j = i≈j
+  
+  μ-natural : ∀ {A B : Setoid c ℓ} (f : A ⟶ B) → (μ B ∘ maybeFun (maybeFun f)) ≋ (maybeFun f ∘ μ A)
+  μ-natural {A} {B} f {nothing} {nothing} i≈j = i≈j
+  μ-natural {A} {B} f {just i} {just j} i≈j = cong (maybeFun f) {i} {j} i≈j
+
+  μ-assoc : ∀ {A : Setoid c ℓ} → (μ A ∘ maybeFun (μ A)) ≋ (μ A ∘ μ (maybeSetoid A))
+  μ-assoc {A} {nothing} {nothing} i≈j = i≈j
+  μ-assoc {A} {just i} {just j} i≈j = cong (μ A) {i} {j} i≈j
+
+  μ-sym-assoc : ∀ {A : Setoid c ℓ} → (μ A ∘ μ (maybeSetoid A)) ≋ (μ A ∘ maybeFun (μ A))
+  μ-sym-assoc {A} {nothing} {nothing} i≈j = i≈j
+  μ-sym-assoc {A} {just i} {just j} i≈j = cong (μ A) {i} {j} i≈j
+
+  identityˡ : ∀ {A : Setoid c ℓ} → (μ A ∘ maybeFun (η A)) ≋ idₛ
+  identityˡ {A} {nothing} {nothing} i≈j = i≈j
+  identityˡ {A} {just _} {just _} i≈j = i≈j
+
+  identityʳ : ∀ {A : Setoid c ℓ} → (μ A ∘ η (maybeSetoid A)) ≋ idₛ
+  identityʳ {A} {i} {j} i≈j = i≈j
 
   maybeMonad : Monad (Setoids c ℓ)
   maybeMonad = record
@@ -103,21 +131,21 @@ module _ {c ℓ : Level} where
       { F₀ = maybeSetoid
       ; F₁ = maybeFun
       ; identity = λ {A} {x} {y} → maybeFun-id {A = A} {x} {y}
-      ; homomorphism = {!   !}
-      ; F-resp-≈ = {!   !}
+      ; homomorphism = λ {A} {B} {C} {f} {g} {i} {j} → maybeFun-comp {A} {B} {C} f g {i} {j}
+      ; F-resp-≈ = maybeFun-resp-≈
       }
     ; η = ntHelper (record 
       { η = η 
-      ; commute = {!   !} 
+      ; commute = η-natural 
       })
     ; μ = ntHelper (record 
       { η = μ 
-      ; commute = {!   !} 
+      ; commute = μ-natural 
       })
-    ; assoc = {!   !}
-    ; sym-assoc = {!   !}
-    ; identityˡ = {!   !}
-    ; identityʳ = {!   !}
+    ; assoc = λ {A} {i} {j} → μ-assoc {A} {i} {j}
+    ; sym-assoc = λ {A} {i} {j} → μ-sym-assoc {A} {i} {j}
+    ; identityˡ = λ {A} {i} {j} → identityˡ {A} {i} {j}
+    ; identityʳ = λ {A} {i} {j} → identityʳ {A} {i} {j}
     }
 
 

src/Monad/Instance/K/Kleene.lagda.md

@@ -3,7 +3,7 @@
 {-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Data.Product using (_,_)
-open import Category.Instance.AmbientCategory
+open import Category.Ambient using (Ambient)
 open import Categories.Object.Terminal
 open import Categories.Functor.Algebra
 open import Categories.Object.Initial

src/Monad/Instance/K/PreElgot.lagda.md

@@ -1,7 +1,7 @@
 <!--
 ```agda
 open import Level
-open import Category.Instance.AmbientCategory
+open import Category.Ambient using (Ambient)
 open import Categories.FreeObjects.Free
 open import Categories.Object.Initial
 open import Categories.NaturalTransformation

src/Monad/Instance/K/Strong.lagda.md

@@ -11,7 +11,7 @@ open import Categories.Adjoint.Properties
 open import Categories.Monad
 open import Categories.Monad.Strong
 open import Categories.Monad.Relative renaming (Monad to RMonad)
-open import Category.Instance.AmbientCategory using (Ambient)
+open import Category.Ambient using (Ambient)
 open import Categories.NaturalTransformation
 open import Categories.Object.Terminal
 

src/Monad/Instance/K/StrongPreElgot.lagda.md

@@ -1,7 +1,7 @@
 <!--
 ```agda
 open import Level
-open import Category.Instance.AmbientCategory
+open import Category.Ambient using (Ambient)
 open import Categories.FreeObjects.Free
 open import Categories.Object.Initial
 open import Categories.NaturalTransformation

src/Monad/PreElgot.lagda.md

@@ -1,9 +1,7 @@
 <!--
 ```agda
-{-# OPTIONS --allow-unsolved-metas #-}
-
 open import Level
-open import Category.Instance.AmbientCategory using (Ambient)
+open import Category.Ambient using (Ambient)
 open import Categories.Monad.Construction.Kleisli
 open import Categories.Monad
 open import Categories.Monad.Strong

src/index.lagda.md

@@ -16,7 +16,7 @@ This is an implementation of this paper by Sergey Goncharov: [arxiv](https://arx
 The work takes place in an ambient category that fits our needs:
 
 ```agda
-open import Category.Instance.AmbientCategory
+open import Category.Ambient using (Ambient)
 ```
 
 ### Delay Monad