From d299a7d09a0c855bf058551dca83ad5442de43bf Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Mon, 4 Dec 2023 12:10:22 +0100
Subject: [PATCH] Work on delay example
---
src/Monad/Instance/K/Instance/Delay'.lagda.md | 109 ++++++++----------
1 file changed, 48 insertions(+), 61 deletions(-)
diff --git a/src/Monad/Instance/K/Instance/Delay'.lagda.md b/src/Monad/Instance/K/Instance/Delay'.lagda.md
index f6ace49..ee31027 100644
--- a/src/Monad/Instance/K/Instance/Delay'.lagda.md
+++ b/src/Monad/Instance/K/Instance/Delay'.lagda.md
@@ -1,6 +1,6 @@
<!--
```agda
-{-# OPTIONS --allow-unsolved-metas --guardedness --exact-split #-}
+{-# OPTIONS --allow-unsolved-metas --guardedness #-}
open import Level
open import Category.Ambient using (Ambient)
@@ -24,6 +24,7 @@ import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_)
open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
open import Codata.Musical.Notation
+import Category.Monad.Partiality
```
-->
@@ -51,71 +52,57 @@ module Monad.Instance.K.Instance.Delay' {c ℓ} where
laterˡ : ∀ {x y} → x ≈ (♭ y) → x ≈ later y
laterʳ : ∀ {x y} → (♭ x) ≈ y → later x ≈ y
- ≈w-refl : (a : Delay C) → a ≈ a
- ≈w-refl (now x) = now refl
- ≈w-refl (later x) = later (♯ ≈w-refl (♭ x))
+ -- later can be dropped
+ laterʳ⁻¹ : ∀ {x : Delay C} {y} → x ≈ later y → x ≈ ♭ y
+ laterʳ⁻¹ {.(later _)} {y} (later x≈y) = laterʳ (♭ x≈y)
+ laterʳ⁻¹ {x} {y} (laterˡ x≈y) = x≈y
+ laterʳ⁻¹ {.(later _)} {y} (laterʳ x≈y) = laterʳ (laterʳ⁻¹ x≈y)
- ≈w-sym : (a b : Delay C) → a ≈ b → b ≈ a
- ≈w-sym .(now _) .(now _) (now eq) = now (sym eq)
- ≈w-sym (later x) (later y) (later eq) = later (♯ (≈w-sym (♭ x) (♭ y) (♭ eq)))
- ≈w-sym x (later y) (laterˡ eq) = laterʳ (≈w-sym x (♭ y) eq)
- ≈w-sym (later x) y (laterʳ eq) = laterˡ (≈w-sym (♭ x) y eq)
+ laterˡ⁻¹ : ∀ {x} {y : Delay C} → later x ≈ y → ♭ x ≈ y
+ laterˡ⁻¹ {x} {.(later _)} (later x≈y) = laterˡ (♭ x≈y)
+ laterˡ⁻¹ {x} {.(later _)} (laterˡ x≈y) = laterˡ (laterˡ⁻¹ x≈y)
+ laterˡ⁻¹ {x} {y} (laterʳ x≈y) = x≈y
- module Trans where
- -- TODO later-trans from stdlib https://agda.github.io/agda-stdlib/v1.7.3/Category.Monad.Partiality.html#2311
- now-trans : ∀ {a b c} → a ≈ b → b ≈ now c → a ≈ now c
- now-trans {now x} {now x₁} {c} (now x₂) (now x₃) = now (IsEquivalence.trans (Setoid.isEquivalence A) x₂ x₃)
- now-trans {now x} {later x₁} {c} (laterˡ a≈b) (laterʳ b≈c) = now-trans a≈b b≈c
- now-trans {later x} {now x₁} {c} (laterʳ a≈b) (now x₂) = laterʳ (now-trans a≈b (now x₂))
- now-trans {later x} {later x₁} {c} (later x₂) (laterʳ b≈c) = laterʳ (now-trans (♭ x₂) b≈c)
- now-trans {later x} {later x₁} {c} (laterˡ a≈b) (laterʳ b≈c) = now-trans a≈b b≈c
- now-trans {later x} {later x₁} {c} (laterʳ a≈b) (laterʳ b≈c) = laterʳ (now-trans a≈b (laterʳ b≈c))
- ≈w-trans : (a b c : Delay C) → a ≈ b → b ≈ c → a ≈ c
- ≈w-trans (now _) (now _) (now _) (now a∼b) (now b∼c) = now (IsEquivalence.trans (Setoid.isEquivalence A) a∼b b∼c)
- ≈w-trans (now a) (now b) (later c) (now a∼b) (laterˡ b≈c) = laterˡ (≈w-trans (now a) (now b) (♭ c) (now a∼b) b≈c)
- ≈w-trans (now a) (later b) (now c) (laterˡ a≈b) (laterʳ b≈c) = ≈w-trans (now a) (♭ b) (now c) a≈b b≈c
- ≈w-trans (now a) (later b) (later c) (laterˡ a≈b) (later b≈c) = laterˡ (≈w-trans (now a) (♭ b) (♭ c) a≈b (♭ b≈c))
- ≈w-trans (now a) (later b) (later c) (laterˡ a≈b) (laterˡ b≈c) = laterˡ (≈w-trans (now a) {! !} (♭ c) a≈b {! !})
- ≈w-trans (now a) (later b) (later c) (laterˡ a≈b) (laterʳ b≈c) = {! !}
- ≈w-trans (later x) (now x₁) (now x₂) a≈b b≈c = {! !}
- ≈w-trans (later x) (now x₁) (later x₂) a≈b b≈c = {! !}
- ≈w-trans (later x) (later x₁) (now x₂) a≈b b≈c = {! !}
- ≈w-trans (later x) (later x₁) (later x₂) a≈b b≈c = {! !}
+ later⁻¹ : ∀ {x y : ∞ (Delay C)} → later x ≈ later y → ♭ x ≈ ♭ y
+ later⁻¹ {x} {y} (later x≈y) = ♭ x≈y
+ later⁻¹ {x} {y} (laterˡ x≈y) = laterˡ⁻¹ x≈y
+ later⁻¹ {x} {y} (laterʳ x≈y) = laterʳ⁻¹ x≈y
+ ≈-refl : (a : Delay C) → a ≈ a
+ ≈-refl (now x) = now refl
+ ≈-refl (later x) = later (♯ ≈-refl (♭ x))
- -- data _≈w_ {A : Setoid c ℓ} : Delay (Setoid.Carrier A) → Delay (Setoid.Carrier A) → Set ℓ where
- -- now : ∀ {x y} → Setoid._≈_ A x y → (now x) ≈w (now y)
- -- later : ∀ {x y} → ∞ (_≈w_ {A} (♭ x) (♭ y)) → (later x) ≈w (later y)
- -- laterˡ : ∀ {x y} → _≈w_ {A} x (♭ y) → x ≈w later y
- -- laterʳ : ∀ {x y} → _≈w_ {A} (♭ x) y → later x ≈w y
+ ≈-sym : (a b : Delay C) → a ≈ b → b ≈ a
+ ≈-sym .(now _) .(now _) (now eq) = now (sym eq)
+ ≈-sym (later x) (later y) (later eq) = later (♯ (≈-sym (♭ x) (♭ y) (♭ eq)))
+ ≈-sym x (later y) (laterˡ eq) = laterʳ (≈-sym x (♭ y) eq)
+ ≈-sym (later x) y (laterʳ eq) = laterˡ (≈-sym (♭ x) y eq)
- -- ≈w-refl : ∀ {A : Setoid c ℓ} (a : Delay (Setoid.Carrier A)) → _≈w_ {A} a a
- -- ≈w-refl {A} (now x) = now (IsEquivalence.refl (Setoid.isEquivalence A) {x})
- -- ≈w-refl {A} (later x) = later (♯ ≈w-refl (♭ x))
+ -- later-trans from stdlib https://agda.github.io/agda-stdlib/v1.7.3/Category.Monad.Partiality.html#2311
+ now-trans : ∀ {a b c} → a ≈ b → b ≈ now c → a ≈ now c
+ now-trans {now x} {now x₁} {c} (now x₂) (now x₃) = now (IsEquivalence.trans (Setoid.isEquivalence A) x₂ x₃)
+ now-trans {now x} {later x₁} {c} (laterˡ a≈b) (laterʳ b≈c) = now-trans a≈b b≈c
+ now-trans {later x} {now x₁} {c} (laterʳ a≈b) (now x₂) = laterʳ (now-trans a≈b (now x₂))
+ now-trans {later x} {later x₁} {c} (later x₂) (laterʳ b≈c) = laterʳ (now-trans (♭ x₂) b≈c)
+ now-trans {later x} {later x₁} {c} (laterˡ a≈b) (laterʳ b≈c) = now-trans a≈b b≈c
+ now-trans {later x} {later x₁} {c} (laterʳ a≈b) (laterʳ b≈c) = laterʳ (now-trans a≈b (laterʳ b≈c))
+ mutual
+ later-trans : ∀ {a b : Delay C} {c : ∞ (Delay C)} → a ≈ b → b ≈ (later c) → a ≈ (later c)
+ later-trans {later a} {later b} {c} (later a≈b) b≈c = later (♯ ≈-trans (♭ a) (♭ b) (♭ c) (♭ a≈b) (later⁻¹ b≈c))
+ {-# CATCHALL #-}
+ later-trans {a} {later b} {c} (laterˡ a≈b) b≈c = later-trans a≈b (laterˡ⁻¹ b≈c)
+ {-# CATCHALL #-}
+ later-trans {later a} {b} {c} (laterʳ a≈b) b≈c = later (♯ ≈-trans (♭ a) b (♭ c) a≈b (laterʳ⁻¹ b≈c))
+ {-# CATCHALL #-}
+ later-trans {a} {b} {c} a≈b (laterˡ b≈c) = laterˡ (≈-trans a b (♭ c) a≈b b≈c)
- -- ≈w-sym : ∀ {A : Setoid c ℓ} (a b : Delay (Setoid.Carrier A)) → _≈w_ {A} a b → _≈w_ {A} b a
- -- ≈w-sym {A} .(now _) .(now _) (now eq) = now (IsEquivalence.sym (Setoid.isEquivalence A) eq)
- -- ≈w-sym {A} (later x) (later y) (later eq) = later (♯ (≈w-sym (♭ x) (♭ y) (♭ eq)))
- -- ≈w-sym {A} x (later y) (laterˡ eq) = laterʳ (≈w-sym x (♭ y) eq)
- -- ≈w-sym {A} (later x) y (laterʳ eq) = laterˡ (≈w-sym (♭ x) y eq)
-
- -- ≈w-trans : ∀ {A : Setoid c ℓ} (a b c : Delay (Setoid.Carrier A)) → _≈w_ {A} a b → _≈w_ {A} b c → _≈w_ {A} a c
- -- ≈w-trans {A} .(now _) .(now _) .(now _) (now eq₁) (now eq₂) = now (IsEquivalence.trans (Setoid.isEquivalence A) eq₁ eq₂)
- -- ≈w-trans {A} (now x) (now y) (later z) (now eq₁) (laterˡ eq₂) = laterˡ (≈w-trans (now x) (now y) (♭ z) (now eq₁) eq₂)
- -- ≈w-trans {A} (later x) (later y) (later z) (later eq₁) (later eq₂) = later (♯ (≈w-trans (♭ x) (♭ y) (♭ z) (♭ eq₁) (♭ eq₂)))
- -- ≈w-trans {A} (later x) (later y) (later z) (later eq₁) (laterˡ eq₂) = laterˡ (≈w-trans (later x) (later y) (♭ z) (later eq₁) eq₂)
- -- -- ≈w-trans {A} .(later _) .(later _) c (later x) (laterʳ eq₂) = {! !}
- -- ≈w-trans {A} (later x) (later y) z (later eq₁) (laterʳ eq₂) = {! !}
- -- ≈w-trans {A} a .(later _) .(later _) (laterˡ eq₁) (later x) = {! !}
- -- ≈w-trans {A} a .(later _) .(later _) (laterˡ eq₁) (laterˡ eq₂) = {! !}
- -- ≈w-trans {A} a .(later _) c (laterˡ eq₁) (laterʳ eq₂) = {! !}
- -- ≈w-trans {A} .(later _) .(now _) .(now _) (laterʳ eq₁) (now x) = {! !}
- -- ≈w-trans {A} .(later _) .(later _) .(later _) (laterʳ eq₁) (later x) = {! !}
- -- ≈w-trans {A} .(later _) b .(later _) (laterʳ eq₁) (laterˡ eq₂) = {! !}
- -- ≈w-trans {A} .(later _) .(later _) c (laterʳ eq₁) (laterʳ eq₂) = {! !}
-
- -- delay-setoid : Setoid c ℓ → Setoid c ℓ
- -- delay-setoid A = record { Carrier = Delay Carrier ; _≈_ = _≈w_ {A} ; isEquivalence = record { refl = λ {x} → ≈w-refl x ; sym = λ {x y} → ≈w-sym x y ; trans = {! !} } }
- -- where open Setoid A
+ ≈-trans : ∀ (a b c : Delay C) → a ≈ b → b ≈ c → a ≈ c
+ ≈-trans a b (now c) a≈b b≈c = now-trans a≈b b≈c
+ ≈-trans a b (later c) a≈b b≈c = later-trans a≈b b≈c
+ delay-setoid : Setoid c ℓ → Setoid c ℓ
+ delay-setoid A = record { Carrier = Delay Carrier ; _≈_ = _≈_ {A} ; isEquivalence = record { refl = λ {x} → ≈-refl x ; sym = λ {x y} → ≈-sym x y ; trans = λ {x y z} → ≈-trans x y z } }
+ where
+ open Setoid A using (Carrier)
+ open Equality
```
\ No newline at end of file