interpretation "Product" 'product x y = (Prod x y).
-definition fst ≝ λA,B.λp:A × B.
+definition fst ≝ λA,B.λp:A \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 B.
match p with [pair a b ⇒ a].
-definition snd ≝ λA,B.λp:A × B.
+definition snd ≝ λA,B.λp:A \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 B.
match p with [pair a b ⇒ b].
interpretation "pair pi1" 'pi1 = (fst ? ?).
interpretation "pair pi1" 'pi1b x y = (fst ? ? x y).
interpretation "pair pi2" 'pi2b x y = (snd ? ? x y).
-theorem eq_pair_fst_snd: ∀A,B.∀p:A × B.
- p = 〈 \fst p, \snd p 〉.
+theorem eq_pair_fst_snd: ∀A,B.∀p:A \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 B.
+ p \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p, \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p 〉.
#A #B #p (cases p) // qed.
(* sum *)
(* sigma *)
inductive Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝
- dp: ∀a:A.(f a)→Sig A f.
\ No newline at end of file
+ dp: ∀a:A.(f a)→Sig A f.
+
+interpretation "Sigma" 'sigma x = (Sig ? x).
\ No newline at end of file