Naïm Camille Favier

icon indicating a website link https://monade.li icon indicating an email [email protected]

icon company Chalmers University of Technology icon location Sweden icon location aka ncf. PhD student working on cubical type theory.

Results 245 comments of Naïm Camille Favier

fix: Checks if message body is NULL before getting number of children.

This fixes https://github.com/altdesktop/playerctl/issues/339 for me.

Presheaf categories are locally cartesian closed.

> Is there a better way to do this? You can use the fact that limits are unique in univalent categories. This will probably compute worse, but computation is going...

Non-infectiveness of --level-universe breaks subject reduction

For what it's worth I think it's a good idea to be as fine-grained as we can with universe features. Our paper only shows that there are no "concrete problems"...

__IMPOSSIBLE__ in Agda.TypeChecking.Substitute.piApply (again)

Beat me to it!

Section 4.8

Unfortunately I think there are more issues in that section... The definition of a predicate p : Pred(S) being "classified by" a map S → T is subtly wrong: the...