From 404998651b62cea79ca03090d2a858263c5aef76 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Sat, 27 May 2023 10:38:06 -0400
Subject: [PATCH] A convenient abstract semantics of the term language

---
 .../Abstract/TermModel/Convenient.agda        | 19 +++++--------------
 1 file changed, 5 insertions(+), 14 deletions(-)

diff --git a/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient.agda b/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient.agda
index 95c2236..29f7841 100644
--- a/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient.agda
+++ b/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient.agda
@@ -66,17 +66,8 @@ record Model â„“ â„“' â„“'' : Type (â„“-suc (â„“-max â„“ (â„“-max â„“' â„“'')))
     -- now the dyn stuff
     -- a model of dyn/casts
     dyn : cat .ob
-    -- type precision
-    _⊑_ : (cat .ob) → (cat .ob) → Type ℓ''
-    isReflexive⊑  : ∀ {a} → a ⊑ a
-    isTransitive⊑ : ∀ {a b c} → a ⊑ b → b ⊑ c → a ⊑ c
-    isProp⊑ : ∀ {a b} → isProp (a ⊑ b)
-
-    -- monotonicity of type constructors
-    prod-is-monotone : ∀ {a a' b b'} → a ⊑ a' → b ⊑ b' → (a × b) ⊑ (a' × b')
-    parfun-is-monotone : ∀ {a a' b b'} → a ⊑ a' → b ⊑ b' → (a ⇀ b) ⊑ (a' ⇀ b')
-    inj-nat : nat ⊑ dyn
-    inj-arr : (dyn ⇀ dyn) ⊑ dyn
-
-    up : ∀ {a b} → a ⊑ b → cat [ a , b ]
-    dn : ∀ {a b} → a ⊑ b → cat [ b , T ⟅ a ⟆ ]
+
+    -- at this point we will model injection and projection as
+    -- arbitrary morphisms
+    inj : cat [ nat + (dyn ⇀ dyn) , dyn ]
+    prj : cat [ dyn , T ⟅ nat + (dyn ⇀ dyn) ⟆ ]
-- 
GitLab