Products of binary relations

Content created by Fredrik Bakke, Egbert Rijke, Fernando Chu, Julian KG, fernabnor and louismntnu.

Created on 2023-03-26.
Last modified on 2024-02-06.

module foundation.products-binary-relations where
Imports 
open import foundation.binary-relations
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.propositions

Idea

Given two relations R and S, their product is given by (R × S) (a , b) (a' , b') iff R a a' and S b b'.

Definition

The product of two relations

module _
  {l1 l2 l3 l4 : Level}
  {A : UU l1} (R : Relation-Prop l2 A)
  {B : UU l3} (S : Relation-Prop l4 B)
  where

  product-Relation-Prop :
    Relation-Prop (l2 ⊔ l4) (A × B)
  product-Relation-Prop (a , b) (a' , b') =
    product-Prop
      ( R a a')
      ( S b b')

Recent changes