# Cartesian products of types equipped with endomorphisms

Content created by Fredrik Bakke, Egbert Rijke and Victor Blanchi.

Created on 2023-05-10.

module structured-types.cartesian-products-types-equipped-with-endomorphisms where

Imports
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.functoriality-cartesian-product-types
open import foundation.universe-levels

open import structured-types.types-equipped-with-endomorphisms


## Idea

The cartesian product of two types equipped with an endomorphism (A , f) and (B , g) is defined as (A × B , f × g)

## Definitions

module _
{l1 l2 : Level}
(A : Type-With-Endomorphism l1) (B : Type-With-Endomorphism l2)
where

type-product-Type-With-Endomorphism : UU (l1 ⊔ l2)
type-product-Type-With-Endomorphism =
type-Type-With-Endomorphism A × type-Type-With-Endomorphism B

endomorphism-product-Type-With-Endomorphism :
type-product-Type-With-Endomorphism → type-product-Type-With-Endomorphism
endomorphism-product-Type-With-Endomorphism =
map-product
( endomorphism-Type-With-Endomorphism A)
( endomorphism-Type-With-Endomorphism B)

product-Type-With-Endomorphism :
Type-With-Endomorphism (l1 ⊔ l2)
pr1 product-Type-With-Endomorphism =
type-product-Type-With-Endomorphism
pr2 product-Type-With-Endomorphism =
endomorphism-product-Type-With-Endomorphism