Homotopy Type Theory
relational dagger 2-poset > history (Rev #2)
Contents
Idea
A dagger 2-poset with elements with a good notion of relation comprehension of morphisms and elements.
Definition
A relational dagger 2-poset C C is a dagger 2-poset with elements 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 ) ( S ∘ R ) ( 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 May 18, 2022 at 16:25:19 by
Anonymous? .
See the history of this page for a list of all contributions to it.