Naïm Camille Favier

PhD student at Chalmers interested in univalent foundations, category theory and music.

Public Key

npub1avwd5p4zn7ndkvjf9qtrsddacax0cvmujryu2qnlxcm6nmlnquwqxz5z7z

NIP-05 Address

ncf@types-pl.mostr.pub

Profile Code

nprofile1qqswk8x6q63flfkmxfyjs93cxk7uwn8uxd7fpjw9qflnvdafalesw8qpz4mhxue69uhhyetvv9ujuerfw36x7tnsw43qz9thwden5te0wfjkccte9ekk7um5wgh8qatz55yrj6

Publishing to

relay.ditto.pub

relay.mostr.pub

Author Public Key

npub1avwd5p4zn7ndkvjf9qtrsddacax0cvmujryu2qnlxcm6nmlnquwqxz5z7z

Show more details

Last Notes

2026-02-20 12:12:16 UTC

- reply

@nprofile…tn9h Oui, le premier est "pas de réponse aux fascistes", le second est "réponse violente". Je parle justement du middle ground entre les deux: réponse pacifique. Est-ce qu'on a des exemples dans l'histoire où ça a marché ? (Je ne sais pas hein, mais c'est la question qu'il faut se poser avant de pouvoir tirer des conclusions, à mon avis.)

2026-02-20 12:04:24 UTC

- reply

@nprofile…tn9h Mais est-ce que la réponse pacifique aux fascistes est historiquement documentée comme une vraie bonne idée ? Sinon on n'est pas plus avancés.

2026-02-09 13:08:08 UTC

- reply

@nprofile…xuzd I'm TAing a proof theory course that uses the book "Structural Proof Theory" and sharing a lot of these feelings at the moment... How can a book published 16 years ago already be so outdated‽
It also does this weird thing where the weight of a formula is defined as its symbol count except that ⊥ counts for 0, so when doing induction on the weight of a formula you have to special case nonsense like ⊥ → ⊥... Way to invent complexity where there is none.

2026-01-28 23:55:38 UTC

- reply

@nprofile…xuzd @nprofile…j8gu @nprofile…htrj @nprofile…xdkd @nprofile…t6k2 Out of curiosity, is there a reason you couldn't formalise them in Agda with --two-level?

2026-01-27 11:33:56 UTC

- reply

@nprofile…t6k2
@nprofile…xdkd and others are right: equality reflection (as a defining component of equality types) doesn't confuse language and metalanguage, but reflects one in the other; to some extent this is what all type formers (but certainly at least the negative ones) do (you could say that the positive ones, like identity types, do it in a different way). Universes reflect the metalanguage judgement "A is a (small) type" into the language judgement "A : 𝒰", etc. I find that section 2.4 of Principles gives an enlightening perspective on this.

2026-01-26 18:49:45 UTC

