Homotopy Type Theory relational dagger 2-poset > history (Rev #1, changes)

Showing changes from revision #0 to #1: Added | Removed | Changed

Contents

Idea

A concrete dagger 2-poset? with a good notion of relation comprehension of morphisms and elements.

Definition

A relational dagger 2-poset CC is a concrete dagger 2-poset? such that for objects A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C) and for morphism R:Hom(A,B)R:Hom(A,B) and elements a:El(A)a:El(A) and b:El(B)b:El(B), there is a type R(a,b)R(a,b) with a term p:isProp(R(a,b))p:isProp(R(a,b)), and an identity

q: A:Ob(C) B:Ob(C) D:Ob(C) R:Hom(A,B) S:Hom(B,C) a:El(A) d:El(D)(SR)(a,d)=[ b:El(B)S(b,d)×R(a,b)]q:\prod_{A:Ob(C)} \prod_{B:Ob(C)} \prod_{D:Ob(C)} \prod_{R:Hom(A,B)} \prod_{S:Hom(B,C)} \prod_{a:El(A)} \prod_{d:El(D)} (S \circ R)(a, d) = \left[\sum_{b:El(B)} S(b,d) \times R(a,b)\right]

See also

Revision on April 25, 2022 at 20:35:59 by Anonymous?. See the history of this page for a list of all contributions to it.