src/Algebra/Elgot.lagda.md

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

src/Algebra/Elgot/Free.lagda.md

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

src/Category/Ambient/Setoid.lagda.md

@@ -1,111 +0,0 @@
-<!--
-```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,5 +1,6 @@
 <!--
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Categories.Category.Cocartesian using (Cocartesian)
 open import Categories.Category.Cartesian using (Cartesian)
@@ -13,7 +14,7 @@ open import Categories.Category
 open import Categories.Category.Distributive
 open import Categories.Category.Extensive.Bundle
 open import Categories.Category.Extensive
-open import Category.Ambient using (Ambient)
+open import Category.Instance.AmbientCategory using (Ambient)
 ```
 -->
 
@@ -209,21 +210,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.Ambient using (Ambient)
+open import Category.Instance.AmbientCategory
 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.Ambient using (Ambient)
+open import Category.Instance.AmbientCategory
 open import Categories.NaturalTransformation
 open import Categories.NaturalTransformation.Equivalence
 open import Categories.Monad

src/Category/Instance/AmbientCategory.lagda.md

@@ -36,14 +36,14 @@ We work in an ambient category that
 - has exponentials `X^ℕ`
 
 ```agda
-module Category.Ambient where
+module Category.Instance.AmbientCategory 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/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.Ambient using (Ambient)
+open import Category.Instance.AmbientCategory using (Ambient)
 open import Data.Product using (∃-syntax; _,_; Σ-syntax)
 ```
 -->

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

@@ -1,12 +1,13 @@
 <!--
 ```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.Ambient using (Ambient)
+open import Category.Instance.AmbientCategory
 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.Ambient using (Ambient)
+open import Category.Instance.AmbientCategory 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.Ambient using (Ambient)
+open import Category.Instance.AmbientCategory
 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.Ambient using (Ambient)
+open import Category.Instance.AmbientCategory using (Ambient)
 open import Categories.Monad.Construction.Kleisli
 ```
 -->

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

@@ -1,7 +1,8 @@
 <!--
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
-open import Category.Ambient using (Ambient)
+open import Category.Instance.AmbientCategory
 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.Ambient using (Ambient)
+open import Category.Instance.AmbientCategory
 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.Ambient using (Ambient)
+open import Category.Instance.AmbientCategory
 open import Categories.Category
 open import Categories.Category.Instance.Setoids
 open import Categories.Monad
@@ -16,29 +16,32 @@ 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 Data.Unit.Polymorphic using (tt; ⊤)
-open import Data.Empty.Polymorphic using (⊥)
+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 Categories.NaturalTransformation using (ntHelper)
 open import Function.Base using (id)
 ```
 -->
 
 ```agda
-module Monad.Instance.K.Instance.Maybe {c ℓ} where
+module Monad.Instance.K.Instance.Maybe {o ℓ e} (ambient : Ambient o ℓ e) where
+open Ambient ambient using ()
 ```
 
 # 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 ℓ
@@ -46,7 +49,7 @@ Assuming the axiom of choice, the maybe monad is an instance of K in the categor
     where
       module A = Setoid A
       refl' : Reflexive (maybe-eq A)
-      refl' {nothing} = tt
+      refl' {nothing} = lift tt
       refl' {just x} = IsEquivalence.refl A.isEquivalence
       sym' : Symmetric (maybe-eq A)
       sym' {nothing} {nothing} = id
@@ -56,7 +59,7 @@ Assuming the axiom of choice, the maybe monad is an instance of K in the categor
       trans' : Transitive (maybe-eq A)
       trans' {nothing} {nothing} {nothing} = λ _ → id
       trans' {nothing} {nothing} {just z} = λ _ → id
-      trans' {nothing} {just y} {nothing} = λ _ _ → tt
+      trans' {nothing} {just y} {nothing} = λ _ _ → lift tt
       trans' {nothing} {just y} {just z} = λ ()
       trans' {just x} {nothing} {nothing} = λ ()
       trans' {just x} {nothing} {just z} = λ ()
@@ -75,27 +78,15 @@ Assuming the axiom of choice, the maybe monad is an instance of K in the categor
 
   _≋_ : ∀ {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
@@ -105,25 +96,6 @@ Assuming the axiom of choice, the maybe monad is an instance of K in the categor
       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
@@ -131,21 +103,21 @@ Assuming the axiom of choice, the maybe monad is an instance of K in the categor
       { F₀ = maybeSetoid
       ; F₁ = maybeFun
       ; identity = λ {A} {x} {y} → maybeFun-id {A = A} {x} {y}
-      ; homomorphism = λ {A} {B} {C} {f} {g} {i} {j} → maybeFun-comp {A} {B} {C} f g {i} {j}
-      ; F-resp-≈ = maybeFun-resp-≈
+      ; homomorphism = {!   !}
+      ; F-resp-≈ = {!   !}
       }
     ; η = ntHelper (record 
       { η = η 
-      ; commute = η-natural 
+      ; commute = {!   !} 
       })
     ; μ = ntHelper (record 
       { η = μ 
-      ; commute = μ-natural 
+      ; commute = {!   !} 
       })
-    ; 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}
+    ; assoc = {!   !}
+    ; sym-assoc = {!   !}
+    ; identityˡ = {!   !}
+    ; identityʳ = {!   !}
     }
 
 

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.Ambient using (Ambient)
+open import Category.Instance.AmbientCategory
 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.Ambient using (Ambient)
+open import Category.Instance.AmbientCategory
 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.Ambient using (Ambient)
+open import Category.Instance.AmbientCategory 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.Ambient using (Ambient)
+open import Category.Instance.AmbientCategory
 open import Categories.FreeObjects.Free
 open import Categories.Object.Initial
 open import Categories.NaturalTransformation

src/Monad/PreElgot.lagda.md

@@ -1,7 +1,9 @@
 <!--
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
+
 open import Level
-open import Category.Ambient using (Ambient)
+open import Category.Instance.AmbientCategory 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.Ambient using (Ambient)
+open import Category.Instance.AmbientCategory
 ```
 
 ### Delay Monad