Cartesian product types

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Julian KG, fernabnor and louismntnu.

Created on 2022-02-04.
Last modified on 2024-03-02.

module foundation-core.cartesian-product-types where
Imports
open import foundation.dependent-pair-types
open import foundation.universe-levels

Definitions

Cartesian products of types are defined as dependent pair types, using a constant type family.

The cartesian product type

product : {l1 l2 : Level} (A : UU l1) (B : UU l2)  UU (l1  l2)
product A B = Σ A  _  B)

pair' :
  {l1 l2 : Level} {A : UU l1} {B : UU l2}  A  B  product A B
pair' = pair

infixr 15 _×_
_×_ : {l1 l2 : Level} (A : UU l1) (B : UU l2)  UU (l1  l2)
_×_ = product

The induction principle for the cartesian product type

ind-product :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : A × B  UU l3} 
  ((x : A) (y : B)  C (x , y))  (t : A × B)  C t
ind-product = ind-Σ

The recursion principle for the cartesian product type

rec-product :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} 
  (A  B  C)  (A × B)  C
rec-product = ind-product

Recent changes