Homotopy Type Theory action > history (Rev #3)

Skip the Navigation Links | Home Page | All Pages | Latest Revisions | Authors |

Contents

Definition

In sets

Let (M,e,μ)(M, e, \mu) be a monoid and let XX be a set. Then a left action is a function α l:M×X→X\alpha_l: M \times X \to X where there exist dependent identity terms

x:X⊢i l(x):α l(e,x)=xx:X \vdash i_l(x): \alpha_l(e, x) = x
g:M,h:M,x:X⊢c l(g,h,x):α l(g,α l(h,x))=α l(μ(g,h),x)g:M, h:M, x:X \vdash c_l(g, h, x): \alpha_l(g, \alpha_l(h, x)) = \alpha_l(\mu(g, h), x)

and a right action is a function α r:X×M→X\alpha_r: X \times M \to X where there exist dependent identity terms

x:X⊢i r(x):α r(x,e)=xx:X \vdash i_r(x): \alpha_r(x, e) = x
g:M,h:M,x:X⊢c r(g,h,x):α r(α r(x,g),h)=α r(x,μ(g,h))g:M, h:M, x:X \vdash c_r(g, h, x): \alpha_r(\alpha_r(x, g), h) = \alpha_r(x, \mu(g, h))

A curried action is a function α f:M→X→X\alpha_f: M \to X \to X where there exist an identity term

i f:α f(e)=id Xi_f: \alpha_f(e) = id_X

and dependent identity terms

g:M,h:M⊢c f(g,h):α f(g)∘α f(h)=α f(μ(g,h))g:M, h:M \vdash c_f(g, h): \alpha_f(g) \circ \alpha_f(h) = \alpha_f(\mu(g, h))

In types

There are a few generalisations of actions on sets to actions on types.

H-actions

Let (M,e,μ)(M, e, \mu) be an A3-space and let XX be a type. Then a left H-action is a function α l:M×X→X\alpha_l: M \times X \to X where there exist dependent identity terms

x:X⊢i l(x):α l(e,x)=xx:X \vdash i_l(x): \alpha_l(e, x) = x
g:M,h:M,x:X⊢c l(g,h,x):α l(g,α l(h,x))=α l(μ(g,h),x)g:M, h:M, x:X \vdash c_l(g, h, x): \alpha_l(g, \alpha_l(h, x)) = \alpha_l(\mu(g, h), x)

and a right H-action is a function α r:X×M→X\alpha_r: X \times M \to X where there exist dependent identity terms

x:X⊢i r(x):α r(x,e)=xx:X \vdash i_r(x): \alpha_r(x, e) = x
g:M,h:M,x:X⊢c r(g,h,x):α r(α r(x,g),h)=α r(x,μ(g,h))g:M, h:M, x:X \vdash c_r(g, h, x): \alpha_r(\alpha_r(x, g), h) = \alpha_r(x, \mu(g, h))

A curried H-action is a function α f:M→X→X\alpha_f: M \to X \to X where there exist an identity term

i f:α f(e)=id Xi_f: \alpha_f(e) = id_X

and dependent identity terms

g:M,h:M⊢c f(g,h):α f(g)∘α f(h)=α f(μ(g,h))g:M, h:M \vdash c_f(g, h): \alpha_f(g) \circ \alpha_f(h) = \alpha_f(\mu(g, h))

The identity types associated with an H-action are only required to hold up to homotopy.

infinity-actions

Let (M,e,μ)(M, e, \mu) be an A-infinity-space? and let XX be a type. Then a left infinity-action is a function α l:M×X→X\alpha_l: M \times X \to X where there exist dependent identity terms

x:X⊢i l(x):α l(e,x)=xx:X \vdash i_l(x): \alpha_l(e, x) = x
g:M,h:M,x:X⊢c l(g,h,x):α l(g,α l(h,x))=α l(μ(g,h),x)g:M, h:M, x:X \vdash c_l(g, h, x): \alpha_l(g, \alpha_l(h, x)) = \alpha_l(\mu(g, h), x)

and associated coherence laws for higher homotopies, whatever they may be,

and a right infinity-action is a function α r:X×M→X\alpha_r: X \times M \to X where there exist dependent identity terms

x:X⊢i r(x):α r(x,e)=xx:X \vdash i_r(x): \alpha_r(x, e) = x
g:M,h:M,x:X⊢c r(g,h,x):α r(α r(x,g),h)=α r(x,μ(g,h))g:M, h:M, x:X \vdash c_r(g, h, x): \alpha_r(\alpha_r(x, g), h) = \alpha_r(x, \mu(g, h))

and associated coherence laws for higher homotopies.

A curried infinity-action is a function α f:M→X→X\alpha_f: M \to X \to X where there exist an identity term

i f:α f(e)=id Xi_f: \alpha_f(e) = id_X

and dependent identity terms

g:M,h:M⊢c f(g,h):α f(g)∘α f(h)=α f(μ(g,h))g:M, h:M \vdash c_f(g, h): \alpha_f(g) \circ \alpha_f(h) = \alpha_f(\mu(g, h))

and associated coherence laws for higher homotopies.

The identity types associated with an infinity-action are required to hold up to coherent higher homotopy.

pre-actions

Let (M,e,μ)(M, e, \mu) be a monoid and let XX be a type. Then a left pre-action is a function α l:M×X→X\alpha_l: M \times X \to X where there exist dependent identity terms

x:X⊢ι l(x):isContr(α l(e,x)=x)x:X \vdash \iota_l(x): isContr(\alpha_l(e, x) = x)
g:M,h:M,x:X⊢κ l(g,h,x):isContr(α l(g,α l(h,x))=α l(μ(g,h),x))g:M, h:M, x:X \vdash \kappa_l(g, h, x): isContr(\alpha_l(g, \alpha_l(h, x)) = \alpha_l(\mu(g, h), x))

and a right pre-action is a function α r:X×M→X\alpha_r: X \times M \to X where there exist dependent identity terms

x:X⊢ι r(x):isContr(α r(x,e)=x)x:X \vdash \iota_r(x): isContr(\alpha_r(x, e) = x)
g:M,h:M,x:X⊢κ r(g,h,x):isContr(α r(α r(x,g),h)=α r(x,μ(g,h)))g:M, h:M, x:X \vdash \kappa_r(g, h, x): isContr(\alpha_r(\alpha_r(x, g), h) = \alpha_r(x, \mu(g, h)))

The identity types associated with a pre-action are thus required to be contractible.

See also

Revision on March 14, 2022 at 19:32:48 by Anonymous?. See the history of this page for a list of all contributions to it.

DiscussNext revision (6 more)Previous revision (2 more)Current version of pageChanges from previous revisionHistory (8 revisions)Rollback Source