* trivial cofibration-fibration factorization
@ 2017-07-06 20:09 Thierry Coquand
0 siblings, 0 replies; only message in thread
From: Thierry Coquand @ 2017-07-06 20:09 UTC (permalink / raw)
To: homotopy Type Theory
[-- Attachment #1: Type: text/plain, Size: 621 bytes --]
For completeness, I wrote down the details <http://www.cse.chalmers.se/~coquand/afs.pdf> of the trivial cofibration-fibration
factorisation in the cubical set model.
It is interesting to compare this with the “small object argument”.
There is no quotient operations and the argument can instead
be seen as an inductive process which is similar to Petersson-Synek “tree types”
(a.k.a. indexed containers): we define inductively a family of sets indexed by
the object of the base category (and all operations are then defined by induction
of this inductively defined indexed family of sets).
Thierry
[-- Attachment #2: Type: text/html, Size: 1088 bytes --]
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2017-07-06 20:09 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2017-07-06 20:09 trivial cofibration-fibration factorization Thierry Coquand
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).