The identity type weak factorisation system

Details The identity type weak factorisation system The identity type weak factorisation system

2008-03-31

arxiv.org/abs/0803.4349v2

Theoretical Computer Science 409 (2008), no. 1, 94--109

Mathematics

Logic

25 pages; accepted for publication in Theoretical Computer Science

Scientific paper

10.1016/j.tcs.2008.08.030

We show that the classifying category C(T) of a dependent type theory T with
axioms for identity types admits a non-trivial weak factorisation system. We
provide an explicit characterisation of the elements of both the left class and
the right class of the weak factorisation system. This characterisation is
applied to relate identity types and the homotopy theory of groupoids.

Affiliated with

Also associated with

No associations

Rating

The identity type weak factorisation system does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with The identity type weak factorisation system, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and The identity type weak factorisation system will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-196866