Updated structure

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,3 @@
+```agda
+module Category.Ambient.Setoid where
+``` 

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
@@ -25,15 +25,13 @@ open import Function.Base using (id)
 -->
 
 ```agda
--- TODO arguments c ℓ here!
-module Monad.Instance.K.Instance.Maybe {o ℓ e} where
+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
@@ -78,6 +76,8 @@ 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
@@ -111,6 +111,21 @@ module _ {c ℓ : Level} where
   μ-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
     { F = record
@@ -128,10 +143,10 @@ module _ {c ℓ : Level} where
       { η = μ 
       ; 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