Trebor

PhD student at IUB interested in type theory and music and stuff

Last Notes

2026-01-26 22:15:18 UTC

- reply

@nprofile…t6k2 In some sense, the eta law for pairs allows us to confuse metalanguage pairs with pairs in the object language, because you can deconstruct and construct pairs any time you want. I guess this is fine because pairs are tame?

2025-12-18 23:17:38 UTC

- reply

@nprofile…dand https://liamoc.net/posts/2015-09-10-girards-paradox/index.html is a formalization of Russell's paradox (despite claiming to be Girard's paradox in the url)

2025-12-18 23:14:14 UTC

- reply

@nprofile…dand Yes, but that is not a version of Russell's paradox anymore.

2025-12-18 22:52:36 UTC

Do we know any version of Russell's paradox with type-in-type and only Pi and Sigma types? If not, what if we allow the identity type with UIP?

2025-12-15 20:40:30 UTC

- reply

@nprofile…3zl5 This is one of the most profound things about 2-category theory --- adjunctions are purely diagrammatic, and so is preserved by anything whatsoever

2025-12-07 01:23:22 UTC

Does cumulativity necessarily imply the rule |- A = B : Un ===> |- A = B : U(n+1)? I feel like in typed conversion we don't have to add it.

2025-12-02 00:59:45 UTC

- reply

@nprofile…dand Now that I think of it, eta for unit types seems really bad for rewriting systems. Do we define a family of reductions, one for each type? Otherwise an untyped reduction can only turn the constructor of Unit into a (fresh) variable, because no other direction makes sense. But then confluence is dead. (I'm assuming eta because this thread is specifically about eta.)

2025-12-02 00:50:07 UTC

- reply

@nprofile…dand Sure. I'm taking unadorned "normalization" to mean "everything has a normal form", where normal forms are mutually inductively defined with the neutral forms, instead of being the terms with no reductions. This makes it so eta for unit types and other things slightly less annoying.

2025-12-02 00:28:59 UTC

- reply

@nprofile…dand The univalence axiom doesn't normalize. Although the Licata trick should be enough to guarantee as many good properties as [MLTT + any postulates]

2025-11-15 01:55:46 UTC

Funny simulation of label types in Agda, so that the eliminator-based definitions never show up in the goals.
https://pool.jortage.com/typespl/media_attachments/files/115/551/218/433/182/401/original/36e6e19e3831c2b2.png

2025-05-22 13:58:03 UTC

- reply

@nprofile…hszg So you can't recover an inductive characterization because this form is no longer the impredicative encoding of some inductive type. Could an investigation of "non-positive" impredicative encodings shed some light on this?
For example, attempting to encode (µX. X → X) will fail because it is not positive, but the result is an interesting type with natural decomposition T = 0 + 1 + 2 + 3 + .... See https://cstheory.stackexchange.com/questions/53855

2025-04-20 14:00:28 UTC

It seems to me that in the category of assemblies, the propositions (underlying set has at most one element), modest sets (every realizer realizes at most one element), and kappa-small assemblies with kappa some large cardinal, are all universes as a model of type theory? The former two seems to be closed under large Pi types, but doesn't this give you a model of system U? Where's my mistake?

2025-04-20 09:03:57 UTC

- reply

@nprofile…6kk0 Ah, so from the perspective of the quotient inductive type, the input should be a map f equipped with an inverse to the structure morphism from dom(f) to the pullback of f with itself, and the output is a name in the subobject classifier. If I understand correctly, this applies when all kernel pairs exist?

2025-04-20 08:31:15 UTC

https://mathoverflow.net/questions/491348/free-categories-involving-subobject-classifiers

2025-02-17 02:13:13 UTC

- reply

@nprofile…6kk0 The go to example for me is "the language { 111...111 | this appears in the decimal expansion of pi } is regular". We don't know what's the algorithm, but we know there exists a FSA for it.