From 4a0ad2e025242d6fef2519d845342d466fdc84c1 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Fri, 25 Mar 2022 14:22:12 -0500 Subject: [PATCH] Oops, forgot a hole! --- prototyping/Properties/Subtyping.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prototyping/Properties/Subtyping.agda b/prototyping/Properties/Subtyping.agda index 25b67500..0a20f244 100644 --- a/prototyping/Properties/Subtyping.agda +++ b/prototyping/Properties/Subtyping.agda @@ -265,7 +265,7 @@ not-quite-set-theoretic-only-if : ∀ {S₁ T₁ S₂ T₂} → (∀ Q → Q ⊆ Comp((Language S₁) ⊗ Comp(Language T₁)) → Q ⊆ Comp((Language S₂) ⊗ Comp(Language T₂))) → (Language (S₁ ⇒ T₁) ⊆ Language (S₂ ⇒ T₂)) -not-quite-set-theoretic-only-if {S₁} {T₁} {S₂} {T₂} s₂ t₂ S₂s₂ ¬T₂t₂ p = {!!} where +not-quite-set-theoretic-only-if {S₁} {T₁} {S₂} {T₂} s₂ t₂ S₂s₂ ¬T₂t₂ p = r where Q : (Tree × Tree) → Set Q (t , u) = Either (¬Language S₁ t) (Language T₁ u)