leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

refactor for exponential algebras

Browse source
This commit is contained in:
Leon Vatthauer 2024-02-04 18:49:12 +01:00
parent 38c29332fc
commit 17c023c944
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
12 changed files with 39 additions and 81 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
agda/src/Algebra/Elgot/Properties.lagda.md
View file

@ -1,4 +1,5 @@
```agda
{-# OPTIONS --allow-unsolved-metas #-}
open import Level
open import Categories.FreeObjects.Free
open import Categories.Functor.Core

2
agda/src/Category/Construction/PreElgotMonads.lagda.md
View file

@ -18,7 +18,7 @@ open import Categories.Category.Core
module Category.Construction.PreElgotMonads {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient
open import Monad.PreElgot ambient
open import Algebra.Elgot ambient
open import Algebra.Elgot cocartesian
open HomReasoning
open Equiv
open M C

2
agda/src/Category/Construction/StrongPreElgotMonads.lagda.md
View file

@ -20,7 +20,7 @@ open import Data.Product using (_,_)
module Category.Construction.StrongPreElgotMonads {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient
open import Monad.PreElgot ambient
open import Algebra.Elgot ambient
open import Algebra.Elgot cocartesian
open HomReasoning
open Equiv
open M C

56
agda/src/FreeObject.lagda.md
View file

@ -1,56 +0,0 @@
<!--
```agda
open import Level
open import Categories.Category
open import Categories.Functor
```
-->
```agda
module FreeObject where
private
variable
o ℓ e o' ℓ' e' : Level
```
# Free objects
The notion of free object has been formalized in agda-categories:
```agda
open import Categories.FreeObjects.Free
```
but we need a predicate expressing that an object 'is free':
```agda
record IsFreeObject {C : Category o ℓ e} {D : Category o' ℓ' e'} (U : Functor D C) (X : Category.Obj C) (FX : Category.Obj D) : Set (suc (e ⊔ e' ⊔ o ⊔ ℓ ⊔ o' ⊔ ℓ')) where
private
module C = Category C using (Obj; id; identityʳ; identityˡ; _⇒_; _∘_; equiv; module Equiv)
module D = Category D using (Obj; _⇒_; _∘_; equiv)
module U = Functor U using (₀; ₁)
field
η : C [ X , U.₀ FX ]
_* : ∀ {A : D.Obj} → C [ X , U.₀ A ] → D [ FX , A ]
*-lift : ∀ {A : D.Obj} (f : C [ X , U.₀ A ]) → C [ (U.₁ (f *) C.∘ η) ≈ f ]
*-uniq : ∀ {A : D.Obj} (f : C [ X , U.₀ A ]) (g : D [ FX , A ]) → C [ (U.₁ g) C.∘ η ≈ f ] → D [ g ≈ f * ]
```
and some way to convert between these notions:
```agda
IsFreeObject⇒FreeObject : ∀ {C : Category o ℓ e} {D : Category o' ℓ' e'} (U : Functor D C) (X : Category.Obj C) (FX : Category.Obj D) → IsFreeObject U X FX → FreeObject U X
IsFreeObject⇒FreeObject U X FX isFO = record
{ FX = FX
; η = η
; _* = _*
; *-lift = *-lift
; *-uniq = *-uniq
}
where open IsFreeObject isFO
-- TODO FreeObject⇒IsFreeObject
```

8
agda/src/Monad/Instance/K.lagda.md
View file

@ -17,9 +17,11 @@ open import Categories.Monad.Construction.Kleisli
```agda
module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient
open import Category.Construction.ElgotAlgebras ambient using (Elgot-Algebras)
open import Algebra.Elgot ambient using (Elgot-Algebra)
open import Algebra.Elgot.Free ambient using (FreeElgotAlgebra; elgotForgetfulF; IsStableFreeElgotAlgebra)
open import Category.Construction.ElgotAlgebras {C = C}
open Cat cocartesian using (Elgot-Algebras)
open import Algebra.Elgot cocartesian using (Elgot-Algebra)
open import Algebra.Elgot.Free cocartesian using (FreeElgotAlgebra; elgotForgetfulF)
open import Algebra.Elgot.Stable distributive using (IsStableFreeElgotAlgebra)
open Equiv
open MR C

8
agda/src/Monad/Instance/K/Commutative.lagda.md
View file

@ -20,9 +20,11 @@ open MIK ambient
open MonadK MK
open import Monad.Instance.K.Strong ambient MK
open import Monad.Instance.K.EquationalLifting ambient MK
open import Category.Construction.ElgotAlgebras ambient
open import Algebra.Elgot ambient
open import Algebra.Elgot.Free ambient using (FreeElgotAlgebra; elgotForgetfulF; IsStableFreeElgotAlgebra)
open import Category.Construction.ElgotAlgebras {C = C}
open Cat cocartesian
open import Algebra.Elgot cocartesian
open import Algebra.Elgot.Free cocartesian using (FreeElgotAlgebra; elgotForgetfulF)
open import Algebra.Elgot.Stable distributive using (IsStableFreeElgotAlgebra)
open Equiv
open HomReasoning

7
agda/src/Monad/Instance/K/EquationalLifting.lagda.md
View file

@ -18,9 +18,10 @@ open Ambient ambient
open MIK ambient
open MonadK MK
open import Monad.Instance.K.Strong ambient MK
open import Category.Construction.ElgotAlgebras ambient
open import Algebra.Elgot ambient
open import Algebra.Elgot.Free ambient using (IsStableFreeElgotAlgebra)
open import Category.Construction.ElgotAlgebras {C = C}
open Cat cocartesian
open import Algebra.Elgot cocartesian
open import Algebra.Elgot.Stable distributive using (IsStableFreeElgotAlgebra)
open HomReasoning
open Equiv

5
agda/src/Monad/Instance/K/PreElgot.lagda.md
View file

@ -18,13 +18,14 @@ module Monad.Instance.K.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK
open Ambient ambient
open MIK ambient
open MonadK MK
open import Algebra.Elgot ambient
open import Algebra.Elgot cocartesian
open import Monad.PreElgot ambient
open import Monad.Instance.K ambient
open import Monad.Instance.K.Commutative ambient MK
open import Monad.Instance.K.Strong ambient MK
open import Category.Construction.PreElgotMonads ambient
open import Category.Construction.ElgotAlgebras ambient
open import Category.Construction.ElgotAlgebras {C = C}
open Cat cocartesian
open Equiv
open HomReasoning

8
agda/src/Monad/Instance/K/Strong.lagda.md
View file

@ -22,9 +22,11 @@ import Monad.Instance.K as MIK
```agda
module Monad.Instance.K.Strong {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
open Ambient ambient
open import Category.Construction.ElgotAlgebras ambient
open import Algebra.Elgot ambient
open import Algebra.Elgot.Free ambient using (FreeElgotAlgebra; elgotForgetfulF; IsStableFreeElgotAlgebra)
open import Category.Construction.ElgotAlgebras {C = C}
open Cat cocartesian
open import Algebra.Elgot cocartesian
open import Algebra.Elgot.Free cocartesian using (FreeElgotAlgebra; elgotForgetfulF)
open import Algebra.Elgot.Stable distributive using (IsStableFreeElgotAlgebra)
open MIK ambient
open MonadK MK

8
agda/src/Monad/Instance/K/StrongPreElgot.lagda.md
View file

@ -21,15 +21,17 @@ module Monad.Instance.K.StrongPreElgot {o ℓ e} (ambient : Ambient o ℓ e) (MK
open Ambient ambient
open MIK ambient
open MonadK MK
open import Algebra.Elgot ambient
open import Algebra.Elgot.Free ambient
open import Algebra.Elgot cocartesian
open import Algebra.Elgot.Free cocartesian
open import Algebra.Elgot.Stable distributive
open import Monad.PreElgot ambient
open import Monad.Instance.K ambient
open import Monad.Instance.K.Commutative ambient MK
open import Monad.Instance.K.Strong ambient MK
open import Monad.Instance.K.PreElgot ambient MK
open import Category.Construction.StrongPreElgotMonads ambient
open import Category.Construction.ElgotAlgebras ambient
open import Category.Construction.ElgotAlgebras {C = C}
open Cat cocartesian
open Equiv
open HomReasoning

13
agda/src/Monad/Instance/Setoids/K.lagda.md
View file

@ -12,13 +12,14 @@ open import Function.Construct.Setoid renaming (setoid to _⇨_; _∙_ to _∘_)
open import Function using (_∘′_; id) renaming (_∘_ to _∘f_)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_) renaming (sym to ≣-sym; refl to ≣-refl; trans to ≣-trans)
open import FreeObject
open import Categories.FreeObjects.Free
open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
open import Data.Product.Function.NonDependent.Setoid using (proj₁ₛ)
open import Categories.Category.Instance.Properties.Setoids.Choice using ()
open import Data.Product.Relation.Binary.Pointwise.NonDependent
open import Data.Product
open import Category.Ambient using (Ambient)
open import Categories.Category.Instance.Setoids
```
-->
@ -27,12 +28,14 @@ open import Data.Product
```agda
module Monad.Instance.Setoids.K {ℓ : Level} where
open _⟶_ using (cong)
open import Monad.Instance.Setoids.Delay {ℓ} {ℓ}
open import Category.Ambient.Setoids
open Ambient (setoidAmbient {ℓ}) using (cocartesian; distributive)
open import Monad.Instance.Setoids.Delay {ℓ} {ℓ}
open import Monad.Instance.K (setoidAmbient {ℓ})
open import Algebra.Elgot (setoidAmbient {ℓ})
open import Algebra.Elgot.Free (setoidAmbient {ℓ})
open import Category.Construction.ElgotAlgebras (setoidAmbient {ℓ})
open import Algebra.Elgot cocartesian
open import Algebra.Elgot.Free cocartesian
open import Category.Construction.ElgotAlgebras {C = Setoids ℓ ℓ}
open Cat cocartesian
open import Monad.PreElgot (setoidAmbient {ℓ})
open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼_ to [_][_∼_]; _∼′_ to [_][_∼′_]; _↓_ to [_][_↓_])
open DelayMonad

2
agda/src/Monad/PreElgot.lagda.md
View file

@ -17,7 +17,7 @@ module Monad.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) where
open HomReasoning
open MR C
open Equiv
open import Algebra.Elgot ambient
open import Algebra.Elgot cocartesian
```
# (strong) pre-Elgot monads