Mercurial > hg > Members > atton > agda > systemF

annotate systemF.agda @ 9:64182a3d9a49

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Relation.Binary.PropositionalEquality
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 module systemF {l : Level} where
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 -- Bool
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 Bool = \{l : Level} -> {X : Set l} -> X -> X -> X
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 T : Bool
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 T = \{X : Set} -> \(x : X) -> \y -> x
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 F : Bool
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 F = \{X : Set} -> \x -> \(y : X) -> y
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 D : {X : Set} -> (U V : X) -> Bool -> X
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 D {X} u v bool = bool {X} u v
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 lemma-bool-t : {X : Set} -> {u v : X} -> D {X} u v T ≡ u
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 lemma-bool-t = refl
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 lemma-bool-f : {X : Set} -> {u v : X} -> D {X} u v F ≡ v
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 lemma-bool-f = refl
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 -- Product
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26
9
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
27 _×_ : {i j k : Level} -> Set i -> Set j -> Set (i ⊔ j ⊔ (suc k))
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
28 _×_ {i} {j} {k} U V = {X : Set k} -> (U -> V -> X) -> X
0
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
9
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
30 <_,_> : {i j k : Level} -> {U : Set i} -> {V : Set j} -> U -> V -> (U × V)
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
31 <_,_> {i} {j} {k} {U} {V} u v = \{X : Set k} -> \(x : U -> V -> X) -> x u v
0
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
9
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
33 π1 : {i j : Level} -> {U : Set i} -> {V : Set j} -> (U × V) -> U
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
34 π1 {i} {j} {U} {V} t = t {U} \(x : U) -> \(y : V) -> x
0
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35
9
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
36 π2 : {i j : Level} -> {U : Set i} -> {V : Set j} -> (U × V) -> V
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
37 π2 {i} {j} {U} {V} t = t {V} \(x : U) -> \(y : V) -> y
0
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 lemma-product-pi1 : {U V : Set l} -> {u : U} -> {v : V} -> π1 (< u , v >) ≡ u
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 lemma-product-pi1 = refl
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 lemma-product-pi2 : {U V : Set l} -> {u : U} -> {v : V} -> π2 (< u , v >) ≡ v
2
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
43 lemma-product-pi2 = refl
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
44
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
45 -- Empty
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
46
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
47
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
48 -- Sum
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
49
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
50 _+_ : {l : Level} -> Set l -> Set l -> Set (suc l)
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
51 _+_ {l} U V = {X : Set l} -> (U -> X) -> (V -> X) -> X
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
52
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
53 ι1 : {U V : Set l} -> U -> (U + V)
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
54 ι1 {U} {V} u = \{X : Set l} -> \(x : U -> X) -> \(y : V -> X) -> x u
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
55
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
56 ι2 : {U V : Set l} -> V -> (U + V)
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
57 ι2 {U} {V} v = \{X : Set l} -> \(x : U -> X) -> \(y : V -> X) -> y v
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
58
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
59 δ : {l : Level} -> {U V : Set l} -> {X : Set l} -> (U -> X) -> (V -> X) -> (U + V) -> X
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
60 δ {l} {U} {V} {X} u v t = t {X} u v
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
61
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
62 lemma-sum-iota1 : {U V X R : Set l} -> {u : U} -> {ux : (U -> X)} -> {vx : (V -> X)} -> δ ux vx (ι1 u) ≡ ux u
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
63 lemma-sum-iota1 = refl
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
64
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
65 lemma-sum-iota2 : {U V X R : Set l} -> {v : V} -> {ux : (U -> X)} -> {vx : (V -> X)} -> δ ux vx (ι2 v) ≡ vx v
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
66 lemma-sum-iota2 = refl
3
26cf9069f70a Wrote Sigma in Existional
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
67
6
e6a39088cb0a Wrote lemmna-nabla
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
68
3
26cf9069f70a Wrote Sigma in Existional
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
69 -- Existential
26cf9069f70a Wrote Sigma in Existional
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
70
5
63e982ff38a5 Rewrite Existential by data constructor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
71 data V {l} (X : Set l) : Set l
63e982ff38a5 Rewrite Existential by data constructor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
72 where
63e982ff38a5 Rewrite Existential by data constructor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
73 v : X -> V X
3
26cf9069f70a Wrote Sigma in Existional
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
74
5
63e982ff38a5 Rewrite Existential by data constructor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
75 Σ_,_ : (X : Set l) -> V X -> Set (suc l)
63e982ff38a5 Rewrite Existential by data constructor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
76 Σ_,_ U u = {Y : Set l} -> ({X : Set l} -> (V X) -> Y) -> Y
63e982ff38a5 Rewrite Existential by data constructor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
77
63e982ff38a5 Rewrite Existential by data constructor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
78 ⟨_,_⟩ : (U : Set l) -> (u : V U) -> Σ U , u
63e982ff38a5 Rewrite Existential by data constructor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
79 ⟨_,_⟩ U u = \{Y : Set l} -> \(x : {X : Set l} -> (V X) -> Y) -> x {U} u
6
e6a39088cb0a Wrote lemmna-nabla
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
80
e6a39088cb0a Wrote lemmna-nabla
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
81 ∇_,_,_ : {W : Set l} -> (X : Set l) -> { u : V X } -> X -> W -> Σ X , u -> W
e6a39088cb0a Wrote lemmna-nabla
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
82 ∇_,_,_ {W} X {u} x w t = t {W} (\{X : Set l} -> \(x : V X) -> w)
e6a39088cb0a Wrote lemmna-nabla
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
83
e6a39088cb0a Wrote lemmna-nabla
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
84 {-
7
aac0c4fc941c Add comments
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
85 lemma-nabla on proofs and types
6
e6a39088cb0a Wrote lemmna-nabla
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
86 (∇ X , x , w ) ⟨ U , u ⟩ ≡ w
7
aac0c4fc941c Add comments
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
87 w[U/X][u/x^[U/X]]
6
e6a39088cb0a Wrote lemmna-nabla
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
88 -}
e6a39088cb0a Wrote lemmna-nabla
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
89
7
aac0c4fc941c Add comments
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
90 lemma-nabla : {X W : Set l} -> {x : X} -> {w : W} -> (∇_,_,_ {W} X {v x} x w) ⟨ X , (v x) ⟩ ≡ w
6
e6a39088cb0a Wrote lemmna-nabla
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
91 lemma-nabla = refl
8
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
92
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
93
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
94 -- Int
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
95
9
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
96 Int : {l : Level} -> Set (suc l)
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
97 Int {l} = {X : Set l} -> X -> (X -> X) -> X
8
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
98
9
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
99 O : {l : Level} -> Int
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
100 O {l} = \{X : Set l} -> \(x : X) -> \(y : X -> X) -> x
8
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
101
9
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
102 S : {l : Level} -> Int -> Int
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
103 S {l} t = \{X : Set l} -> \(x : X) -> \(y : X -> X) -> y (t {X} x y)
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
104
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
105 It : {U : Set l} -> (u : U) -> (U -> U) -> Int -> U
8
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
106 It {U} u f t = t {U} u f
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
107
9
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
108 lemma-it-o : {U : Set l} -> {u : U} -> {f : U -> U} -> It u f O ≡ u
8
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
109 lemma-it-o = refl
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
110
9
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
111 lemma-it-s-o : {U : Set l} -> {u : U} -> {f : U -> U} -> {t : Int} -> It u f (S t) ≡ f (It u f t)
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
112 lemma-it-s-o = refl
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
113
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
114 -- U only
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
115 --g : {i : Level} -> {U : Set (suc i)} -> {f : U -> Int {i} -> U} -> (U × (Int {i})) -> U
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
116 --g {i} {U} {f} = \(x : (U × Int {i})) -> (f (π1 x) (π2 x))
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
117
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
118 -- Int Only
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
119 --g : {i : Level} -> {U : Set (suc i)} -> {f : U -> Int {i} -> U} -> (U × (Int {i})) -> Int {i}
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
120 --g {i} {U} {f} = \(x : (U × Int {i})) -> (π2 x)
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
121
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
122 g : {i : Level} -> {U : Set (suc i)} -> {f : U -> Int {i} -> U} -> (U × (Int {i})) -> U × Int {i}
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
123 g {i} {U} {f} = \(x : (U × Int {i})) -> < (f (π1 x) (π2 x)) , (π2 x) >