Homotopies of binary operations
Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Fernando Chu.
Created on 2023-02-13.
Last modified on 2023-09-13.
module foundation.binary-homotopies where
Imports
open import foundation.dependent-pair-types open import foundation.equality-dependent-function-types open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopy-induction open import foundation.universe-levels open import foundation-core.contractible-types open import foundation-core.equivalences open import foundation-core.homotopies open import foundation-core.identity-types
Idea
Consider two binary operations f g : (x : A) (y : B x) → C x y
. The type of
binary homotopies between f
and g
is defined to be the type of pointwise
identifications of f
and g
. We show that this characterizes the identity
type of (x : A) (y : B x) → C x y
.
Definition
module _ {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3} where binary-htpy : (f g : (x : A) (y : B x) → C x y) → UU (l1 ⊔ l2 ⊔ l3) binary-htpy f g = (x : A) → f x ~ g x refl-binary-htpy : (f : (x : A) (y : B x) → C x y) → binary-htpy f f refl-binary-htpy f x = refl-htpy binary-htpy-eq : (f g : (x : A) (y : B x) → C x y) → (f = g) → binary-htpy f g binary-htpy-eq f .f refl = refl-binary-htpy f is-contr-total-binary-htpy : (f : (x : A) (y : B x) → C x y) → is-contr (Σ ((x : A) (y : B x) → C x y) (binary-htpy f)) is-contr-total-binary-htpy f = is-contr-total-Eq-Π ( λ x g → f x ~ g) ( λ x → is-contr-total-htpy (f x)) is-equiv-binary-htpy-eq : (f g : (x : A) (y : B x) → C x y) → is-equiv (binary-htpy-eq f g) is-equiv-binary-htpy-eq f = fundamental-theorem-id ( is-contr-total-binary-htpy f) ( binary-htpy-eq f) extensionality-binary-Π : (f g : (x : A) (y : B x) → C x y) → (f = g) ≃ binary-htpy f g pr1 (extensionality-binary-Π f g) = binary-htpy-eq f g pr2 (extensionality-binary-Π f g) = is-equiv-binary-htpy-eq f g eq-binary-htpy : (f g : (x : A) (y : B x) → C x y) → binary-htpy f g → f = g eq-binary-htpy f g = map-inv-equiv (extensionality-binary-Π f g)
Recent changes
- 2023-09-13. Fredrik Bakke and Egbert Rijke. Refactor structured monoids (#761).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-03-26. Fernando Chu and Fredrik Bakke. First definitions towards n-ary functoriality of set quotients (#528).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).