Homotopy Type Theory
map-evaluational dagger 2-poset > history (Rev #2, changes)
Showing changes from revision #1 to #2:
Added | Removed | Changed
Contents
Definition
An evaluational dagger 2-poset C C 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) , ( g ∘ f ) ( x ) = g ( f ( x ) ) (g \circ f)(x) = g(f(x)) .
See also
Revision on April 25, 2022 at 18:07:28 by
Anonymous? .
See the history of this page for a list of all contributions to it.