Mercurial > hg > Members > atton > agda > systemF
view systemF.agda @ 9:64182a3d9a49
Trying g of Int. but not completed
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 08 Apr 2014 12:36:49 +0900 |
parents | 1801268c523d |
children | 49721ad2f556 |
line wrap: on
line source
open import Level open import Relation.Binary.PropositionalEquality module systemF {l : Level} where -- Bool Bool = \{l : Level} -> {X : Set l} -> X -> X -> X T : Bool T = \{X : Set} -> \(x : X) -> \y -> x F : Bool F = \{X : Set} -> \x -> \(y : X) -> y D : {X : Set} -> (U V : X) -> Bool -> X D {X} u v bool = bool {X} u v lemma-bool-t : {X : Set} -> {u v : X} -> D {X} u v T ≡ u lemma-bool-t = refl lemma-bool-f : {X : Set} -> {u v : X} -> D {X} u v F ≡ v lemma-bool-f = refl -- Product _×_ : {i j k : Level} -> Set i -> Set j -> Set (i ⊔ j ⊔ (suc k)) _×_ {i} {j} {k} U V = {X : Set k} -> (U -> V -> X) -> X <_,_> : {i j k : Level} -> {U : Set i} -> {V : Set j} -> U -> V -> (U × V) <_,_> {i} {j} {k} {U} {V} u v = \{X : Set k} -> \(x : U -> V -> X) -> x u v π1 : {i j : Level} -> {U : Set i} -> {V : Set j} -> (U × V) -> U π1 {i} {j} {U} {V} t = t {U} \(x : U) -> \(y : V) -> x π2 : {i j : Level} -> {U : Set i} -> {V : Set j} -> (U × V) -> V π2 {i} {j} {U} {V} t = t {V} \(x : U) -> \(y : V) -> y lemma-product-pi1 : {U V : Set l} -> {u : U} -> {v : V} -> π1 (< u , v >) ≡ u lemma-product-pi1 = refl lemma-product-pi2 : {U V : Set l} -> {u : U} -> {v : V} -> π2 (< u , v >) ≡ v lemma-product-pi2 = refl -- Empty -- Sum _+_ : {l : Level} -> Set l -> Set l -> Set (suc l) _+_ {l} U V = {X : Set l} -> (U -> X) -> (V -> X) -> X ι1 : {U V : Set l} -> U -> (U + V) ι1 {U} {V} u = \{X : Set l} -> \(x : U -> X) -> \(y : V -> X) -> x u ι2 : {U V : Set l} -> V -> (U + V) ι2 {U} {V} v = \{X : Set l} -> \(x : U -> X) -> \(y : V -> X) -> y v δ : {l : Level} -> {U V : Set l} -> {X : Set l} -> (U -> X) -> (V -> X) -> (U + V) -> X δ {l} {U} {V} {X} u v t = t {X} u v lemma-sum-iota1 : {U V X R : Set l} -> {u : U} -> {ux : (U -> X)} -> {vx : (V -> X)} -> δ ux vx (ι1 u) ≡ ux u lemma-sum-iota1 = refl lemma-sum-iota2 : {U V X R : Set l} -> {v : V} -> {ux : (U -> X)} -> {vx : (V -> X)} -> δ ux vx (ι2 v) ≡ vx v lemma-sum-iota2 = refl -- Existential data V {l} (X : Set l) : Set l where v : X -> V X Σ_,_ : (X : Set l) -> V X -> Set (suc l) Σ_,_ U u = {Y : Set l} -> ({X : Set l} -> (V X) -> Y) -> Y ⟨_,_⟩ : (U : Set l) -> (u : V U) -> Σ U , u ⟨_,_⟩ U u = \{Y : Set l} -> \(x : {X : Set l} -> (V X) -> Y) -> x {U} u ∇_,_,_ : {W : Set l} -> (X : Set l) -> { u : V X } -> X -> W -> Σ X , u -> W ∇_,_,_ {W} X {u} x w t = t {W} (\{X : Set l} -> \(x : V X) -> w) {- lemma-nabla on proofs and types (∇ X , x , w ) ⟨ U , u ⟩ ≡ w w[U/X][u/x^[U/X]] -} lemma-nabla : {X W : Set l} -> {x : X} -> {w : W} -> (∇_,_,_ {W} X {v x} x w) ⟨ X , (v x) ⟩ ≡ w lemma-nabla = refl -- Int Int : {l : Level} -> Set (suc l) Int {l} = {X : Set l} -> X -> (X -> X) -> X O : {l : Level} -> Int O {l} = \{X : Set l} -> \(x : X) -> \(y : X -> X) -> x S : {l : Level} -> Int -> Int S {l} t = \{X : Set l} -> \(x : X) -> \(y : X -> X) -> y (t {X} x y) It : {U : Set l} -> (u : U) -> (U -> U) -> Int -> U It {U} u f t = t {U} u f lemma-it-o : {U : Set l} -> {u : U} -> {f : U -> U} -> It u f O ≡ u lemma-it-o = refl lemma-it-s-o : {U : Set l} -> {u : U} -> {f : U -> U} -> {t : Int} -> It u f (S t) ≡ f (It u f t) lemma-it-s-o = refl -- U only --g : {i : Level} -> {U : Set (suc i)} -> {f : U -> Int {i} -> U} -> (U × (Int {i})) -> U --g {i} {U} {f} = \(x : (U × Int {i})) -> (f (π1 x) (π2 x)) -- Int Only --g : {i : Level} -> {U : Set (suc i)} -> {f : U -> Int {i} -> U} -> (U × (Int {i})) -> Int {i} --g {i} {U} {f} = \(x : (U × Int {i})) -> (π2 x) g : {i : Level} -> {U : Set (suc i)} -> {f : U -> Int {i} -> U} -> (U × (Int {i})) -> U × Int {i} g {i} {U} {f} = \(x : (U × Int {i})) -> < (f (π1 x) (π2 x)) , (π2 x) >