]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/tutorial/chapter4.ma
tutorial
[helm.git] / matita / matita / lib / tutorial / chapter4.ma
1 (*
2   Propositions as Types
3 *)
4
5 include "basics/logic.ma".
6
7 (* In the previous section, we introduced many interesting logical connectives 
8 by means of inductive definitions in the sort Prop. Do the same constructions 
9 make any sense in Type? The answer is yes! Not only they make sense, but they 
10 are indeed very familiar constructions: cartesian product, disjoint sum, empty 
11 and singleton types, and ``sigma types'' (disjoint union of families of types 
12 indexed over a given base type). This is not a coincidence, but a consequence of 
13 a strong principle known under the name of ``Propositions as Types analogy'' (or 
14 Curry-Howard correspondence).
15
16 We shall first discuss the constructions, and then we shall come back on the 
17 general analogy.*)
18
19 (***************************** Cartesian Product ******************************)
20
21 (* The cartesian product of two types A and B is defined as follows: *)
22
23 inductive Prod (A,B:Type[0]) : Type[0] ≝
24   pair : A → B → Prod A B.
25   
26 (* Observe that the definition is identical to the definition of the logical 
27 conjunction, but for the fact that the sort Prop has been replaced by Type[0].
28
29 The following declarations allows us to use the canonical notations A × B for 
30 the product and 〈a,b〉 for the pair of the two elements a and b. *)
31
32 notation "hvbox(x break × y)" with precedence 70 for @{ 'product $x $y}.
33 interpretation "Cartesian product" 'product A B = (Prod A B).
34
35 notation "hvbox(\langle term 19 a, break term 19 b\rangle)" 
36   with precedence 90 for @{ 'pair $a $b}.
37 interpretation "Pair construction" 'pair x y = (pair ?? x y).
38
39 (* We can define the two projections fst and snd by a simple case analysis of 
40 the term: *)
41
42 definition fst ≝ λA,B.λp:A×B. match p with [pair a b ⇒ a].
43 definition snd ≝ λA,B.λp:A×B. match p with [pair a b ⇒ b].
44
45 (* As in the case of inductive propositions, Matita automatically generates
46 elimination principles for A × B. In this case, however, it becomes interesting
47 to consider the possibility that the proposition towards which we are 
48 eliminating a given pair p:A × B$ contains a copy of p itself. In other words, 
49 if we have p:A × B in the current context, it is possible that p also occurs in 
50 the current goal, that is that the current goal "depends" on p.
51
52 A typical example is in the proof of the so called ``surjective pairing'' 
53 property: *)
54
55 lemma surjective_pair: ∀A,B.∀p:A×B. p = 〈fst ?? p, snd ?? p〉.
56
57 (* where p explicitly occurs in the conclusion. The proof is straightforward: we 
58 introduce A, B and p and proceed by cases on p: since p is a pair, the only 
59 possible case is that it is of the form 〈a,b〉 for some a and b.*)
60
61 #A #B #p cases p #a #b
62
63 (* At this point the goal looks like 
64       〈a,b〉 = 〈fst A B  〈a,b〉, snd A B 〈a,b〉〉 
65 and the two sides of the equation are convertible. *)
66 // qed.
67
68 (* When we call cases p we are actually applying the dependent elimination 
69 principle Prod_ind for the product, so it becomes interesting to have a look at 
70 it (we shall postpone the discussion of the way it is generated in a later 
71 section):
72
73   ∀A,B.∀P:A×B →Prop.(∀a:A,∀b:B. P 〈a,b〉) → ∀x:A×B.P x
74   
75 The previous principle has a very natural backward reading: in order to prove 
76 that the property (P x) holds for any x of type A×B it is enough to prove P〈a,b〉 
77 for any a:A and b:B. *)
78
79 (******************************* Disjoint Sum *********************************)
80
81 (* By reflecting in Type the definition of the logical disjunction we obtain the 
82 disjoint union (the sum) of two types: *)
83
84 inductive Sum (A,B:Type[0]) : Type[0] ≝
85   inl : A → Sum A B
86 | inr : B → Sum A B.
87
88 notation "hvbox(a break + b)" 
89   left associative with precedence 55 for @{ 'plus $a $b }.
90
91 interpretation "Disjoint union" 'plus A B = (Sum A B).
92
93 (* The two constructors are the left and right injections. The dependent 
94 elimination principle Sum_ind has the following shape: 
95
96   ∀A,B.∀P:A+B →Prop.
97     (∀a:A.P (inl A B a)) → (∀b:B.P (inr A B b))  → ∀x:A×B.P x
98     
99 that is, in order to prove the property (P x) for any x:A+B it is enough to
100 prove P (inl A B a) and P (inr A B b) for all a:A and b:B. *)
101
102 (************************* Empty Type and Unit Type ***************************)
103
104 (* The counterparts of False and True are, respectively, an empty type and a 
105 singleton type: *)
106
107 inductive void : Type[0] ≝.
108 inductive unit : Type[0] ≝ it: unit.
109
110 (* The elimination principle void_ind for void is simply 
111
112      ∀P:void→Prop.∀x:void.P x
113    
114 stating that any property is true for an element of type void (since we have no
115 such element).
116
117 Similarly, the elimination principle for the unit type is:
118
119     ∀P:unit→Prop. P it → ∀x:unit.P x
120   
121 Indeed, in order to prove that a property is true for any element of the unit
122 type, it is enough to prove it for the unique (canonical) inhabitant "it".
123
124 As an exercise, let us prove that all inhabitants of unit are equal to each 
125 other: *)
126
127 lemma eq_unit: ∀a,b:unit. a = b.
128
129 (* The idea is to proceed by cases on a and b: we have only one possibility, 
130 namely a=it and b=it, hence we end up to prove it=it, that is trivial. Here is 
131 the proof: *) 
132
133 #a cases a #b cases b // qed. (* also: * * // qed. *)
134
135 (* It is interesting to observe that we get exactly the same behavior by 
136 directly applying unit_ind instead of proceeding by cases. In fact, this is an 
137 alternative proof: *)
138
139 lemma eq_unit_again: ∀a,b:unit. a = b.
140 @unit_ind @unit_ind // qed.
141
142 (********************* Sigma Types and dependent matching *********************)
143
144 (* As a final example, let us consider ``type'' variants of the existential 
145 quantifier; in this case we have two interesting possibilities: *)
146
147 inductive Sig (A:Type[0]) (Q:A → Prop) : Type[0] ≝
148    Sig_intro: ∀x:A. Q x →  Sig A Q.
149
150 inductive DPair (A:Type[0]) (Q:A → Type[0]) : Type[0] ≝
151    DPair_intro: ∀x:A. Q x →  DPair A Q.
152
153 (* We shall use the notation Σx:A.Q x for the sigma type, and the similar 
154 notation ∑x:A.Q x for dependent pairs. *)
155
156 notation "hvbox(\Sigma ident i : ty break . p)"
157  left associative with precedence 20 
158 for @{'sigma (\lambda ${ident i} : $ty. $p) }.
159
160 notation "hvbox(\Sigma ident i break . p)"
161  with precedence 20 for @{'sigma (\lambda ${ident i}. $p) }.
162  
163 interpretation "Sigma" 'sigma x = (Sig ? x).
164
165 notation "hvbox(∑ ident i : ty break . p)"
166  left associative with precedence 20 
167  for @{'dpair (\lambda ${ident i} : $ty. $p) }.
168
169 notation "hvbox(∑ ident i break . p)" 
170  with precedence 20 for @{'dpair (\lambda ${ident i}. $p) }.
171  
172 interpretation "Sum" 'dpair x = (DPair ? x).
173
174 (* In the first case (traditionally called sigma type), an element of type 
175 (Sig A P) is a pair (Sig_intro ?? a h) where a is an element of type A and h is a 
176 proof that the property (P a) holds. 
177
178 A suggestive reading of (Sig A P) is as the subset of A enjoying the property P, 
179 that is {a:A | P(a)}.
180
181 In the second case, an element of DPair A B is a "dependent" pair 
182 (DPair_intro ?? a h) where a is element of type A and h maps a into an element in 
183 (B a); the intuition is to look at DProd A B as a (disjoint) family of sets B_a 
184 indexed over elements a:A. 
185
186 In both case it is possible to define projections extracting the two components
187 of the pair. Let us discuss the case of the sigma type (the other one is 
188 analogous). 
189
190 Extracting the first component (the element) is easy: *)
191
192 definition Sig_fst  ≝ λA:Type[0].λP:A→Prop.λx:Sig A P. 
193   match x with [Sig_intro a h ⇒ a].
194
195 (* Getting the second component is a bit trickier. The first problem is
196 the type of the result: given a pair (Sig_intro ?? a h): Sig A P, the type of 
197 h is (P a), that is P applied to the first argument of the pair of which we want 
198 to extract the second component! 
199 Luckily, in a language with dependent types, it is not a problem to write such a
200 a type: 
201
202   definition Sig_snd : ∀A,P.∀x:Sig A P.P (Sig_fst A P x) ≝ ...
203
204 A subtler problem is met when we define the body. If we just write 
205
206   definition Sig_snd : ∀A,P.∀x.Sig A P → P (Sig_fst A P x) ≝ λA,P,x.
207     match x with [Sig_intro a h ⇒ h].
208
209 the system will complain about the type of h. The point is that the type of this 
210 term depends on a, that is, in a not so trivial way, from the input argument x. 
211 In this situations, the type inference algorithm of Matita requires a little 
212 help: in particular the user is asked to explicitly provide the return type of 
213 the match expression, that is a map uniformly expressing the type of all 
214 branches of the case as a function of the matched expression. 
215 In our case we only have one branch and the return type is  
216
217    λx.P (Sig\_fst A P x)
218
219 We declare such a type immediately after the match, introduces by the keyword 
220 ``return'': *)
221
222 definition Sig_snd : ∀A,P.∀x:Sig A P.P (Sig_fst A P x) ≝ λA,P,x.
223   match x return λx.P (Sig_fst A P x) with [Sig_intro a h ⇒ h].
224   
225 (* Similarly, we have: *)
226
227 definition DPair_fst  ≝ λA:Type[0].λP:A→Type[0].λx:DPair A P. 
228   match x with [DPair_intro a h ⇒ a].
229   
230 definition DPair_snd : ∀A,P.∀x:DPair A P.P (DPair_fst A P x) ≝ λA,P,x.
231   match x return λx.P (DPair_fst A P x) with [DPair_intro a h ⇒ h].
232   
233 (* Remark: The careful reader may have possibly remarked that we also did a 
234 systematic abuse of the arrow symbol: the expression A → B was sometimes 
235 interpreted as the "implication" between A and B and sometimes as the "function 
236 space" between A and B. The reason of this fact is that, actually, in a 
237 foundational system like the Calculus of Construction, they are the very same 
238 notion: we only distinguish them according to the sort of the resulting 
239 expression.
240 Similarly for the dependent product ∏x:A.B: if the resulting expression is of 
241 sort Prop we shall look at it as a "universal quantification" (using the 
242 notation ∀x:A.B), while if it is in Type we shall typically regard it as a 
243 generalized cartesian product of a family of types B indexed over a base type A.
244 *)
245
246 (************************ Kolmogorov interpretation ***************************)
247
248 (* The previous analogy between propositions and types is a consequence of a 
249 deep philosophical interpretation of the notion of proof in terms of a 
250 constructive procedure that transforms proofs of the premises into a proof of 
251 the conclusion. This usually referred to as Kolmogorov interpretation, or 
252 Brouwer–Heyting–Kolmogorov (BHK) interpretation.
253
254 The interpretation states what is intended to be a proof of a given formula φ, 
255 and is specified by induction on the structure of A:
256
257 - a proof of P∧Q is a pair 〈a,b〉 where a is a proof of P and b is a proof of Q;
258 - a proof of P∨Q is a pair 〈a,b〉 where either a is 0 and b is a proof of P, or 
259   a=1 and b is a proof of Q; 
260 - a proof of P→Q is a function f which transforms a proof of x:P into a proof of 
261   (f x):Q;
262 - a proof of ∃x:S.φ(x) is a pair 〈a,b〉 where a is an element of S, and b is a 
263   proof of φ(a);
264 - a proof of ∀x:S.ϕ(x) is a function f which transforms an element x of S into a 
265   proof of \varphi(a);
266 - the formula ¬P is defined as P → False, so a proof of it is a function f which 
267   transforms a proof of P into a proof of False;
268 - there is no proof of False.
269
270 For instance, a proof of the formula P → P is a function transforming a proof of 
271 P into a proof of P: but we can just take the identity!
272
273 You can explicitly exploit this idea for writing proofs in Matita. Instead of 
274 declaring a lemma and proving it interactively, you may define your lemma as if 
275 it was the type of an expression, and directly proceed to inhabit it with its 
276 proof: *)
277
278 definition trivial: ∀P:Prop.P→P ≝ λP,h.h.
279
280 (* It is interesting to observe that this is really the very same proof
281 (intensionally!!) that would be produce interactively, as testified by the 
282 following fragment of code: *)
283
284 lemma trivial1: ∀P:Prop.P→P. #P #h @h qed.
285 lemma same_proofs: trivial = trivial1. @refl qed.
286
287 (* Even more interestingly, we can do the opposite, namely define functions
288 interactively. 
289 Suppose for instance that we need to define a function with the following
290 type: ∀A,B,C:Type[0]. (A → B → C) → A× B → C.
291 If we just declare the type of the function followed by a fullstop, Matita will 
292 start an interactive session completely analogous to a proof session, and we can 
293 use the usual tactics to ``close the goal'', that is to inhabit the type. *)
294
295 definition uncurrying: ∀A,B,C:Type[0]. (A→B→C)→A×B→C.
296 #A #B #C #f * @f qed.
297
298 (********************** The Curry-Howard correspondence ***********************)
299
300 (* The philosophical ideas contained in the BHK interpretation of a proof as a
301 constructive procedure building a proof of the conclusion from proofs of the 
302 hypothesis get a precise syntactical systematization via the so called 
303 Curry-Howard correspondence, expressing a direct relationship between computer 
304 programs and proofs. 
305 The Curry-Howard correspondence, also known as proofs-as-programs analogy, is a 
306 generalization of a syntactic analogy between systems of formal logic and 
307 computational calculi first observed by Curry for Combinatory Logic and Hilbert-
308 style deduction systems, and later by Howard for λ-calculus and Natural 
309 Deduction: in both cases the formation rules for well typed terms have precisely 
310 the same shape of the logical rules of introduction of the correspondent 
311 connective.
312  
313 As a consequence, the expression 
314
315         M:A
316         
317 really has a double possible reading: 
318
319 - M is a term of type A
320 - M is a proof of the proposition A
321
322 In both cases, M is a witness that the object A is "inhabited". A free variable 
323 x:A is an assumption about the validity of A (we assumeto have an unknown proof 
324 named x). Let us consider the cases of the introduction and elimination rule of 
325 the implication in natural deduction, that are particularly interesting:
326
327       Γ,A ⊢ B                    Γ ⊢ A → B    Γ ⊢ A
328       ----------                 -------------------
329       Γ ⊢ A → B                         Γ ⊢ B
330      
331 The first step is to enrich the representation by decorating formulae with
332 explicit proof terms. In particular, formulae in the context, being assumptions,
333 will be decorated with free variables (different form each others), while the 
334 conclusion will be decorated with a term expression with free variables 
335 appearing in the context.
336
337 Suppose Γ,x:A ⊢ M:B. What is the expected decoration for A → B?
338 According to Kolmogorov interpretation, M is a procedure transforming the proof 
339 x:A into a proof of M:B; the proof of A → B is hence the function that, taken x 
340 as input, returns M, and our canonical notation for expressing such a function 
341 is λx:A.M. Hence we get:
342
343     Γ,x:A ⊢ M:B
344     -----------------
345     Γ ⊢ λx:A.M: A → B
346     
347 that is precisely the typing rule for functions. 
348
349 Similarly, let us suppose that Γ ⊢ M:A → B,  and Γ ⊢ N:A, and let us derive a 
350 natural proof decoration for the arrow elimination rule (that is just the well 
351 known modus ponens rule). Again, we get inspiration from Kolmogorov 
352 interpretation: a proof M:A → B is a function transforming a proof of A into a 
353 proof of B hence, since we have a proof N:A in order to get a proof of B it is 
354 enough to apply M to the argument N:
355
356     Γ ⊢ M: A → B      Γ ⊢ N: A 
357     --------------------------
358           Γ ⊢ (M N):B 
359           
360 But this is nothing else than the typing rule for the application!
361
362 There is still a point that deserve discussion: the most interesting point of p
363 rograms is that they can be executed (in a functional setting, terms can be 
364 reduced to a normal form). By the Curry-Howard correspondence, this should 
365 correspond to a normalization procedure over proofs: does this operation make 
366 any sense at the logical level? Again the answer is yes: not only it makes 
367 sense, but it was independently investigated in the field of proof theory. A 
368 reducible expression corresponds to what is traditionally called a "cut". A cut
369 is a logical ``detour'' typically arising by an introduction rule immediately 
370 followed by an elimination rule for the same connective, as in a beta-redex, where 
371 we have a direct "interaction" between an application and a λ-abstraction:
372
373     (beta-rule)   λx.M N → M[N/x] 
374     
375 One of the main meta-theoretical results that is usually investigated on proof 
376 systems is if they enjoy the so called "cut-elimination" principle, that is if 
377 the cut-rule is "admissible": any proof that makes use of cuts can be turned 
378 into a cut-free proof. Since a cut is redex, a cut-free proof is a term that 
379 does not contain any redex, that is a term in normal form.
380 Hence, the system enjoys cut-elimination if and only if the corresponding 
381 calculus is normalizing.
382
383 Cut-elimination is a major tool of proof theory, with important implications on
384 e.g. "consistency", "automation" and "interpolation". 
385
386 Let us make a final remark. If a program is a proof, then what does it 
387 correspond to the act of verifying the correctness of a proof M of some 
388 proposition A? Well, M is just an expression that is supposed to have type A, so 
389 "proof verification" is nothing else that "type checking"! 
390
391 This should also clarify that proof verification is a much easier task than 
392 proof search. While the former corresponds to type checking, the second
393 one corresponds to the automatic synthesis of a program from a specification!
394
395 The main ideas behind the Curry-Howard correspondence are summarized in the 
396 following Picture:
397
398                Curry-Howard Correspondence
399
400           Logic           | Programming
401                           |
402           proposition     | type
403           proof           | program 
404           cut             | reducible expression (redex) 
405           cut free        | normal form 
406           cut elimination | normalization 
407           correctness     | type checking 
408 *)
409
410 (******************************* Prop vs. Type ********************************)
411     
412 (* In view of the Curry-Howard analogy, the reader could wonder if there is any 
413 actual difference between the two sorts Prop and Type in a system like the 
414 Calculus of Constructions, or if it just a matter of flavour. 
415
416 In fact there is a subtle difference concerning the type of product types over 
417 the given sorts. Consider for instance a higher order sentence of
418 the kind ∀P:Prop.P: this is just a sentence asserting that any proposition is 
419 true, and it looks natural to look at it as an object of sort Prop. However, if 
420 this is the case, when we are quantifying over ``all propositions' we are also 
421 implicitly quantifying over the proposition we are in the act of defining, that 
422 creates a strange and possibly dangerous circularity. 
423
424 In mathematics, definitions of this kind, where the definition (directly or 
425 indirectly) mentions or quantifies over the entity being defined are called 
426 "impredicative".
427
428 The opposite notion of impredicativity is "predicativity", which essentially 
429 entails building stratified (or ramified) theories where quantification over 
430 lower levels results in objects of some new type.
431
432 Impredicativity can be dangerous: a well known example is Russel's ``set of all 
433 sets'' resulting in famous logical paradox: does such a set contain itself as an 
434 element? If it does then by definition it should not, and if it does not then by 
435 definition it should.
436
437 A predicative approach would consist in distinguishing e.g. between ``small'' 
438 sets and ``large'' sets (collections), where the set of all small sets would 
439 result in a large set.
440
441 In fact, if we look at ∀P:Type[0].P$ as a dependent product, and we identify 
442 Type[0] as a universe of (small) ``sets'', it would seem strange to conclude 
443 that quantifying over all (small) sets we could obtain another (small) set. 
444
445 In Matita, ∀P:Type[0].P has in fact type Type[1] and not Type[0], where Type[1] 
446 is also the type of Type[0].
447
448 So, while Prop is impredicative, sorts of the kind Type[i] define a potentially 
449 infinite hierarchy of predicative sorts.
450
451 The difference between predicative and impredicative sorts is in the typing rule 
452 for the product ∏x:A.B: if the sort of B is Prop then ∏x:A.B has type Prop 
453 whatever the sort of A is; if A:Type[i] and B:Type[j], then ∏x:A.B:Type[k] where 
454 Type[k] is the smallest sort strictly larger than Type[i] and Type[j]:
455
456    Γ ⊢ A : s    Γ,x:A ⊢ B:Prop         Γ ⊢ A : Type[i]    Γ,x:A ⊢ B:Type[j]
457    ---------------------------         ------------------------------------
458        Γ ⊢ ∏x:A.B : Prop                       Γ ⊢ ∏x:A.B : Type[k]
459
460 for k = max{i,j}+1.
461
462 It is worth to observe that in Matita, the index i is just a label: constraints 
463 among universes are declared by the user. The standard library (see 
464 "basics/pts.ma" declares a few of them, with the following relations:
465
466      Type[0] < Type[1] < Type[2] < … 
467      
468 The impredicativity of Prop is not a problem from the point of view of the 
469 logical consistency, but there is a price to be paid for this: we are not 
470 allowed to eliminate Prop vs. Type[i]. In concrete terms this means that while 
471 we are allowed to build terms, types or even propositions by structural 
472 induction on terms, the only think we can do by structural induction/case 
473 analysis on proofs is to build other proofs.
474
475 For instance, we know that a proof of p:A∨B is either a proof of A or a proof B, 
476 and one could be tempted to define a function that returns the boolean true in 
477 the first case and false otherwise, by performing a simple case analysis on p: 
478
479 definition discriminate_to_bool ≝ λA,B:Prop.λp:A∨B.
480   match p with
481   [ or_introl a ⇒ tt
482   | or_intror b ⇒ ff
483   ]. 
484
485 If you type the previous definition, Matita will complain with the following 
486 error message: ``TypeChecker failure: Sort elimination not allowed: Prop towards 
487 Type[0]''.
488 Even returning the two propositions True and False intead of two booleans would 
489 not work: 
490
491 definition discriminate_to_Prop ≝ λA,B:Prop.λp:A∨B.
492  match p with
493  [ or_introl a ⇒ True
494  | or_intror b ⇒ False
495  ].
496  
497 The error message is the same as before: in both cases the sort of the branches 
498 is Type[0]. The only thing we can do is to return other proofs, like in the 
499 following example: *)
500
501 definition or_elim ≝ λA,B,C:Prop.λp:A∨B.λf:A→C.λg:B→C.
502  match p with
503  [ or_introl a ⇒ f a
504  | or_intror b ⇒ g b
505  ].
506
507 (* Exercise: repeat the previous examples in interactive mode, eliminating the
508 hypothesis p:A∨B. *)
509
510 (**************************** The axiom of choice *****************************)
511
512 (* The axiom of choice says that given a collection of non-empty sets S_i 
513 indexed over a base set I, it is possible to make a selection of exactly one
514 element x_i ∈ S_i. 
515 In type theory, this can be expressed in the following terms: *)
516
517 axiom choice_ax: ∀I:Type[0].∀S:I→Type[0].∀A:(∀i:I.S i → Type[0]).
518   (∀i:I.(∑x:S i.A i x)) → ∑f:∀i:I.S i.∀i:I.A i (f i).
519
520 (* The axiom of choice is independent from the traditional basic axioms of set
521 theory, like Zermelo–Fraenkel set theory, hence, if required, must be explicitly
522 added to the theory. This extension of ZF, known as ZFC, provides the "standard" 
523 axiomatization of set theory. 
524
525 The controversial nature of the axiom of choice is related to the effectiveness
526 of performing the selection claimed by the axiom of choice; for this reasons the 
527 axiom of choice is usually rejected by constructive mathematicians. 
528
529 However, if the proof of the existence on an inhabitant x_i for each type S_i is
530 itself constructive, then this proof already provides a method that, when 
531 applied to an element i∈I returns the witness x_i. In other words, not only the
532 above axiom "choice" is perfectly acceptable, but it is actually provable! *)
533
534 theorem choice: ∀I:Type[0].∀S:I→Type[0].∀A.
535   (∀i:I.∑x:S i.A i x) → ∑f:∀i:I.S i.∀i:I.A i (f i).
536 #I #S #A #H   
537 (* The goal is 
538     ∑f:∀i:I.S i.(∀i:I.A i (f i))
539 We need to provide the function f:∀i:I.S i, and the proof that for any i:I, 
540 A i (f i). The hypothesis H tells us that for any i we can build an object 
541 (H i): ∑x:S i.A i x. The first projection of (H i) is an element of type (S i), 
542 and we may define f ≝ λi. DPair_fst … (H i).The second projection of (H i) is
543 a witness of A i (DPair_fst … (H i)), that is, according to our defintion 
544 of f, a witness of A i (f i). Hence, λi.DPair_snd ?? (H i): ∀i:I.A i (f i). *)
545 %{(λi.DPair_fst ?? (H i)) (λi.DPair_snd ?? (H i))}
546 qed.
547
548 (* It is worth to observe that if we try to repeat the same proof with either 
549 the existential of the sigma type it will not work. For instance, the 
550 following property is not provable: *)
551
552 axiom Pchoice: ∀I:Type[0].∀S:I→Type[0].∀A.
553   (∀i:I.∃x:S i.A i x) → ∃f:∀i:I.S i.∀i:I.A i (f i).
554   
555 (* The point is that the proof would require to extract from a non-informative
556 content, namely the fact that there exists an x such that (A i x), the actual 
557 witness x, that is an informative notion, and we know that this is forbidden for 
558 consistency reasons. *)
559
560
561
562
563