8.16.0.1
3.5 Dependent Pairs
| (require cur/stdlib/sigma) | package: cur-lib |
This library defines the strong dependent pair datatype, Σ, and basic
operations and syntax sugar.
1 parameter type
Σ0 : (-> (A : (Type 0)) (P : (-> A (Type 0))) (Type 0))
constructor
: (-> (A : (Type 0)) (P : (-> A (Type 0))) (a : A) (b : (P a)) (Σ0 A P))
The strong dependent pair datatype, for universe (Type 0)
1 parameter type
Σ1 : (-> (A : (Type 1)) (P : (-> A (Type 1))) (Type 1))
constructor
: (-> (A : (Type 1)) (P : (-> A (Type 1))) (a : A) (b : (P a)) (Σ1 A P))
The strong dependent pair datatype, for universe (Type 1)
Syntactic sugar for writing Σ0 and Σ1.
Infers which constructor to use based on the universe level of A.
The syntax (Σ (x : A) P) expands to (Σ A (λ (x : A) P)).
Examples:
> (Σ (x : Nat) (== Nat x 5)) (Σ0 (Nat) #<procedure:...ur/stdlib/sigma.rkt:42:14>)
> (Σ0 Nat (λ (x : Nat) (== Nat x 5))) (Σ0 (Nat) #<procedure>)
syntax
(pair P a b)
Syntactic sugar for writing pair0 and pair1.
Infers the type annotation A based on the type of a
Also infers which constructor to use based on the universe level of A.
Example:
> (pair (λ (x : Nat) (== Nat x 5)) 5 (refl Nat 5)) (pair0 (Nat) #<procedure> (s (s (s (s (s (z)))))) (refl (Nat) (s (s (s (s (s (z))))))))
Takes the first projection of p.
syntax
(fst p)
Syntactic sugar for fst0 and fst1, like pair.
Infers the type arguments A and P from p, and
expands to (fst0 A P p) or (fst1 A P p) depending on the
universe levels of the types.
Example:
Takes the second projection of p.
syntax
(snd p)
Example: