Mercurial > hg > Members > atton > agda > systemF
changeset 4:f52b8d899cf1
Rewrote Existential Sigma and < , >. but has yellow
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 25 Mar 2014 17:20:45 +0900 |
| parents | 26cf9069f70a |
| children | 63e982ff38a5 |
| files | systemF.agda |
| diffstat | 1 files changed, 9 insertions(+), 10 deletions(-) [+] |
line wrap: on
line diff
--- a/systemF.agda Mon Mar 24 20:12:59 2014 +0900 +++ b/systemF.agda Tue Mar 25 17:20:45 2014 +0900 @@ -67,15 +67,14 @@ -- Existential ---Σ_,_ : {l : Level} -> (X : Set l) -> (V : Set l) -> {Y : Set l} -> {X : Set l} -> {VX : (Set -> Set )} -> Set l ---Σ_,_ : Set l -> Set l -> {Y : Set l} -> (Set l -> Y) -> Y ---Σ_,_ : Set -> Set -> {Y : Set l} -> ? -> ? ---Σ_,_ X V = \{Y : Set l} -> (\(V : Set) -> Y) -> Y +--Σ_,_ : {Vx : Set l} -> Set (suc l) +--Σ_,_ = {Vx : Set l} -> (X : Set l) -> (V : {var : Set l} -> Vx) -> {Y : Set l} -> ({X : Set l} -> (Vx -> Y)) -> Y + +Σ_,_ : {Vx : Set l} -> (X : Set l) -> (V : {var : Set l} -> Vx) -> Set (suc l) +Σ_,_ {Vx} X V = {Y : Set l} -> ({X : Set l} -> (Vx -> Y)) -> Y -Σ_,_ : Set l -> (V : Set l) -> {v : V} -> {Y : Set l} -> (V -> Y) -> Y -Σ_,_ X V {v} = \{Y : Set l} -> \(vy : V -> Y) -> vy v +--⟨_,_⟩ : {Vu : Set l} -> (U : Set l) -> (u : Vu) -> (Σ_,_ {Vu} U u) +--⟨_,_⟩ : {Vu : Set l} -> (U : Set l) -> (u : Vu) -> {Y : Set l} -> ({X : Set l} -> Set l -> Set l) -> Set l ---⟨_,_⟩ : (U : Set l) -> (u : U) -> (Σ U , V) ---⟨_,_⟩ : Set l -> ? -> {Y : Set l} -> ? -> ? -> ? ---⟨_,_⟩ U u = \{Y : Set l} -> (x : (\{X} -> \(v : V) -> y)) -> x U u ---⟨_,_⟩ U u = \{Y : Set l} -> \(x : (\{X : Set l} -> (VY : (V -> Y)))) -> x U u +⟨_,_⟩ : {Vu : Set l} -> {V : {U : Set l} -> Vu} -> (U : Set l) -> (u : Vu) -> (Σ_,_ {Vu} U V) +⟨_,_⟩ {Vu} {V} U u = \{Y : Set l} -> \(x : ({X : Set l} -> (Vu -> Y))) -> x {U} u