Jacob Frey -> Jonas Frey
Anonymouse
]]>Adding reference
Anonymouse
]]>added these pointers:
Henning Basold, Herman Geuvers, Niels van der Weide, Higher Inductive Types in Programming, Journal of Universal Computer Science 23 1 (2017) 63-88 [pdf, slides pdf]
Niccolò Veltri, Niels van der Weide, Constructing Higher Inductive Types as Groupoid Quotients, Logical Methods in Computer Science 17 2 (2021) [arXiv:2002.08150doi:10.23638/LMCS-17(2:8)2021]
added pointer to:
added pointer to:
added pointer to:
to the item
I have added the label
(deprecated)
and added instead pointer to:
]]>this link in the entry doesn’t work for me:
In any case, I gather that it points not to a writeup but to a research grant landing page, and so I have clarified that in the entry.
]]>I have added publication data for these two items:
Kristina Sojakova, Higher Inductive Types as Homotopy-Initial Algebras, ACM SIGPLAN Notices 50 1 (2015) 31–42 [arXiv:1402.0761, doi:10.1145/2775051.2676983]
Steve Awodey, Nicola Gambino, Kristina Sojakova, Homotopy-initial algebras in type theory, Journal of the ACM 63 6 (2017) 1–45 [arXiv:1504.05531, doi:10.1145/3006383]
and added a cross-link with initial algebra over an endofunctor
]]>Adding reference
Anonymous
]]>in the example item for the circle (here), I added the actual references
]]>Added a section linking to and listing examples from quotient inductive type.
]]>It would be more helpful for the change message to indicate what exactly was moved. It appears that what was moved was all the examples of HITs that are also QITs, except for set-quotients. While those examples should certainly be at quotient inductive type, I think it’s also helpful to at least list them at higher inductive type.
]]>moving to quotient inductive type
Anonymous
]]>Does the interval as truncation of the booleans have anything to tell us about cubical type theory?
The main novelty of cubical type theory is to move the interval (and other things) into the primitive syntax. So it is a kind of strictification/rigidification, and the result you are referring to could perhaps be viewed as partial indication that this is reasonable.
]]>Does the interval as truncation of the booleans have anything to tell us about cubical type theory?
]]>“booleans” is a pretty standard name for the 2-element type. Especially if it is hyperlinked, I don’t think there is a problem with using it.
]]>Here is Martins email:
]]>My post showing that ||2|| has the universal property of the interval (judgementally for the first order equations and propositional for the second order equations) was in this thread, back in July: https://groups.google.com/forum/#!topic/homotopytypetheory/KyJZKbbr1SM
The proof is easy and short. The only trick is to come up with a suitable proposition to work with.
Assume a type two with points 0,1:2, and let ||-|| denote the (-1)-truncation.
Define I = ||2||, and let seg : |0| = |1| the path arising from the definition of ||-|| (I call it the “truncation path”).
The end-points of I are taken to be |0| and |1|, of course.
Given points x0,x1:X and a path p:x0=x1, we wish to build g:I->X such that g|0|=x0 and g|1|=x1 (judgementally), and ap g seg = p (propositionally).
The trouble is that X is not assumed to be a proposition, and hence the recursion principle for ||-|| can’t be used.
So work instead with paths-from x0, i.e. Sigma(x:X).x0=x, which is a proposition.
Now define f:2->paths-from x0 by
f 0 = (x0, refl) f 1 = (x1, p)
By the recursion principle for ||-||, f “extends” to g’:||2||->paths-from x0.
Now define g:||2||->X to be g’ composed with the first projection, which I call “endpoint” in this discussion.
You can check that g|0|=x0 and g|1|=x1 judgementally, by simply expanding the definitions (or with Agda, as the proof refl is accepted).
The proof that ap g seg = p is equally easy. It suffices to consider x0,x1 the same, say x, and p=refl x, in a proof by induction.
We have, in this case,
ap g’ seg = refl (x,refl x),
using the fact that ||2|| is an proposition and hence an set.
Applying the first projection (called “end-point”) to this path, we get
ap end-point (ap g’ seg) = ap end-point (refl (x,refl x)),
Now the lhs is equal to
ap (end-point o g’) seg
and in turn, by the definition of g, to
ap g seg.
And the rhs is refl by the definition of ap. Putting this together, we get
ap g seg = refl
and our proof by induction is complete. Q.E.D.
Moreover, it is known that recursion on I gives induction. However, as far as I know, it doesn’t give it judgementally. Hence in the Agda file I also include a proof that the induction principle for the interval does hold judgementally if we take I=||2||.
Additionally, the above proof technique can be used to show that if a function f:X->Y factors through |-|:X->||X||, then we can find a judgemental factorization. Also in that file. Nicolai then used this to define his mysterious pseudo-inverse of |-|:X->||X||.
To conclude, here is an observation. We discussed constancy (many times) in this list.
Mike’s definition is that f:X->Y is constant iff we are in possession of y:Y such that f=\lambda x.y. Let’s adopt this terminology. (In the Agda file I call this “constant-valued”.)
It is easy to see that f:X->Y has a factor through |-|:X->||X|| iff ||X||->constant f.
Martin
Concerning #67, I would argue that “2 element type” is clearer than “booleans”.
]]>Worth a word on how it can be used to prove functional extensionality from propositional truncation?
]]>interval as truncation of the booleans.
]]>I don’t think that database idea has become a reality yet. But all the more will it help if we format all our references uniformly now, for then there will be a chance to automatically collect them into a database later!
]]>Thanks. I had overlooked that.
I seem to recall that Richard also implemented a feature for a general citation database, but it does not appear to be in the HowTo.
]]>Hi Bas,
please check out How to cite and record references.
(It’s not just a formality: If you care about the references you give, anchoring and linking them means that readers will be more likely to open them.)
]]>