Homotopy Type Theory map-extensional dagger 2-poset > history (Rev #3, changes)

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

Contents

Idea

An map-evaluational dagger 2-poset where maps satisfy the axiom of extensionality.

Definition

An map-extensional dagger 2-poset CC is a map-evaluational dagger 2-poset such that for maps f:Map(A,B)f:Map(A,B) and g:Map(A,B)g:Map(A,B), if f(x)=g(x)f(x) = g(x) for all elements x:El(A)x:El(A), then f=gf = g.

See also

Revision on May 18, 2022 at 15:11:15 by Anonymous?. See the history of this page for a list of all contributions to it.