Left-invertible magmas

Content created by Fredrik Bakke.

Created on 2026-05-05.
Last modified on 2026-05-05.

module structured-types.left-invertible-magmas where
Imports 
open import foundation.dependent-pair-types
open import foundation.dependent-products-propositions
open import foundation.equivalences
open import foundation.propositions
open import foundation.universe-levels

open import structured-types.magmas

Idea

A magma A is left-invertible if the multiplication map μ(a,-) : A → A is an equivalence for every a : A. In other words, if multiplying by a fixed element on the left is always an equivalence.

Left-invertibility appears as Definition 2.1(4) of [BCFR23] in the context of H-spaces.

Definitions

The predicate of being a left invertible magma

module _
  {l : Level} (A : Magma l)
  where

  is-left-invertible-Magma : UU l
  is-left-invertible-Magma = (a : type-Magma A) → is-equiv (mul-Magma A a)

  is-prop-is-left-invertible-Magma : is-prop is-left-invertible-Magma
  is-prop-is-left-invertible-Magma =
    is-prop-Π (λ a → is-property-is-equiv (mul-Magma A a))

  is-left-invertible-prop-Magma : Prop l
  is-left-invertible-prop-Magma =
    ( is-left-invertible-Magma , is-prop-is-left-invertible-Magma)

References

[BCFR23]
Ulrik Buchholtz, J. Daniel Christensen, Jarl G. Taxerås Flaten, and Egbert Rijke. Central H-spaces and banded types. 02 2023. arXiv:2301.02636.

Recent changes