got extend working and made a draft of gameEquiv

dlicata335 · Feb 7, 2017 · c4f472d · c4f472d
1 parent 3a0e6fe
commit c4f472d
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 7 deletions.
diff --git a/mso/Signatures.agda b/mso/Signatures.agda
@@ -235,7 +235,7 @@ module mso.Signatures where
   extend' A1 AA {r x} b = AA ,rs b
 
   extend : ∀ {oc} {Σ : Signature} (A : Structure oc Σ) {s : SigThing} → Branch A s → Structure oc (s :: Σ)
-  extend {oc} (A , AA) brnch = A , extend' {oc} (fst (A , AA)) (snd (A , AA))  brnch
+  extend {oc} (A , AA) brnch = A , extend' {oc} A AA  brnch
  -- extend {Open} (A , AA) {i x} (None) = A , AA ,none
  -- extend {Closed} (A , AA) {i x} a = A , AA ,is a
  --- extend (A , AA) {r x} b = A, AA ,rs b

diff --git a/mso/opentruth.agda b/mso/opentruth.agda
@@ -110,15 +110,23 @@ module mso.opentruth where
 
   mutual
 
-    gameEquiv : ∀ {Σ} (A1 A2 : Structure Open Σ) (φ : Formula Σ) → A1 ⊩s φ → A2 ⊩s φ → fixed (fst A1) (fst A2) → Type
+    gameEquiv : ∀ {Σ} (A1 A2 : Structure Open Σ) (φ : Formula Σ) → A1 ⊩s φ → A2 ⊩s φ → fixed (fst A1) (fst A2) → Type --f didn't have the same type but it worked??
     gameEquiv A1 A2 φ g1 g2 f =  positionEquiv' A1 A2 f × gameEquiv' A1 A2 φ g1 g2 f
 
     gameEquiv' : ∀ {Σ} (A1 A2 : Structure Open Σ) (φ : Formula Σ) → A1 ⊩s φ → A2 ⊩s φ → fixed (fst A1) (fst A2) → Type
-    gameEquiv' A1 A2 (∀i τ φ) g1 g2 f = Σ (λ (b : ListBijection (fst g1) (fst g2)) →
-                                                    ∀ bi (x : bi ∈ fst g1) → gameEquiv (extend A1 bi) (extend A2 (fst (fst b (bi , x)))) φ (snd g1 x) (snd g2 (snd (fst b (bi , x)))) {!!}) --need notion of bijection between two lists; define this to be bijection between membership types
-    gameEquiv' A1 A2 (∃i τ φ) g1 g2 f = {!!}
-    gameEquiv' A1 A2 (∀p τ φ) g1 g2 f = {!!}
-    gameEquiv' A1 A2 (∃p τ φ) g1 g2 f = {!!}
+    gameEquiv' A1 A2 (∀i τ φ) g1 g2 f = Σ (λ (b : ListBijection (fst g1) (fst g2)) → ∀ bi (x : bi ∈ fst g1)
+                                             → gameEquiv (extend A1 bi) (extend A2 (fst (fst b (bi , x)))) φ (snd g1 x) (snd g2 (snd (fst b (bi , x)))) f) --need notion of bijection between two lists; define this to be bijection between membership types
+    gameEquiv' A1 A2 (∃i τ φ) g1 g2 f = Σ (λ (b : ListBijection (fst g1) (fst g2)) →
+                                             ∀ bi (x : bi ∈ fst g1) →
+                                             gameEquiv (extend A1 bi) (extend A2 (fst (fst b (bi , x)))) φ (snd g1 x) (snd g2 (snd (fst b (bi , x)))) f)
+    gameEquiv' A1 A2 (∀p τ φ) g1 g2 f = Σ (λ (b : ListBijection (fst g1) (fst g2)) →
+                                             ∀ bi (x : bi ∈ fst g1) →
+                                             gameEquiv (extend A1 bi) (extend A2 (fst (fst b (bi , x)))) φ
+                                             (snd g1 x) (snd g2 (snd (fst b (bi , x)))) f)
+    gameEquiv' A1 A2 (∃p τ φ) g1 g2 f = Σ (λ (b : ListBijection (fst g1) (fst g2)) →
+                                             ∀ bi (x : bi ∈ fst g1) →
+                                             gameEquiv (extend A1 bi) (extend A2 (fst (fst b (bi , x)))) φ
+                                             (snd g1 x) (snd g2 (snd (fst b (bi , x)))) f)
     gameEquiv' A1 A2 (φ1 ∧ φ2) (Inl (prod1)) (Inl prod2) f = gameEquiv A1 A2 φ1 (fst prod1) (fst prod2) f  ×
                                                                   gameEquiv A1 A2 φ2 (snd prod1) (snd prod2) f
     --gameEquiv A1 A2 {!!} prod1 prod2  --help with this formula!