Homotopy Type Theory
A3-space > history (changes)
Showing changes from revision #10 to #11:
Added | Removed | Changed
Idea
< A3-space?
Sometimes we can equip a type with a certain structure, called an A 3 A_3 -algebra structure, allowing us to derive some nice properties about the type and 0-truncate it to form monoids .
Definition
An A 3 A_3 -space or A 3 A_3 -algebra in homotopy types or H-monoid consists of
A type A A ,
A basepoint e : A e:A
A binary operation μ : A → A → A \mu : A \to A \to A
A left unitorλ : ∏ ( a : A ) μ ( e , a ) = a \lambda:\prod_{(a:A)} \mu(e,a)=a
A right unitorρ : ∏ ( a : A ) μ ( a , e ) = a \rho:\prod_{(a:A)} \mu(a,e)=a
An asssociatorα : ∏ ( a : A ) ∏ ( b : A ) ∏ ( c : A ) μ ( μ ( a , b ) , c ) = μ ( a , μ ( b , c ) ) \alpha:\prod_{(a:A)} \prod_{(b:A)} \prod_{(c:A)} \mu(\mu(a, b),c)=\mu(a,\mu(b,c))
Homomorphisms of A 3 A_3 -spaces
A homomorphism of A 3 A_3 -spaces between two A 3 A_3 -spaces A A and B B consists of
ϕ λ : ( ∏ ( a : A ) μ ( e A , a ) = a ) → ( ∏ ( b : B ) μ ( e B , b ) = b ) \phi_\lambda:\left(\prod_{(a:A)} \mu(e_A,a)=a\right) \to \left(\prod_{(b:B)} \mu(e_B,b)=b\right)
such that the left unitor is preserved:
ϕ λ ( λ A ) = λ B \phi_\lambda(\lambda_A) = \lambda_B
ϕ ρ : ( ∏ ( a : A ) μ ( a , e A ) = a ) → ( ∏ ( b : B ) μ ( b , e B ) = b ) \phi_\rho:\left(\prod_{(a:A)} \mu(a, e_A)=a\right) \to \left(\prod_{(b:B)} \mu(b, e_B)=b\right)
such that the right unitor is preserved:
ϕ ρ ( ρ A ) = ρ B \phi_\rho(\rho_A) = \rho_B
ϕ α : ( ∏ ( a 1 : A ) ∏ ( a 2 : A ) ∏ ( a 3 : A ) μ ( μ ( a 1 , a 2 ) , a 3 ) = μ ( a 1 , μ ( a 2 , a 3 ) ) ) → ( ∏ ( b 1 : B ) ∏ ( b 2 : B ) ∏ ( b 3 : B ) μ ( μ ( b 1 , b 2 ) , b 3 ) = μ ( b 1 , μ ( b 2 , b 3 ) ) ) \phi_\alpha:\left(\prod_{(a_1:A)} \prod_{(a_2:A)} \prod_{(a_3:A)} \mu(\mu(a_1, a_2),a_3)=\mu(a_1,\mu(a_2,a_3))\right) \to \left(\prod_{(b_1:B)} \prod_{(b_2:B)} \prod_{(b_3:B)} \mu(\mu(b_1, b_2),b_3)=\mu(b_1,\mu(b_2,b_3))\right)
such that the associator is preserved:
ϕ α ( α A ) = α B \phi_\alpha(\alpha_A) = \alpha_B
Examples
The integers are an A 3 A_3 -space.
Every loop space is naturally an A 3 A_3 -space with path concatenation as the operation. In fact every loop space is a group .
The type of endofunctions A → A A \to A has the structure of an A 3 A_3 -space, with basepoint id A id_A , operation function composition.
A monoid is a 0-truncated A 3 A_3 -space.
See also
On the nlab
Classically, an A3-space is a homotopy type equipped with the structure of a monoid in the homotopy category (only).
Last revised on June 9, 2022 at 14:44:42.
See the history of this page for a list of all contributions to it.