say you have "equality types" with refl and equality reflection (if p : Id A a b then a = b : A) but nothing else. you could consider adding
\0. nothing
the negative η rule for Id, which says that p = refl : Id A a a for all p : Id A a a
the J eliminator (seeing Id as a positive type) with β and η rules
the J eliminator with β but no η
i'm trying to work out the relationships between these. i think:
2 implies 1 (nLab)
1 implies 2 (easy, exercise 4.2 in Principles)
2 implies 3 (obviously)
but does 3 imply {1, 2}? i.e. if you add equality reflection to identity types do you get equality types? i know you get axiom K, which is a propositional version of 1, but do you get the judgemental version?
(i don't think 0 implies any of them: without J or p = refl you can have multiple equality proofs witnessing the same judgemental equality (say Id A a b is ℕ if a = b, ⊥ otherwise))
ping @nprofile…j77f it's your fault i'm thinking about this

2026-01-22 18:11:46 UTC

the ACM DL added a cover page to our paper (why?) with the wrong affiliations (again, after we corrected them something like 5 times during the publication process). they for some reason also added the region (Västra Götaland), but spelt it without accents (Vastra Gotaland, which I guess must sound really funny to a Swede). why?? how hard is it to copy and paste a $!@#* text field??? you have one job????

2026-01-13 16:14:40 UTC

ACM is asking me to complete a survey about my publication experience and i can't even tell them how disastrous it has been because the survey is a 404 👌

2026-01-06 16:50:53 UTC

- reply

@nprofile…a3ey Is the author on Mastodon? The dual construction with Π-types also works, so it seems like one doesn't even need Σ-types.
It would be interesting to analyse what's going on here categorically. Smells like Kan extensions but I can't put my finger on it.

2025-12-03 21:32:35 UTC

- reply

@nprofile…w8t5 @nprofile…qp4w So, if I understand correctly, there are inclusions
ℕ∞ ⊆ Σ𝓛 ℕ ⊆ Ω𝓛 ℕ
(where Σ𝓛 / Ω𝓛 is the lifting monad for Rosolini propositions / all propositions), with both inclusions a priori strict constructively, and the elements in the image of the first inclusion are the sharp elements?

2025-12-03 21:19:23 UTC

- reply

@nprofile…dand As in https://martinescardo.github.io/papers/partial-elements-and-recursion.pdf. I think some choice might be required for it to actually form a monad, but I don't need that.

2025-12-03 20:57:05 UTC

What is the relationship between 𝓛 ℕ and ℕ∞, where 𝓛 is the Rosolini lifting monad and ℕ∞ is the conatural numbers? More generally, can "one-point compactification" be expressed type-topologically?
(ping @nprofile…w8t5)

2025-11-24 19:53:41 UTC

- reply

@nprofile…rrqe @nprofile…d7hz Yeah, that's why I said free. Maybe-algebras are just normal pointed sets

2025-11-24 19:50:07 UTC

- reply

@nprofile…rrqe @nprofile…d7hz Fair point. I guess I would call it a free Maybe-algebra or something then

2025-11-24 19:29:30 UTC

- reply

@nprofile…d7hz Isn't the type of such things equivalent to the type of sets, via coproduct with 1? If so, why not just call it a set? :)

2025-10-18 13:24:28 UTC

@nprofile…rrqe In your note on algebraic type theory you mention the "Lindenbaum-Tarski model generated by the raw syntax of pure MLTT without connectives". Just to be sure, this model is trivial, right? There are no types, so the only context is the terminal one.

2025-10-15 19:23:21 UTC

how easy is it to switch Mastodon instances? can i send all my toots over?

2025-10-15 15:03:06 UTC

- reply

@nprofile…rrqe @nprofile…dand Yeah, I still see people insisting on learning type theory from books that use the lambda cube. It's a sad state of affairs.
(Related discussion in this previous thread.)

2025-10-15 14:22:52 UTC

Is the Wikipedia page on the calculus of constructions wrong? It seems to present a type theory with Prop : Type and where both are impredicative, while also claiming that this is consistent...
(ping @nprofile…dand since you seem to be on an editing roll)

2025-09-07 00:08:18 UTC

- reply

@nprofile…6kk0 I've learned enough to answer (or perhaps unask) my own question now.
In the context of algebraic (finite products) theories, this is kind of obvious: initial models and theories are not even the same type of objects. For example, the theory of a group can be given as a finite-products category whose objects are natural numbers n representing contexts of the form x₁, …, xₙ : G and whose morphisms are substitutions in the language of groups (equivalently, this is the opposite of the category of finitely generated free groups); or as a finite-limits category (essentially algebraic theory) whose objects are contexts built from assumptions of the form x : G and equational assumptions (equivalently, the opposite of the category of finitely presented groups); or as a topos, etc. All of these are in a sense the "free category with {some structural stuff} and a group object", and in that sense they are initial structured-categories-with-a-group-object. But the initial model in sets is just the trivial group, which bears no relation to any of this.
Another example, which more closely addresses my confusion, is in the context of Uemura's framework for type theories. In the spirit of functorial semantics, a type theory is defined as a (small) category with representable maps, where each object encodes a form of judgement and the representable maps pick out the judgements that can be hypothesized; a model of 𝕋 is then a functor from 𝕋 to a representable map category, with the "natural" class of models being restricted to presheaf categories.
We can then look at a very concrete example: the "basic dependent type theory" 𝕋 with a "type" judgement ⊢ A, a representable "term" judgement ⊢ a : A over that, and nothing else; that is, the representable map category freely generated by a single representable map. This turns out to have a description as the opposite category of the category of finite GATs, which is far from trivial. On the other hand, the initial model of this theory is (I think) trivial: its base category is the full subcategory of 𝕋 on the objects whose map into 1 is representable, i.e. the "closed" forms of judgement that are hypothesizable; but the only such thing is the trivial judgement 1, since you can't hypothesize a type and you need a type to hypothesize an element. So the initial DTT-model is just the empty function ∅ → ∅ in Set (which is vacuously a representable map of presheaves over 1).

2025-08-25 18:41:33 UTC

- reply

@nprofile…hszg all of them

2025-08-25 18:16:21 UTC

is the existence of an isomorphism ℝ ≃ ℝ + 1 equivalent to WLPO? (question intentionally vague)

2025-08-05 21:57:37 UTC

- reply

@nprofile…6kk0 which meaning of "twist" is that referring to?

2025-08-05 21:49:08 UTC

does anyone know why the twisted gluing category (of Altenkirch, Hofmann & Streicher) is called twisted? looks pretty straight to me

2025-08-03 19:20:31 UTC

Is there an "established" name for the construction in HoTT that associates to every 1-type A the category with A as objects and paths as morphisms, i.e. turns a groupoid (type) into a groupoid (category)?

2025-07-27 11:29:19 UTC

- reply

@nprofile…6kk0 What should I read in order to understand this? Something by Uemura, I assume? Is there a simple example from algebra that illustrates the difference?
I'll admit the only definition of "syntactic category" I know is the one from the nLab, which looks a lot like an initial model to me.

2025-07-06 20:40:58 UTC

- reply

(Paper A was apparently revised after paper B was written)

2025-07-06 20:39:52 UTC

I'm reading papers about recursion and paper A is like "paper B did foo" so I go to check paper B and it's like "paper A did bar"... does this have a fixed point

2025-07-06 15:03:04 UTC

- reply

@nprofile…hszg (re (2): you now get unqualified constructors that might not typecheck, so the issue isn't fixed, but this scenario should at least be less common)

2025-07-04 16:18:22 UTC

I just realised that one can do the Tarski vs. Russell universe dance one rung up (down?) the dependency ladder, about universes themselves: are universes and universe levels the same thing or do you have an explicit decoding family U : Level → Type?
So, do you like your universes à la Russell à la Russell or à la Tarski à la Tarski?

2025-07-04 11:42:47 UTC

Does anyone know how to make sense of the following, from section 3.2 of "The independence of Peano's fourth axiom…":
The W-introduction rule in [4] does not have a bottom clause 0 ∈ (Wx ∈ A)B(x) since such a clause can be derived using a universe. We can now see that this use of a universe is necessary.
The W-introduction rule in the referenced Martin-Löf paper is the standard one: from a : A and b : B(a) → W A B, get sup(a, b) : W A B.
What on earth is a "bottom clause", and why would such a thing be derivable with a universe? If this means adding a premise that W A B is inhabited to the W-introduction rule, then wouldn't the new rule be trivially derivable by ignoring the premise?

2025-07-02 15:08:24 UTC

- reply

@nprofile…6kk0 @nprofile…tphs @nprofile…9vrk Would some kind of descent condition help at all? That's how I think about large elimination, but I don't know if that's what you're looking for.

2025-07-02 09:49:17 UTC

- reply

@nprofile…6kk0 @nprofile…hszg Wouldn't a preorder have 0 = 1?

2025-07-01 20:31:08 UTC

- reply

@nprofile…hszg @nprofile…lgwr No, since positive-not-zero uses universes.

2025-07-01 20:20:19 UTC

- reply

@nprofile…hszg MLTT has canonicity, right? So to prove 0 = 1 or 0 ≠ 1 you really have to prove one or the other. Which one? You would have to pick 0 = 1 in one model and 0 ≠ 1 in another.

2025-07-01 20:14:43 UTC

- reply

@nprofile…hszg The natural numbers don't have decidable equality without universes, since 0 ≠ 1 is independent. Nice try! :)

2025-07-01 18:03:21 UTC

It's known that 0 ≠ 1 is independent from MLTT without universes. Can the same be said about the fact that 0 = 0 is contractible? The same countermodel doesn't work, because there everything inhabited is contractible. Maybe some kind of — × S¹ translation?

2025-06-24 09:56:34 UTC

- reply

@nprofile…hszg I don't think you can: this seems to require at least (-2)-univalence ("all contractible types in 𝓤 are equal") (see also this answer by @nprofile…2pts ; I don't know if either of you inspired the other).
As a counterexample, consider the Tarski universe with two distinct unit types and nothing else, 𝓤 = (2, λ _ → ⊤). This is clearly not univalent, nor even (-2)-univalent, but it can be closed under Σ and Id in such a way that χ and τ are fibrewise inverses (where τ is the map assigning total spaces to functions into 𝓤).
To see this, note that closing 𝓤 under Σ amounts to choosing a function σ : 2 × 2 → 2, while closing 𝓤 under Id amounts to choosing a function ι : 2 → 2. Then, under the obvious identifications (⊤ → 2) = ((X : 2) × ⊤ → ⊤) = 2, we have
χ Y X = σ X (ι Y)
τ Y X = σ Y X
Thus the two maps can be made into fibrewise inverses of each other by choosing ι to be the identity and σ to be XOR.
The question in your first post is even easier to refute, as it doesn't ask that χ or τ be a fibrewise equivalence; only that there is some fibrewise equivalence. We can even find a counterexample that satisfies (-1)-univalence: take 𝓤 = (ℕ, Fin). This is not univalent (because it is a set and contains the booleans), but it is (-1)-univalent, and the domain and codomain of χ Y are both countably infinite when Y > 0 and equal to 1 when Y = 0, so they are fibrewise equivalent.
Of course, χ can't be a fibrewise equivalence since that would imply that ℕ is univalent; the cardinality of the fibre of χ Y at a function f : Fin Y → ℕ seems to be the multinomial coefficient of f.
(@nprofile…ujms @nprofile…4vq9 can you check that I'm not bullshitting too much?)

2025-06-10 15:15:46 UTC

I've been reading the paper on small induction-recursion (which is really well-written btw!) and I think there might be a similar kind of terminological thingy about induction-recursion as with the "type-theoretic axiom of choice".
For context, "type-theoretic axiom of choice" is an old name for the distributivity of Π over Σ, which has nothing to do with choice. The reason it's named that is that, if you interpret ∀ as Π and ∃ as Σ, the first-order formulation of the axiom of choice in terms of relations
(∀ (x : X). ∃ (y : Y). R(x, y)) → (∃ (f : X → Y). ∀ (x : X). R(x, f(x)))
is just the distributivity of Π over Σ, which is trivial. The real mathematical content of the axiom of choice in type theory comes from the distributivity of Π over the propositional truncation, since the correct interpretation of ∃ x. P x is ∥ Σ x. P x ∥.
Similarly, "induction-recursion" is made up of two parts: small induction-recursion, which is equivalent to indexed inductive definitions and thus rather anodyne, and the resizing of those definitions so that they live in U when they should live in U⁺, which is where the expressive power of IR comes from.
So, while "type-theoretic axiom of choice" is a very strong name for something innocuous, "induction-recursion" is an innocuous name for something very strong, essentially for dual reasons.
I hope this is not too obvious; I sure wish someone had explained this to me the first time I learned about induction-recursion.

2025-05-31 14:36:21 UTC

- reply

@nprofile…hszg I've added a sentence to "subterminal object".

2025-05-31 14:14:15 UTC

Funny observation: a subterminal object is just an idempotent comonoid in a cartesian monoidal category (what's the problem?).

2025-05-21 16:55:25 UTC

What do you get if you interpret "f : A → B is surjective" (∀ b : B. ∃ a : A. f(a) = b) in the internal language of a [whatever adjectives you need to make sense of that statement] category? I think the existential should be interpreted as the inclusion im f → B in a regular category, so the ∀ should give you a section of that? What flavour of epimorphism is this?

2025-05-20 20:28:16 UTC

- reply

@nprofile…hszg (System T has higher-order primitive recursion, which is strictly more powerful than primitive recursion.)

2025-05-10 12:50:40 UTC

I am once again thinking about the terminological mess that are lifted/created limits. Definitions:
F : A → B lifts limits of a diagram D : J → A if, assuming F ∘ D has a limit in B, then D has a limit in A and F preserves this limit.
F : A → B creates limits of D if it lifts limits of D and also reflects them.
F lifts/creates limits of shape J if it lifts/creates limits of all diagrams J → A.
Now, some authors write things like "F creates all limits that exist in its codomain" (say, if F is a monadic functor for example). But, if you take the definition above, the side condition "that exist in its codomain" is redundant! Indeed, the whole definition of "creates limits of D" can be put in the form "assuming F ∘ D has a limit in B, then […]", so it already only applies to limits that exist in B.
I suspect that the reason people say things like that is because there is another definition in circulation (actually, I can only find it on the nLab…): F : A → B creates limits of D : J → A if F preserves and reflects limits of D and, if F ∘ D has a limit in B, then D has a limit in A. This definition is not equivalent to the definition above, because "F preserves limits of D" does not assume that F ∘ D has a limit.
As an example, let A be a category with a terminal object, B be a category without a terminal object, and F : A → B a functor. Then F (vacuously) creates terminal objects (according to the first definition above), but F doesn't preserve terminal objects. On the other hand, F vacuously preserves the terminal objects that exist in B, so I guess it is also natural to say that F creates terminal objects that exist in B.

2025-04-13 14:10:26 UTC

- reply

@nprofile…6kk0 OK, that answers my first question :)
I am familiar with that book; I was mainly looking for references on GATs, and your second paper seemed like an approachable one (but I will disregard the first one).

2025-04-13 13:58:30 UTC

@nprofile…6kk0 in oktt you write
The most well-adapted way to add a universe is in the Tarskian style; universes à la Russell should be understood as a matter of elaboration, definitely not as a matter of semantics.
and in Algebraic Type Theory and Universe Hierarchies you write
It is commonly believed that algebraic notions of type theory support only universes à la Tarski, and that universes à la Russell must be removed by elaboration. We clarify the state of affairs […]
What's the story here? Did you change your mind, or am I missing the point and this is not actually a contradiction? I'm not sure what the chronological relation is between the two papers.
Also, in the latter paper you write
concrete computerized implementations of type theory tend to be much closer to the abstract syntax of the initial cwf than to the “raw” syntax which some have insisted is a primary object of study.
Did you have anything specific in mind? Is this about NbE?

2025-03-17 19:53:22 UTC

I recently discovered that Agda's @0/Erased modality for runtime irrelevance (see the docs, or Danielsson 2019 for a more detailed treatment) is an open modality (in the sense of Modalities in homotopy type theory, corresponding semantically to open subtoposes).
That is, one can prove (assuming function extensionality) that Erased A is equivalent to the function type Compiling → A, where Compiling is the following inductive type:
data Compiling : Type where
@0 compiling : Compiling
(and, over this equivalence, if A : Erased Type then Erased A is equivalent to the dependent function type (c : Compiling) → A c).
This is because Agda considers clauses that match on erased constructors as erased, so that pattern matching on the erased constructor compiling is equivalent to copattern matching on the erased field of the Erased record type.
I think this is pretty neat, because we get a bunch of theory for free: for instance, every open modality ○ has an associated closed modality ●, which we can define in Cubical Agda as the following higher inductive type:
data ●_ (A : Type ℓ) : Type ℓ where
η● : A → ● A
@0 tip : ● A
@0 cone : (a : A) → η● a ≡ tip
Whereas ○ A trivialises A's runtime information, one can think of ● A as the complementary operation that glues all of A together at compile time but leaves the runtime part unchanged.
I've formalised these things here, as well as proved an "Artin gluing" theorem that says that any type A can be reconstructed from its compile-time part ○ A and its runtime part ● A in a suitable sense.
This seems pretty closely related to some of the synthetic Tait computability stuff by @nprofile…6kk0. In particular in Logical relations as types a similar open modality is used to express some kind of phase distinction between static and dynamic things. I wonder how precise the relationship can be made.
I am also wondering if there is a nice semantic place in which to make sense of all this. For example, it seems like we could interpret Compiling in a category of assemblies as the assembly with singleton carrier and no realisers, but this is disallowed by the definition of assemblies which requires every element to have at least one realiser. Is there a good reason for this restriction? (@nprofile…r8sr do you know?)
Also pinging @nprofile…hszg because of some of your comments here: maybe this suggests that a suitable axiomatisation of computational erasure (at least of the kind under discussion here) is simply a proposition C, possibly such that ¬¬C holds if we want ⊥ to be modal (corresponding to the ability to pattern match on erased arguments of the empty type).
(Sorry for the long post 😅)

2025-01-19 20:37:12 UTC

- reply

@nprofile…e5g0 No statement in T can be proven to be unprovable within T, because that would imply T's consistency.