Type arithmetic for dependent pair types

module foundation.type-arithmetic-dependent-pair-types where

open import foundation-core.type-arithmetic-dependent-pair-types public

Idea

We prove laws for the manipulation of dependent pair types with respect to themselves and contractible types.

See also

• Functorial properties of dependent pair types are recorded in foundation.functoriality-dependent-pair-types.

• Equality proofs in dependent pair types are characterized in foundation.equality-dependent-pair-types.

• The universal property of dependent pair types is treated in foundation.universal-property-dependent-pair-types.

• Arithmetical laws involving cartesian product types are recorded in foundation.type-arithmetic-cartesian-product-types.

• Arithmetical laws involving dependent product types are recorded in foundation.type-arithmetic-dependent-function-types.

• Arithmetical laws involving coproduct types are recorded in foundation.type-arithmetic-coproduct-types.

• Arithmetical laws involving the unit type are recorded in foundation.type-arithmetic-unit-type.

• Arithmetical laws involving the empty type are recorded in foundation.type-arithmetic-empty-type.