Binary operations on unordered pairs of types

module foundation.binary-operations-unordered-pairs-of-types where

open import foundation.products-unordered-pairs-of-types
open import foundation.unordered-pairs

open import foundation-core.universe-levels

Idea

A binary operation on an unordered pair of types A indexed by a 2-element type I is a map ((i : I) → A i) → B.

Definition

binary-operation-unordered-pair-types :
  {l1 l2 : Level} (A : unordered-pair (UU l1)) (B : UU l2) → UU (l1 ⊔ l2)
binary-operation-unordered-pair-types A B = product-unordered-pair-types A → B