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

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

Contents

Idea

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

Definition

An extensional dagger 2-poset CC is a relational dagger 2-poset with a term

p: A:Ob(C) B:Ob(C) R:Hom(A,B) a:El(A) a :El(A) b:El(B) b :El(B)(R(a,b)×id A(a,a )×id B(b,b ))R(a ,b )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 19, 2022 at 01:03:00 by Anonymous?. See the history of this page for a list of all contributions to it.