Homotopy Type Theory action > history (Rev #4, changes)

Showing changes from revision #3 to #4: Added | Removed | Changed

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×XX\alpha_l: M \times X \to X where there exist dependent identity terms

x:Xi l(x):α l(e,x)=xx:X \vdash i_l(x): \alpha_l(e, x) = x
g:M,h:M,x:Xc 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×MX\alpha_r: X \times M \to X where there exist dependent identity terms

x:Xi r(x):α r(x,e)=xx:X \vdash i_r(x): \alpha_r(x, e) = x
g:M,h:M,x:Xc 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:MXX\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:Mc 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×XX\alpha_l: M \times X \to X where there exist dependent identity terms

x:Xi l(x):α l(e,x)=xx:X \vdash i_l(x): \alpha_l(e, x) = x
g:M,h:M,x:Xc 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×MX\alpha_r: X \times M \to X where there exist dependent identity terms

x:Xi r(x):α r(x,e)=xx:X \vdash i_r(x): \alpha_r(x, e) = x
g:M,h:M,x:Xc 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:MXX\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:Mc 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×XX\alpha_l: M \times X \to X where there exist dependent identity terms

x:Xi l(x):α l(e,x)=xx:X \vdash i_l(x): \alpha_l(e, x) = x
g:M,h:M,x:Xc 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×MX\alpha_r: X \times M \to X where there exist dependent identity terms

x:Xi r(x):α r(x,e)=xx:X \vdash i_r(x): \alpha_r(x, e) = x
g:M,h:M,x:Xc 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:MXX\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:Mc 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×XX\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×MX\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 May 25, 2022 at 01:17:45 by Anonymous?. See the history of this page for a list of all contributions to it.