From 6fac2c54b74e421a6dad62075c53dfb79de89c30 Mon Sep 17 00:00:00 2001
From: Eric Giovannini <ecg19@seas.upenn.edu>
Date: Fri, 28 Jul 2023 16:56:24 -0400
Subject: [PATCH] Addition to monotone combinators
---
.../Semantics/MonotoneCombinators.agda | 12 +++++++-----
1 file changed, 7 insertions(+), 5 deletions(-)
diff --git a/formalizations/guarded-cubical/Semantics/MonotoneCombinators.agda b/formalizations/guarded-cubical/Semantics/MonotoneCombinators.agda
index 0071aab..efbb8ad 100644
--- a/formalizations/guarded-cubical/Semantics/MonotoneCombinators.agda
+++ b/formalizations/guarded-cubical/Semantics/MonotoneCombinators.agda
@@ -119,11 +119,7 @@ Case' f g = record {
Case : ⟨ (A ==> C) ==> (B ==> C) ==> ((A ⊎p B) ==> C) ⟩
Case = {!!}
--- Lifting a monotone function functorially
-_~->_ : {A B C D : Poset ℓ ℓ'} ->
- ⟨ A ==> B ⟩ -> ⟨ C ==> D ⟩ -> ⟨ (B ==> C) ==> (A ==> D) ⟩
-pre ~-> post = {!!}
- -- λ f -> mCompU post (mCompU f pre)
+
@@ -301,6 +297,12 @@ Comp : (Γ : Poset ℓ ℓ') -> {A B C : Poset ℓ ℓ'} ->
Comp Γ f g = {!!}
+-- Lifting a monotone function functorially
+_~->_ : {A B C D : Poset ℓ ℓ'} ->
+ ⟨ A ==> B ⟩ -> ⟨ C ==> D ⟩ -> ⟨ (B ==> C) ==> (A ==> D) ⟩
+pre ~-> post = Curry ((mCompU post App) ∘m (With2nd pre))
+
+
module ClockedCombinators (k : Clock) where
--
GitLab