7.7
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
constructor
: (-> (A : (Type 0)) (P : (-> A (Type 0))) (a : A) (b : (P a)) (Σ0 A P))
1 parameter type
constructor
: (-> (A : (Type 1)) (P : (-> A (Type 1))) (a : A) (b : (P a)) (Σ1 A P))
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) (...impl/runtime.rkt:231:31 (Nat) #<procedure:...impl/runtime.rkt:231:31>))
> (Σ0 Nat (λ (x : Nat) (== Nat x 5))) (Σ0 (Nat) (...impl/runtime.rkt:231:31 (Nat) #<procedure:...impl/runtime.rkt:231:31>))
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) (...impl/runtime.rkt:231:31 (Nat) #<procedure:...impl/runtime.rkt:231:31>) (s (s (s (s (s (z)))))) (PM-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: