make isProp⊑ admissible

formalizations/guarded-cubical/Syntax/Logic.agda

@@ -60,7 +60,7 @@ data Val⊑ where
   up-L : ∀ S⊑T → Val⊑ ((ty-prec S⊑T) ∷ []) (refl-⊑ (ty-right S⊑T)) (up S⊑T) var
   up-R : ∀ S⊑T → Val⊑ ((refl-⊑ (ty-left S⊑T)) ∷ []) (ty-prec S⊑T) var (up S⊑T)
 
-  trans : Val⊑ C c V V' → Val⊑ D d V' V'' → Val⊑ (trans-⊑ctx C D) (trans c d) V V''
+  trans : Val⊑ C c V V' → Val⊑ D d V' V'' → Val⊑ (trans-⊑ctx C D) (trans-⊑ c d) V V''
   isProp⊑ : isProp (Val⊑ C c V V')
 
 data EvCtx⊑ where
@@ -73,7 +73,7 @@ data EvCtx⊑ where
   dn-R : ∀ S⊑T → EvCtx⊑ [] (ty-prec S⊑T) (refl-⊑ (ty-left S⊑T)) ∙E (dn S⊑T)
   retractionR : ∀ S⊑T → EvCtx⊑ [] (refl-⊑ (ty-right S⊑T)) (refl-⊑ (ty-right S⊑T)) ∙E (upE S⊑T ∘E dn S⊑T)
 
-  trans : EvCtx⊑ C b c E E' → EvCtx⊑ C' b' c' E' E'' → EvCtx⊑ (trans-⊑ctx C C') (trans b b') (trans c c') E E''
+  trans : EvCtx⊑ C b c E E' → EvCtx⊑ C' b' c' E' E'' → EvCtx⊑ (trans-⊑ctx C C') (trans-⊑ b b') (trans-⊑ c c') E E''
   isProp⊑ : isProp (EvCtx⊑ C c d E E')
 
 data Comp⊑ where
@@ -85,7 +85,7 @@ data Comp⊑ where
 
   err⊥ : Comp⊑ (refl-⊑ctx Γ) (refl-⊑ S) err' M
 
-  trans : Comp⊑ C c M M' → Comp⊑ D d M' M'' → Comp⊑ (trans-⊑ctx C D) (trans c d) M M''
+  trans : Comp⊑ C c M M' → Comp⊑ D d M' M'' → Comp⊑ (trans-⊑ctx C D) (trans-⊑ c d) M M''
   isProp⊑ : isProp (Comp⊑ C c M M')
 
 Subst⊑-homo : (γ γ' : Subst Δ Γ) → Type _
@@ -117,17 +117,17 @@ up-monotone : (S⊑S' : S ⊑ S')(S⊑T : S ⊑ T)(S'⊑T' : S' ⊑ T') (T⊑T'
 up-monotone {S}{S'}{T}{T'} S⊑S' S⊑T S'⊑T' T⊑T' =
   transport (λ i → Val⊑ (split-dom (~ i) ∷ []) (split-cod (~ i)) (substId {V = up (mkTyPrec S⊑S')} i) (varβ {δ = !s}{V = (up (mkTyPrec T⊑T'))} i))
   (trans (up-L (mkTyPrec (S⊑S'))) (var {C = []})
-  [ transport (λ i → Subst⊑ (trans S⊑T (refl-⊑ T) ∷ []) (swap-middle i) (ids1-expand (~ i)) (!s ,s up (mkTyPrec T⊑T')))
+  [ transport (λ i → Subst⊑ (trans-⊑ S⊑T (refl-⊑ T) ∷ []) (swap-middle i) (ids1-expand (~ i)) (!s ,s up (mkTyPrec T⊑T')))
     (!s ,s trans ((var {C = []})) (up-R (mkTyPrec T⊑T'))) ]v)
   where
-    split-cod : S'⊑T' ≡ trans (refl-⊑ _) S'⊑T'
-    split-cod = isProp⊑ _ _
+    split-cod : S'⊑T' ≡ trans-⊑ (refl-⊑ _) S'⊑T'
+    split-cod = isPropTy⊑ _ _
 
-    split-dom : S⊑T ≡ trans S⊑T (refl-⊑ _)
-    split-dom = isProp⊑ _ _
+    split-dom : S⊑T ≡ trans-⊑ S⊑T (refl-⊑ _)
+    split-dom = isPropTy⊑ _ _
 
-    swap-middle : Path ((S ∷ []) ⊑ctx (T' ∷ [])) (trans S⊑T T⊑T' ∷ []) (trans S⊑S' S'⊑T' ∷ [])
-    swap-middle i = (isProp⊑ (trans S⊑T T⊑T') (trans S⊑S' S'⊑T') i) ∷ []
+    swap-middle : Path ((S ∷ []) ⊑ctx (T' ∷ [])) (trans-⊑ S⊑T T⊑T' ∷ []) (trans-⊑ S⊑S' S'⊑T' ∷ [])
+    swap-middle i = (isPropTy⊑ (trans-⊑ S⊑T T⊑T') (trans-⊑ S⊑S' S'⊑T') i) ∷ []
 
 -- TODO: show down is monotone
 

formalizations/guarded-cubical/Syntax/Types.agda

@@ -26,17 +26,34 @@ data _⊑_ : Ty → Ty → Type where
   dyn : dyn ⊑ dyn
   _⇀_ : R ⊑ R' → S ⊑ S' → (R ⇀ S) ⊑ (R' ⇀ S')
   inj-nat : nat ⊑ dyn
-  inj-arr : (dyn ⇀ dyn) ⊑ dyn
-  trans   : R ⊑ S → S ⊑ T → R ⊑ T
-  -- this is not provable bc we can do a trans with an id relation
-  -- might cause issues later though...
-  isProp⊑ : isProp (R ⊑ S)
+  inj-arr : S ⊑ (dyn ⇀ dyn) → S ⊑ dyn
 
 refl-⊑ : ∀ S → S ⊑ S
 refl-⊑ nat = nat
 refl-⊑ dyn = dyn
 refl-⊑ (S ⇀ T) = refl-⊑ S ⇀ refl-⊑ T
 
+trans-⊑ : S ⊑ T → T ⊑ U → S ⊑ U
+trans-⊑ nat nat = nat
+trans-⊑ dyn dyn = dyn
+trans-⊑ inj-nat dyn = inj-nat
+trans-⊑ (inj-arr c) dyn = inj-arr c
+trans-⊑ (c ⇀ c') (d ⇀ d') = trans-⊑ c d ⇀ trans-⊑ c' d'
+trans-⊑ nat inj-nat = inj-nat
+trans-⊑ (c ⇀ c') (inj-arr d) = inj-arr (trans-⊑ (c ⇀ c') d)
+
+isPropTy⊑ : isProp (S ⊑ T)
+isPropTy⊑ nat nat = refl
+isPropTy⊑ dyn dyn = refl
+isPropTy⊑ (c ⇀ c') (d ⇀ d') = cong₂ _⇀_ (isPropTy⊑ c d) (isPropTy⊑ c' d')
+isPropTy⊑ inj-nat inj-nat = refl
+isPropTy⊑ (inj-arr c) (inj-arr d) = cong inj-arr (isPropTy⊑ c d)
+
+dyn-⊤ : S ⊑ dyn
+dyn-⊤ {nat} = inj-nat
+dyn-⊤ {dyn} = dyn
+dyn-⊤ {S ⇀ S₁} = inj-arr (dyn-⊤ ⇀ dyn-⊤)
+
 record TyPrec : Type where
   field
     ty-left  : Ty
@@ -72,7 +89,7 @@ refl-⊑ctx (S ∷ Γ) = (refl-⊑ S) ∷ (refl-⊑ctx Γ)
 
 trans-⊑ctx : Γ ⊑ctx Δ → Δ ⊑ctx Θ → Γ ⊑ctx Θ
 trans-⊑ctx [] [] = []
-trans-⊑ctx (c ∷ C) (d ∷ D) = (trans c d) ∷ (trans-⊑ctx C D)
+trans-⊑ctx (c ∷ C) (d ∷ D) = (trans-⊑ c d) ∷ (trans-⊑ctx C D)
 
 record CtxPrec : Type where
   field