Dependent pair types
Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Julian KG, fernabnor and louismntnu.
Created on 2022-01-26.
Last modified on 2023-09-10.
module foundation.dependent-pair-types where
Imports
open import foundation.universe-levels
Idea
Consider a type family B
over A
. The dependent pair type Σ A B
is the
type consisting of (dependent) pairs (a , b)
where a : A
and b : B a
.
Such pairs are sometimes called dependent pairs because the type of b
depends
on the value of the first component a
.
Definition
record Σ {l1 l2 : Level} (A : UU l1) (B : A → UU l2) : UU (l1 ⊔ l2) where constructor pair field pr1 : A pr2 : B pr1 open Σ public {-# BUILTIN SIGMA Σ #-} infixr 3 _,_ pattern _,_ a b = pair a b
Constructions
ind-Σ : {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : Σ A B → UU l3} → ((x : A) (y : B x) → C (pair x y)) → ((t : Σ A B) → C t) ind-Σ f (x , y) = f x y ev-pair : {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : Σ A B → UU l3} → ((t : Σ A B) → C t) → (x : A) (y : B x) → C (pair x y) ev-pair f x y = f (x , y) triple : {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3} → (a : A) (b : B a) → C a b → Σ A (λ x → Σ (B x) (C x)) pr1 (triple a b c) = a pr1 (pr2 (triple a b c)) = b pr2 (pr2 (triple a b c)) = c triple' : {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : Σ A B → UU l3} → (a : A) (b : B a) → C (pair a b) → Σ (Σ A B) C pr1 (pr1 (triple' a b c)) = a pr2 (pr1 (triple' a b c)) = b pr2 (triple' a b c) = c
Families on dependent pair types
module _ {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} where fam-Σ : ((x : A) → B x → UU l3) → Σ A B → UU l3 fam-Σ C (x , y) = C x y
Recent changes
- 2023-09-10. Fredrik Bakke. Define precedence levels and associativities for all binary operators (#712).
- 2023-06-25. Fredrik Bakke, louismntnu, fernabnor, Egbert Rijke and Julian KG. Posets are categories, and refactor binary relations (#665).
- 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644).