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

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

Contents

Definition

A map-evaluational dagger 2-poset CC is a concrete dagger 2-poset?dagger 2-poset with elements with a function ()(()):Map(A,B)×El(A)El(B)(-)((-)): Map(A,B) \times El(A) \to El(B) for map evaluation for elements of objects A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C) such that for maps f:Map(A,B)f:Map(A,B) and g:Map(B,C)g:Map(B,C) and element x:El(A)x:El(A), (gf)(x)=g(f(x))(g \circ f)(x) = g(f(x)).

See also

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