Binary equivalences on unordered pairs of types

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-05-01.
Last modified on 2023-06-10.

module foundation.binary-equivalences-unordered-pairs-of-types where
Imports 
open import foundation.binary-operations-unordered-pairs-of-types
open import foundation.products-unordered-pairs-of-types
open import foundation.universe-levels
open import foundation.unordered-pairs

open import foundation-core.equivalences
open import foundation-core.function-types

Idea

A binary operation f : ((i : I) → A i) → B is a binary equivalence if for each i : I and each x : A i the map f ∘ pair x : A (swap i) → B is an equivalence.

Definition

is-binary-equiv-unordered-pair-types :
  {l1 l2 : Level} (A : unordered-pair (UU l1)) {B : UU l2}
  (f : binary-operation-unordered-pair-types A B) → UU (l1 ⊔ l2)
is-binary-equiv-unordered-pair-types A f =
  (i : type-unordered-pair A) (x : element-unordered-pair A i) →
  is-equiv (f ∘ pair-product-unordered-pair-types A i x)

Recent changes