Homotopy Type Theory extensional dagger 2-poset > history (Rev #2)

Contents

Idea
Definition
See also

Idea

A relational dagger 2-poset where morphisms satisfy the axiom of extensionality.

Definition

An extensional dagger 2-poset $C$ is a relational dagger 2-poset with a term

p:\prod_{A:Ob(C)} \prod_{B:Ob(C)} \prod_{R:Hom(A,B)} \prod_{a:El(A)} \prod_{a^{'}:El(A)} \prod_{b:El(B)} \prod_{b^{'}:El(B)} (R(a,b) \times id_A(a,a^{'}) \times id_B(b,b^{'})) \to R(a^{'},b^{'})

See also

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