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

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

Contents

Definition

An A evaluational map-evaluational dagger 2-posetCC is a concrete dagger 2-poset? 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 09:58:12 by Anonymous?. See the history of this page for a list of all contributions to it.