On this page:
Σ0
pair0
Σ1
pair1
Σ
pair
fst0
fst1
fst
snd0
snd1
snd
7.0

3.5 Dependent Pairs

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

pair0

 : (-> (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

pair1

 : (-> (A : (Type 1)) (P : (-> A (Type 1))) (a : A) (b : (P a)) (Σ1 A P))
The strong dependent pair datatype, for universe (Type 1)

syntax

(Σ (x : A) P)

(Σ 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:229:31 (Nat) #<procedure:...impl/runtime.rkt:229:31>))

> (Σ0 Nat (λ (x : Nat) (== Nat x 5)))

(Σ0 (Nat) (...impl/runtime.rkt:229:31 (Nat) #<procedure:...impl/runtime.rkt:229: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:229:31 (Nat) #<procedure:...impl/runtime.rkt:229:31>) (s (s (s (s (s (z)))))) (PM-refl (Nat) (s (s (s (s (s (z))))))))

procedure

(fst0 A P p)  A

  A : (Type 0)
  P : (-> A (Type 0))
  p : (Σ0 A P)
Takes the first projection of p.

procedure

(fst1 A P p)  A

  A : (Type 1)
  P : (-> A (Type 1))
  p : (Σ1 A P)
Like fst0 but for Σ1.

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:
> (fst (pair (λ (x : Nat) (== Nat x 5)) 5 (refl Nat 5)))

(s (s (s (s (s (z))))))

procedure

(snd0 A P p)  (P (fst p))

  A : (Type 0)
  P : (-> A (Type 0))
  p : (Σ0 A P)
Takes the second projection of p.

procedure

(snd1 A P p)  (P (fst p))

  A : (Type 1)
  P : (-> A (Type 1))
  p : (Σ1 A P)
Like snd0 but for Σ1.

syntax

(snd p)

Syntactic sugar for snd0 and snd1, like fst.

Example:
> (snd (pair (λ (x : Nat) (== Nat x 5)) 5 (refl Nat 5)))

(PM-refl (Nat) (s (s (s (s (s (z)))))))