some more refactor

This commit is contained in:
Leon Vatthauer 2024-02-15 21:51:54 +01:00
parent 98837f659c
commit e4af840dc2
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
2 changed files with 30 additions and 3 deletions

View file

@ -375,6 +375,24 @@ module DelayMonad where
open DelayMonad
-- custom definition of natural numbers together with the setoid on with propositional equality
module nat {} where
data : Set where
zero :
suc :
-setoid : Setoid
-setoid = record
{ Carrier =
; _≈_ = _≡_
; isEquivalence = Eq.isEquivalence
}
suc-inj : ∀ {n m} → suc n ≡ suc m → n ≡ m
suc-inj Eq.refl = Eq.refl
open nat
module extra {A : Setoid c (c ⊔ )} where
≲→≈ : {x y : Delay A } → [ A ][ x ≲ y ] → [ A ][ x ≈ y ]
≲→≈′ : {x y : Delay A } → [ A ][ x ≲′ y ] → [ A ][ x ≈′ y ]

View file

@ -30,17 +30,18 @@ open import Categories.Category.Instance.Properties.Setoids.CCC using (Setoids-C
module Monad.Instance.Setoids.K { : Level} where
open _⟶_ using (cong)
open import Category.Ambient.Setoids
open Ambient (setoidAmbient {}) using (cocartesian; distributive)
open Ambient (setoidAmbient {} {}) using (cocartesian; distributive)
open import Monad.Instance.Setoids.Delay {} {}
open import Monad.Instance.K (setoidAmbient {})
open import Monad.Instance.K (setoidAmbient {} {})
open import Algebra.Elgot cocartesian
open import Algebra.Elgot.Free cocartesian
open import Algebra.Elgot.Stable distributive
open import Category.Construction.ElgotAlgebras {C = Setoids } cocartesian
open import Monad.PreElgot (setoidAmbient {})
open import Monad.PreElgot (setoidAmbient {} {})
open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈_ to [_][_≈_]; __ to [_][__]; __ to [_][__]; _↓_ to [_][_↓_])
open DelayMonad
open extra
open nat
open Setoid using () renaming (Carrier to _; _≈_ to [_][_≡_])
open eq using () renaming (refl to ≡-refl; sym to ≡-sym; trans to ≡-trans)
@ -297,6 +298,14 @@ module Monad.Instance.Setoids.K { : Level} where
delay-lift' = record { to = < helper # > ; cong = helper#≈-cong }
-- interesting note:
-- the following definition prevents more general universe levels, i.e. we would like to parametrize this module by two levels c and , one for carriers and one for proofs.
-- but adopting this approach would force us to talk about setoids of type Setoid (c ⊔ ), this does not work with the definition below,
-- since propositional equality lives on the same level as values, this means the type below would have to look like:
-- ‖_‖ : Setoid c (c ⊔ ) → Setoid c c
-- this in turn does not play together nicely with later definition.
-- discretize a setoid
‖_‖ : Setoid → Setoid
_ ‖ X ‖ = X