Jacob Frey -> Jonas Frey

Anonymouse

]]>Adding reference

- Steve Awodey, Jacob Frey, and Sam Speight. “Impredicative Encodings of (Higher) Inductive Types”. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. LICS ’18. Oxford, United Kingdom: ACM, 2018, pp. 76–85. (ISBN:978-1-4503-5583-4, doi:10.1145/3209108.3209130)

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:

- Kajetan Söhnen,
*Higher Inductive Types in Homotopy Type Theory*,Munich (2018) [pdf]

added pointer to:

]]>added pointer to:

- Andrea Vezzosi, Anders Mörtberg, Andreas Abel, §4 in:
*Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types*, Proceedings of the ACM on Programming Languages**3**ICFP 87 (2019) 1–29 [doi:10.1145/3341691, pdf]

to the item

- Guillaume Brunerie,
*Implementation of higher inductive types in HoTT-Agda*(2016) [github]

I have added the label

(deprecated)

and added instead pointer to:

]]>this link in the entry doesn’t work for me:

- Michael Rathjen,
*Homotopical Inductive Types*

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

- Magnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg, Andrea Vezzosi,
*Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks*(arXiv:2102.01969)

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.)

]]>