Categorical logic in Lean? (algebraic theories, etc.)

Stream: maths

[Adrian Marti]

Hi all,

I was wondering whether anyone thought about formalizing categorical logic in Lean. Specifically, I am interested in general definitions for different fragments of geometric logic: algebraic theories, regular theories and geometric theories.

For those not familiar with the subject, let me give you the TL;DR for the mathematics involved. In the same way that in model theory one can define a first-order theory and what its models are, in categorical logic we define theories, but instead of having models be sets equipped with a certain structure, we can consider models in any other category (with sufficient structure).

For instance, one can define a theory of rings and consider models in any category with finite limits. This means that any equation that we deduce in this theory of rings will have validity in any category with finite limits. A related key example are local rings.

In fact, one can go much further than that and define a class of categories in which we can take models of a first-order-theory. Typically though, in this area, we do use something like geometric logic instead of first-order-logic, where classical reasoning (like negation) is not allowed so that we allow models in categories like sheaves over a topological space.

One reason that I think this is interesting to formalize is that it provides us with a way of proving statements in a very general setting, which can have useful consequences in different settings. Things like group objects, ring objects and module objects are considered all the time, and with this there would be no discussions of continuity or naturality of maps like the division map for groups (To be fair, these facts simply follow from composability of morphisms. But I do not know how this, and more complex statements, possibly involving quantification, plays out in the formalized setting).

Perhaps a better reason to play with this, is that that it lets us work synthetically by proving statements in these theories instead of working with specific models. By doing this, we remove questions of typeclass-inference and definitional equality from the problem, and it also opens the door to using ATPs. Of course, working within the constrains of the theory would also be challenging at times (or not possible).

I honestly have no idea of how this would play out :man_shrugging: I do suspect that these ideas might lead to an interesting way to build APIs (using macros to define logical formulas?) or even useful computational procedures, but in the end we really don't know until we try. I would say it's definitely something to explore. Unfortunately, I never got around to starting to look into this in more detail and formulating some less vague applications :sweat_smile: But maybe someone will find this useful or has also had thoughts in a similar direction :)

Generally, I think that if we can prove statements synthetically or by abstract nonsense, this will pay off much more when working on a proof assistant than when working with pen-and-paper.

Side note: This is all related to the theory of classifying toposes. One can also explore formalizing those, but the above is more accessible.

[Robin Carlier]

I have an open PR (#25735, currently gatekeeped by boring stuff about colimits preservation of tensor products) that characterizes sifted categories as those for which the colimit functor preserves finite products. Once it's merged, I plan on adding some stuff related to algebraic theories, following Adámek-Rosicky-Vitale's book, such as the fact that finite-product preserving presheaves on a category with finite coproducts is a free sifted-colimit completion, and basic general fact about algebraic categories.

[Tom de Jong]

There was a TYPES abstract by Kenji Maillard and Yiming Xu on geometric logic in Lean. The slides and recording are available too.

[Adrian Marti]

Thank both of you! This is the sort of stuff I was looking for. I will dig a little deeper into the geometric logic formalization and see what is there. If I find something cool one can do, I might report back!

[Tom de Jong]

It just occurred to me that I could ping @Kyod (Kenyi) and @Yiming Xu (not sure if this is same person as the co-author of the abstract)

[Yiming Xu]

Tom de Jong said:

It just occurred to me that I could ping Kyod (Kenyi) and Yiming Xu (not sure if this is same person as the co-author of the abstract)

Thank you for pinging me! (Moreover, the other one is also me... I was previously at the ANU.)

[Yiming Xu]

Yes I am the one from the LMU. One of the authors. FYI, I am currently formalizing a construction of classifying topos. It is equivalent to, but not quite the same as the one in Johnstone. This is the PhD work of Joshua Wrigley, as outlined here (the topology is defined around 17:00 of the video): https://www.youtube.com/watch?v=jjmAScdm4D4
We are currently working towards an interpretation on sheaf topoi (for sheaves on the site, i.e. just the Grothendieck topoi stuff). Feel free to email or DM me to chat about it.

[Adrian Marti]

Wow, this is great! I will look into your work and if anything arises I will dm you. Just to confirm, is this the correct repo for your ongoing work on formalizing a construction for the classifying topos?

[Yiming Xu]

Yes indeed, but I have something not pushed yet. That was my failure that I did not include the link in my slides.

[Bhavik Mehta]

Let me mention that I formalised some of the above material on toposes 5-6 years ago here: https://github.com/b-mehta/topos. The "What's coming soon?" section is a bit out of date, since 1 and 4 were done and 2 was partially done too. This was attempting to lay the groundwork to formalise my Part III essay on classifying toposes.

[Yiming Xu]

Bhavik Mehta said:

Let me mention that I formalised some of the above material on toposes 5-6 years ago here: https://github.com/b-mehta/topos. The "What's coming soon?" section is a bit out of date, since 1 and 4 were done and 2 was partially done too. This was attempting to lay the groundwork to formalise my Part III essay on classifying toposes.

There are very useful materials that would be beneficial if someone could translate them into Lean4. It would be very ideal if someone encounters this post, sees the hope of getting a neat library for categorical semantics in Lean, and starts working on that. I am very happy to help with that because I think I will use that.

[Adrian Marti]

@Bhavik Mehta Yes, I've run into Lean 3 topos theory repository before!

@Yiming Xu Yeah that would be cool! I want to look at things a bit on weekends, but unfortunately I do not have a big amount resources to dedicate to this :smiling_face_with_tear: .

I also tried to build your repository with lake exe cache get and then lake build, but there are multiple files that do not check. Is this because you do not have the mathlib version pinned or is this just stuff that needs to be fixed?

[Yiming Xu]

Adrian Marti said:

Bhavik Mehta Yes, I've run into Lean 3 topos theory repository before!

Yiming Xu Yeah that would be cool! I want to look at things a bit on weekends, but unfortunately I do not have a big amount resources to dedicate to this :smiling_face_with_tear: .

I also tried to build your repository with lake exe cache get and then lake build, but there are multiple files that do not check. Is this because you do not have the mathlib version pinned or is this just stuff that needs to be fixed?

Yes I understand, it is always challenging to convince oneself to dedicate to something. Just playing around and you can find a bunch of fun possibilities. We can communicate more concretely about this. For example, what I am recently formalizing is supposed to pave the way of reasoning with propositional geometric logic internally. I am interested in digging in that direction as well (I am a fan of seeing things to be put together in a coherent framework, I want to see that but I only have one head so I have not touched anything relevant yet...). In that direction, a whole bunch of interesting topics around locale would be nice to have. (If you would like to explore this direction, perhaps you want to search for "Stone duality" + "classifying topos". ) The other big topic to explore is the construction of classifying topoi (maybe for restricted fragments of logics). The syntactical approach appears to be a canonical thing to do, I do not have time to try, but I want to see, model-theoretic approaches as well. Something like this one https://arxiv.org/abs/1008.3145 .

I have not updated Mathlib in the past two or three months! So this should build with an earlier version I think. Maybe this is the reason... I will check and attempt to fix things in recent days.

[Adrian Marti]

I do not know what best practices are, and maybe someone else can give some input on this, but one idea would be to fix the mathlib version in the lakefile.lean with

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "v4.20.0-rc4"

putting the desired mathlib version where it sais v4.20.0-rc4 (one can also specify a git commit). Then it would make sure that other people are using the intended version (even if the mathlib version is a bit out of date).

I did watch your talk and also Joshua Wrigley's talk and I thought it was quite interesting. I thought that it was pretty cool that you defined the semantics in presheaf topoi and proved the soundness of the Hilbert calculus. I'm still in the process of looking through the formalization though. I also thought it was interesting that you could construct the syntactic site by only taking the morphisms that are substitutions instead of all provably-functional formulas.

About the reasoning with reasoning with propositional geometric logic internally, I am not completely sure what type of result you mean. Is this related to Joshua Wrigley's work? I am aware though, that there is are some really interesting things in the area of duality, (syntax-semantics duality, results concerning representation by topological groupoids) but that may be out of scope for formalization for now :)

One quite fundamental thing I would like to see (lets see when I have some time..) is defining a hierarchy of formulas AlgebraicFormula: RegularFormula: CoherentFormula: GeometricFormula and the analogous hierarchy on properties of categories CartesianCategory: RegularCategory: CoherentCategory: GeometricCategory. Then, the definition of semantics of those formulas in those different categories and possibly a discussion of deduction calculi as you have done (This is an area where one could attempt to write some algorithms!).

When attempting to do this, especially when formalizing, we might expect to have some extra care when defining the semantics. When we work with formulas everything works up to equality, but in the respective categories we are using (co-)limits like pullbacks and coequalizers, where there might be no canonical choices of those and things only hold up to isomorphism (strictness concerns).

I have not looked into how the model-theory-topos repo does this, but perhaps working with presheaves simplifies this, since in presheaves (co-)limits can be computed pointwise.

[Yiming Xu]

I am very happy to see that you would like to see the hierarchy stuff. With my collaborators, we are going to discuss if we should throw time in this direction. I think it would be helpful because you do not need full geometric theory to do useful things. (Thanks to @Fernando Chu for reminding me about that possibility recently.) For example, regular theories are already useful to prove properties about a category. On the other end, we do not have to stop at geometric category. If we have internal HOL (in elementary topoi), then we can even do more.

[Yiming Xu]

Regarding propositional geometric logic stuff, yes it is relevant to Joshua Wrigley's work. I will say it is a bit far, indeed, but not as far as the duality stuff. You are right that this will not be the first thing to try at this stage.

[Yiming Xu]

In Lean we have HasFiniteProduct and ChosenFiniteProduct for instances of category having fin products, we work with the second one, and expect we can work chosen lims/colimits in a similar way. Moreover, I think we have the option of not directly attack geometric categories, but Grothendieck topoi, if we want canonical choice of almost everything? And yes, in presheaves, we did it pointwise.

[Chris Henson]

Maybe this is considered slightly separate, but I have been working on categorical semantics of lambda calculi in Lean. (This will be a major topic of my PhD). It is surprisingly difficult to express the categorical semantics of a concrete representation of a lambda calculus formally. Even for simple types there are issues:

1. In Mathlib, we cannot work with morphisms in Prop without universe lifting
2. If our typing derivations have separate types for contexts and types, we must decide how to translate this to a single type of objects

[Yiming Xu]

Chris Henson said:

Maybe this is considered slightly separate, but I have been working on categorical semantics of lambda calculi in Lean. (This will be a major topic of my PhD). It is surprisingly difficult to express the categorical semantics of a concrete representation of a lambda calculus formally. Even for simple types there are issues:

1. In Mathlib, we cannot work with morphisms in Prop without universe lifting
2. If our typing derivations have separate types for contexts and types, we must decide how to translate this to a single type of objects

Thanks for jumping out and pointing out the directions in type theories. I asked @Kyod about concrete possibilities on topoi from dependent type theories. And the conclusion is that this is a bit far if we want to reach there from our current work.

I am curious though, if it is fine to ask, why would you like different types for (models of?) contexts and (models of?) types?

[Adrian Marti]

Yiming Xu said:

In Lean we have HasFiniteProduct and ChosenFiniteProduct for instances of category having fin products, we work with the second one, and expect we can work chosen lims/colimits in a similar way. Moreover, I think we have the option of not directly attack geometric categories, but Grothendieck topoi, if we want canonical choice of almost everything? And yes, in presheaves, we did it pointwise.

Yes! But when one does this, concerns like are our chosen pullbacks strictly functorial or just functorial up to iso? (pullback-pasting up to iso or up to equality on objects) might come up, which is what my concern is about. I am not entirely sure if this is needed though.

[Adrian Marti]

Chris Henson said:

Maybe this is considered slightly separate, but I have been working on categorical semantics of lambda calculi in Lean. (This will be a major topic of my PhD). It is surprisingly difficult to express the categorical semantics of a concrete representation of a lambda calculus formally. Even for simple types there are issues:

1. In Mathlib, we cannot work with morphisms in Prop without universe lifting
2. If our typing derivations have separate types for contexts and types, we must decide how to translate this to a single type of objects

Typed or untyped?

[Adrian Marti]

Nevermind, it's probably typed.

[Yiming Xu]

We do not need the notion of pullback of presheaves to define semantics on presheaves. But in general, people have criticism on working with equality between functors. So if we want to work with strict equality, we may need to fight against some criticism (but sometimes we have to do it...) we will also encounter relevant heterogeneous equality problems. In this project, we are trying to avoid equality between functors. But personally, since I work with equality between functors on another thing, I personally do not against strict equalities, but I need to be convinced first that they are objectively equalities, and we are not making strong assumptions that will make our development weaker. (i.e. if we define two functors, and they are objectively equal, we have the option of working with equality between functors or equivalence between functors. In this case, I am can take the option of just working with equalities. But I will be careful with assumptions/instances stating "we consider interpretations in a category with chosen limits where pullback-pasting squares are strict.")

[Adrian Marti]

I think that while philosophically, we might want to think of isomorphisms only, I think it is very practical to think of equality and certainly also definitional equality when working in Lean.

Okay, you are right, you do not need pullbacks just to define semantics of formulas/sequents :) But, when defining semantics of substitutions, you would need to use pullbacks, right (and aren't substitutions part of the Hilbert calculus)? Then, you might want (I am not sure if you do) a functoriality property for substitutions: If we apply two substitutions to a formula, we are applying two pullbacks to a formula and maybe we might want strict functoriality (the object given by applying both substitutions in sequence is equal to the object given by applying the composition of the substitutions). Does this come up at all in your soundness proof or is this not relevant? :)

[Chris Henson]

Yiming Xu said:

I am curious though, if it is fine to ask, why would you like different types for (models of?) contexts and (models of?) types?

I mean that there is a mismatch between a typical type signature for typing derivations versus morphisms in a category. Typically in formalized metatheory we have some inductive type of derivations ⊢ : Ctx → Ty → 𝒰, where 𝒰 is some universe. We have separate types for contexts and types for many reasons, ranging from practicality (maybe it is nice to reuse a standard list or multiset type) to conceptually mirroring the fact that one is metatheoretic and the other object level. On the other hand, morphisms in a category should have a single type for objects.

[Yiming Xu]

Adrian Marti said:

I think that while philosophically, we might want to think of isomorphisms only, I think it is very practical to think of equality and certainly also definitional equality when working in Lean.

Okay, you are right, you do not need pullbacks just to define semantics of formulas/sequents :) But, when defining semantics of substitutions, you would need to use pullbacks, right (and aren't substitutions part of the Hilbert calculus)? Then, you might want (I am not sure if you do) a functoriality property for substitutions: If we apply two substitutions to a formula, we are applying two pullbacks to a formula and maybe we might want strict functoriality (the object given by applying both substitutions in sequence is equal to the object given by applying the composition of the substitutions). Does this come up at all in your soundness proof or is this not relevant? :)

I will say people with intention of against functor equalities have philosophy in their mind. But I am not sure if strong assumption can cause problem in practice. I am not familiar with concrete examples, but I have the impression that type theory people can work with crazy elementary topoi, and it is not necessarily true that the pb square is always strict, or people do not care it... (I will appreciate if some one can throw me a concrete example.) It will be better if our work can be useful for such cases as well.

Are you talking about modelling substitutions of formulas? If so, iterated substitution does not occur in proof rules, so the soundness proof is not relevant to this. We do have the definition of interpreting substitutions, this is by pre-compositon (yes, it is also called pullback, but we do not need to have a pullback in Psh to define it).

[Yiming Xu]

Chris Henson said:

Yiming Xu said:

I am curious though, if it is fine to ask, why would you like different types for (models of?) contexts and (models of?) types?

I mean that there is a mismatch between a typical type signature for typing derivations versus morphisms in a category. Typically in formalized metatheory we have some inductive type of derivations ⊢ : Ctx → Ty → 𝒰, where 𝒰 is some universe. We have separate types for contexts and types for many reasons, ranging from practicality (maybe it is nice to reuse a standard list or multiset type) to conceptually mirroring the fact that one is metatheoretic and the other object level. On the other hand, morphisms in a category should have a single type for objects.

If I understand correctly, you mean you need to control the universe level of the type you obtained from a context and the universe level of the context. If so, then I am convinced...

[Chris Henson]

Yiming Xu said:

If I understand correctly, you mean you need to control the universe level of the type you obtained from a context and the universe level of the context. If so, then I am convinced...

This is true if typing derivations live in Type, but not what I was tying to point out. I will try to explain better. Look at this (slightly informal, but standard) diagram:
image.png

We are mapping into some ccc $\mathscr{C}$, taking contexts/types to objects and derivations to morphisms. Look at the object in the upper right. This $\Gamma$ is used as a type in the first derivation $\Delta \vdash \Gamma$ of the composition, then as a context in the proceeding morphism $\Gamma \vdash \tau$.

This does not immediately allow for composition, because the semantics of a derivation has type

$${\llbracket \Gamma \vdash \tau \rrbracket}_{\vdash} : \mathscr{C}({\llbracket \Gamma \rrbracket}_{\mathrm{Ctx}},{\llbracket \tau \rrbracket}_{\mathrm{Ty}})$$

To be able to compose this formally, we need that ${\llbracket \cdot \rrbracket}_{\mathrm{Ctx}}$ and ${\llbracket \cdot \rrbracket}_{\mathrm{Ty}}$ are compatible in the sense that they map to equal objects, and we can then use docs#CategoryTheory.eqToHom to construct an indentity morphism to switch from treating $\Gamma$ as a type to treating it as an object. So our diagram really looks like
image.png

where $\, \, \widehat{\cdot} : \mathrm{Ctx} \to \mathrm{Ty}$ is a function that we prove satisfies the identity ${\llbracket \widehat{\Gamma} \rrbracket}_{\mathrm{Ty}} = {\llbracket \Gamma \rrbracket}_{\mathrm{Ctx}}$

[Adrian Marti]

@Yiming Xu I am really glad to hear that this pullback strictness business does not come up here and I hope it continues not to come up :) I was actually a bit worried haha

[Yiming Xu]

Chris Henson said:

Yiming Xu said:

If I understand correctly, you mean you need to control the universe level of the type you obtained from a context and the universe level of the context. If so, then I am convinced...

This is true if typing derivations live in Type, but not what I was tying to point out. I will try to explain better. Look at this (slightly informal, but standard) diagram:
image.png

We are mapping into some ccc $\mathscr{C}$, taking contexts/types to objects and derivations to morphisms. Look at the object in the upper right. This $\Gamma$ is used as a type in the first derivation $\Delta \vdash \Gamma$ of the composition, then as a context in the proceeding morphism $\Gamma \vdash \tau$.

This does not immediately allow for composition, because the semantics of a derivation has type

$${\llbracket \Gamma \vdash \tau \rrbracket}_{\vdash} : \mathscr{C}({\llbracket \Gamma \rrbracket}_{\mathrm{Ctx}},{\llbracket \tau \rrbracket}_{\mathrm{Ty}})$$

To be able to compose this formally, we need that ${\llbracket \cdot \rrbracket}_{\mathrm{Ctx}}$ and ${\llbracket \cdot \rrbracket}_{\mathrm{Ty}}$ are compatible in the sense that they map to equal objects, and we can then use docs#CategoryTheory.eqToHom to construct an indentity morphism to switch from treating $\Gamma$ as a type to treating it as an object. So our diagram really looks like
image.png

where $\, \, \widehat{\cdot} : \mathrm{Ctx} \to \mathrm{Ty}$ is a function that we prove satisfies the identity ${\llbracket \widehat{\Gamma} \rrbracket}_{\mathrm{Ty}} = {\llbracket \Gamma \rrbracket}_{\mathrm{Ctx}}$

I think I see--you are trying to emphasize on eqToHom stuff. Yes that is very painful, and depend on cases you may want to turn it into HEq to see it looks better, very hard to predict. (I encounter eqToHom a lot for formalizing a model of type theory, but it is not such a problem for formalizing geometric logic semantics.) Thanks for writing and drawing all this for the clarification!

[Yiming Xu]

Adrian Marti said:

Yiming Xu I am really glad to hear that this pullback strictness business does not come up here and I hope it continues not to come up :) I was actually a bit worried haha

I do not think it will come up for the soundness as long as we do not have a proof rule about it. It is a bit hard for me to imagine why would we ever want a proof rule with iterated substitution, maybe it happens in some type theory? Have not encountered such a thing yet. I also cannot predict when it would be used. If I find something suspicious, I will comment on this post to let you know.

[Chris Henson]

@Yiming Xu You're welcome, glad that made sense! Yes, it is essentially an issue about using eqToHom. It seems unavoidable if we do not either alter our derivation typing or use multicategories. Do you have any examples in a public repo where you've worked with models of type theories? I've not tried to use HEq like you suggest and would be interested to see what that looks like.

[Yiming Xu]

Chris Henson said:

Yiming Xu You're welcome, glad that made sense! Yes, it is essentially an issue about using eqToHom. It seems unavoidable if we do not either alter our derivation typing or use multicategories. Do you have any examples in a public repo where you've worked with models of type theories? I've not tried to use HEq like you suggest and would be interested to see what that looks like.

Unfortunately what we find is that it is just unavoidable as well. I mean in proof exploration you may encounter some eqToHom ... >> term >> eqToHom ..., you may want to get rid of too many eqToHoms in your goal, in which case you can try these lemmas with "comp" and "eqToHom" https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/EqToHom.html#CategoryTheory.comp_eqToHom_iff

For instance, you see

heq_eqToHom_comp_iff, heq_comp_eqToHom_iff,
      eqToHom_comp_heq_iff, comp_eqToHom_heq_iff

in
https://github.com/sinhp/groupoid_model_in_lean4/blob/master/GroupoidModel/Groupoids/Sigma.lean
(My collaborators wrote this and I am still getting better on these things.)

[Fernando Chu]

Chris Henson said: ...

Hi, I'm very curious in what the problem is here, could you please help me understand this? What is the the lambda calculus in this picture? I'm in particular not sure what this $\, \, \widehat{\cdot} : \mathrm{Ctx} \to \mathrm{Ty}$ function is supposed to be.

[Chris Henson]

@Fernando Chu This lambda calculus is just STLC, extended with pairs and a unit type. That function takes a context and gives a type such that both have as their semantics the same object in a CCC. Explicitly, it can just map a context to the product of its elements, terminated with the unit type for the empty context.

To rephrase what I say above, the question here is what it means to compose $\Delta \vdash \Gamma$ and $\Gamma \vdash \tau$. If contexts and types are syntactically different entities, $\Gamma$ must be either a context or type (I choose context here), and we need to speak about the composition of

${\llbracket \Delta \vdash \widehat{\Gamma} \rrbracket}_{\vdash} : \mathscr{C}({\llbracket \Delta \rrbracket}_{\mathrm{Ctx}},{\llbracket \widehat{\Gamma} \rrbracket}_{\mathrm{Ty}})$
and
${\llbracket \Gamma \vdash \tau \rrbracket}_{\vdash} : \mathscr{C}({\llbracket \Gamma \rrbracket}_{\mathrm{Ctx}},{\llbracket \tau \rrbracket}_{\mathrm{Ty}})$

which typechecks becasue we have ${\llbracket \widehat{\Gamma} \rrbracket}_{\mathrm{Ty}} = {\llbracket \Gamma \rrbracket}_{\mathrm{Ctx}}$.

If it helps you to read code, see this Lean 4 Web link. (I admit the definition of the semantics of a derivation because universes used in Mathlib's category definition makes it difficult to write it directly in Prop).

[Fernando Chu]

I see, thanks for sharing the code and clearly explaining things!

Is there a reason on why you use Prop-valued derivations instead of type-valued terms? This is what causing the first problem. I just now realize I could also ask this to @Yiming Xu w.r.t. the geometric logic project.

About the lemma

theorem subst_lemma {Δ Γ : Ctx K} {τ : Ty K} (d1 : Δ ⊢ Γ.to_ty) (d2 : Γ ⊢ τ) (ρ : ∀ {σ : Ty K}, σ ∈ Γ → Δ ⊢ σ) :
  ⟦d1⟧ᵈ ≫ eqToHom (Γ.to_ty_eq) ≫ ⟦d2⟧ᵈ = ⟦d2.subst ρ⟧ᵈ := sorry

The ⟦d1⟧ᵈ ≫ eqToHom (Γ.to_ty_eq) approach seems a bit weird to me. What I had seen before is giving semantics to contexts morphisms ∀ {σ : Ty K}, σ ∈ Γ → Δ ⊢ σ of type ⟦Δ⟧ᶜ ⟶ ⟦Γ⟧ᶜ and using this instead. This has the conceptual benefit of working for type theories that do not have product types. If you want then you could show that this is the same as using ⟦d1⟧ᵈ ≫ eqToHom (Γ.to_ty_eq) but at least you won't see more eqToHoms anymore.

[Yiming Xu]

Fernando Chu said:

I see, thanks for sharing the code and clearly explaining things!

Is there a reason on why you use Prop-valued derivations instead of type-valued terms? This is what causing the first problem. I just now realize I could also ask this to Yiming Xu w.r.t. the geometric logic project.

About the lemma

theorem subst_lemma {Δ Γ : Ctx K} {τ : Ty K} (d1 : Δ ⊢ Γ.to_ty) (d2 : Γ ⊢ τ) (ρ : ∀ {σ : Ty K}, σ ∈ Γ → Δ ⊢ σ) :
  ⟦d1⟧ᵈ ≫ eqToHom (Γ.to_ty_eq) ≫ ⟦d2⟧ᵈ = ⟦d2.subst ρ⟧ᵈ := sorry

The ⟦d1⟧ᵈ ≫ eqToHom (Γ.to_ty_eq) approach seems a bit weird to me. What I had seen before is giving semantics to contexts morphisms ∀ {σ : Ty K}, σ ∈ Γ → Δ ⊢ σ of type ⟦Δ⟧ᶜ ⟶ ⟦Γ⟧ᶜ and using this instead. This has the conceptual benefit of working for type theories that do not have product types. If you want then you could show that this is the same as using ⟦d1⟧ᵈ ≫ eqToHom (Γ.to_ty_eq) but at least you won't see more eqToHoms anymore.

At least for our current formulation of the (Josh's construction of) syntactic category, we do not care about what is the actual proof, but only care about the fact that we have a proof. So the fact that we do not store a Type-valued proof term. Otherwise, I may have misunderstood you (in which case it would be helpful to define your relevant notions with examples...). I remember you asked me on TYPES in person before.

[Fernando Chu]

I forgot sorry, you're indeed right :)

[Yiming Xu]

Ah no worries! BTW, regarding the treatment of proof theory, we may also try sequent calculi, but depend on how much time/energy we have...

[Fernando Chu]

I guess this is then remedied by making the interpretation of formulas (interp_fml) noncomputable

[Yiming Xu]

There are a bunch of noncomputable that is only because Lean imposes noncomputable to something. And if we remove the noncomputable in the relevant notion from Mathlib, many of the things are computable.

[Yiming Xu]

We aim to make (almost, to be safe) everything computable. Myself is not entirely clear about the computability technology involved. I should figure these things out at some point.

[Fernando Chu]

I see, my previous comment is completely wrong, so please ignore that.

[Yiming Xu]

No worries! I think computability issues are confusing. I have the impression that sometimes it is not the fact that things does not compute, but rather the designers of Mathlib do not want people to compute with them. Therefore, there exist things that are marked noncomputable but actually computable (it seems that the designers intend to discourage people from doing something). We should ask about why it happens months ago... but happened to forget it.

(If an expert passes by, many thanks for explaining that to me by answering the question: why are there something computable marked noncomputable in Mathlib?)

[Adrian Marti]

As an example I just ran into, it happens when you are constructing data from a proposition, which you did not prove to satisfy Decidable (this is a condition that says that we can compute with a certain proposition). For example, you might say you want the least natural number satisfying a property (this is Nat.find), but unless you prove that your property is Decidable, the computer will not be able to use commands like #reduce to compute it.

So while classical reasoning ('every proposition is true or false') is allowed when working with Prop, computability can break down when you move from Prop to other types (by things like case distinctions or the axiom of choice). These things result in objects in mathlib like Polynomial not being computable, because it seems like it would take some extra effort to make it computable. There is a whole thread on this here (I do not know the exact details of where Polynomial uses classical reasoning for construction of data).

In any case, this is my understanding of how this works.

[Adrian Marti]

@Chris Henson Thank you for the illuminating web link with the interpretation of non-depedent type theory into cartesian-closed categories. You actually ran into the exact issue I am describing in the previous message :slight_smile:

You are constructing Der as a proposition, which means that it carries no data. So Lean can't extract data from Der to construct a morphism in K unless you rely on noncomputable behaviour. One is a property and the other one is an arrow in a category! Think about it this way: Each way to derive a sequent gives you a (a priori) possibly distinct interpretation as a morphism in K. So, of course, you could just say choose some way to derive and make it a morphism (use the axiom of choice).

You could also keep things computable and define Der to actually carry the data of how we arrived at the derivation (make it Type-valued, as @Fernando Chu sais) and use this. You can always still define a predicate Derives to say that there exists a derivation. In code:

@[aesop unsafe [constructors, cases]]
inductive Der' {K} : Ctx K → Ty K → Type
| var {Γ σ} : σ ∈ Γ → Der' Γ σ
| lam {Γ σ τ} : Der' (σ :: Γ) τ → Der' Γ (σ ⤳ τ)
| app {Γ σ τ} : Der' Γ (σ ⤳ τ) → Der' Γ σ → Der' Γ τ
| π₁ {Γ σ τ} : Der' Γ (σ ⨯ τ) → Der' Γ σ
| π₂ {Γ σ τ} : Der' Γ (σ ⨯ τ) → Der' Γ τ
| pair {Γ σ τ} : Der' Γ σ →  Der' Γ τ → Der' Γ (σ ⨯ τ)
| uni {Γ} : Der' Γ Ty.Unit

abbrev Derives {K} (Γ: Ctx K) (σ: Ty K) := Nonempty (Der' Γ σ)

Then you should have no trouble constructing the desired map

def Der'.interp {Γ : Ctx K} {σ : Ty K} : Der' Γ σ → (⟦Γ⟧ᶜ ⟶  ⟦σ⟧ᵗ) := by
  sorry

by structural recursion.

For your second issue, the problem is that the equality ⟦Γ.to_ty⟧ᵗ = ⟦Γ⟧ᶜ does not hold definitionally. So while the terms can be proved to be equal, Lean cannot prove this automatically with the tactic rfl when it checks composability. One way to fix it is to define ⟦Γ⟧ᶜ := ⟦Γ.to_ty⟧ᵗ :upside_down:

Here is the modified part of your web code:

/-- A mapping from context to type that preserves interpretation -/
@[simp]
def Ctx.to_ty : Ctx K → Ty K
| [] => Ty.Unit
| hd :: tl => hd ⨯ Ctx.to_ty tl

/-- A mapping from contexts into a Cartesian closed category. -/
@[simp]
noncomputable def Ctx.interp : Ctx K → K := Ty.interp ∘ Ctx.to_ty

notation:arg "⟦" Γ "⟧ᶜ" => Ctx.interp Γ

/-- Ctx.to_ty preserves semantics -/
theorem Ctx.to_ty_eq (Γ : Ctx K) : ⟦Γ.to_ty⟧ᵗ = ⟦Γ⟧ᶜ := by
  rfl

This fixes the composability issue and you will not have to use Ctx.to_ty_eq to compose. Lets just hope that this doesn't run you into any trouble anywhere else :)

I hope this helps even though I did not provide any working examples!

[Chris Henson]

@Adrian Marti Redefining Ctx.interp in that way is interesting! Seems it might be easier to work with when proving soundness.

I have previously constructed Der in Type similar to what you describe. You are completely correct, I just find this unsatisfying because this is downstream of Mathlib having morphisms in Type rather than Sort (I recently asked about this in #mathlib4 > categories with morphisms in Prop, there are some links about the history of this decision)

[Chris Henson]

Fernando Chu said:

Is there a reason on why you use Prop-valued derivations instead of type-valued terms?

I have done this previously both ways, having derivations in Prop or Type. Here I just copied over the Prop one because it was more succinct as an example. In general, I find this limitation of disallowing Prop-valued morphisms an unfortunate implementation detail.

I do not quite follow

What I had seen before is giving semantics to contexts morphisms ∀ {σ : Ty K}, σ ∈ Γ → Δ ⊢ σ of type ⟦Δ⟧ᶜ ⟶ ⟦Γ⟧ᶜ and using this instead. This has the conceptual benefit of working for type theories that do not have product types.

do you mean something related to the categories of context renamings or context substitutions? If so, I think I understand. I agree it is desirable to not require product types. For the "usual" semantics of STLC in CCCs it is a bit stange when we extend the type theory at the object level to mirror the structure of contexts at the meta level.

[Adrian Marti]

Why would you like to have morphisms in Prop? I would say that the issue is that you are mapping from a proposition to a type. If you would like to use derivations in Prop you can do this:

noncomputable def Der.interp {Γ : Ctx K} {σ : Ty K} : Der Γ σ → (⟦Γ⟧ᶜ ⟶  ⟦σ⟧ᵗ) := by
  intro der
  apply Classical.choice
  induction der
  -- Your construction by structural recursion here
  sorry

but you won't be able to compute things (and I don't think that there is a way around this).

[Adrian Marti]

Unless of course, you want to discuss semantics in cartesian closed categories with morphisms in Prop (i.e. Heyting algebras only). But I think it would be nice to get general cartesian-closed categories :)

[Chris Henson]

Adrian Marti said:

Why would you like to have morphisms in Prop? I would say that the issue is that you are mapping from a proposition to a type.

Yes, the issue is mapping from Prop to Type. I am just saying the reason this problem exists (at least partially) is because of our definition of a category, which differs from several other category theory libraries in not allowing morphisms in Prop. As a practical matter your noncomputable solution is fine, because we already have other sources of noncomputability, and I agree that it is nice to consider CCCs more generally.

To clarify why I'm bothering with this at all: usually when someone is working with categorical semantics formally, they are also the ones defining the syntax and make certain allowances to smooth the formalization. My interest is when we take a more "off the shelf" formalization of a lambda calculus that has idiomatic features like typing derivations living in Prop. I think it is interesting to explore what techniques we need to adopt in this situation where the syntax was not written to ease formalization of a categorical semantics.

[Adrian Marti]

I guess in the end its a matter of taste whether to use Prop (if we do not care about computability).

Part of what I'm envisioning for the potential future is being able to specify terms in different categories by using general logical symbols (a kind of metaprogramming), and I think that the constructive approach is much more suitable for this application. Of course, after one is done with the constructive definition, one can always deduce the nonconstructive definition by using Nonempty as I did above.

One should also keep in mind the practicalities that computable definitions give you: They will have better-behaved definitional equalities and will require less rewriting/simping. On the hand, doing things computably can require a bit more thinking, and it seems to be mathlib's approach to not bother with it if its not easy (which is very reasonable).

[Chris Henson]

Yes, very much a matter of taste. Your metaprogramming idea is something I have also been thinking about as well! It seems like we should be able to write a term in the syntax and interpret it in whichever categories are included in the semantics. I also had the thought that you should be able to search for theorems in this way, but this is more complicated because you can only rely on the structure given by the semantics.

[Fernando Chu]

I've been told that @𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 Is working on this kind of metaprograming applications, though I don't know the specifics. (This also seem like a good opportunity to find out)

[Kevin Buzzard]

I have no understanding of the theory which is being talked about here, but I have a dumb question. For me two categories are "the same" if they are equivalent. In my kind of mathematics this is the right notion of "the same", sometimes theorems are proved by saying "we want to prove stuff about things in this super-abstract category $C$ most of whose objects we can't understand, but by a deep theorem in arithmetic geometry this category is equivalent to some totally different-looking category $D$, and in $D$ we can do explicit calculations because there are basically formulae for all the objects, and because we have been careful not to be evil we can deduce deep theorems about $C$ via concrete calculations in $D$. This is a key technique in my area. As a result, for me "don't be evil" is high priority, because I might not be able to use evil ideas (e.g. equality of functors) when I'm pulling off tricks like this.

To give an example of two functors which are absolutely not equal, we have these equivalences from $C$ to $D$ and from $D$ to $C$, and if you apply one functor and then the other, the result is a functor from $D$ to $D$ which is provably not equal to the identity functor, for dumb set-theoretic reasons (it would be like taking the double-dual of a finite-dimensional vector space and getting a new vector space which is both completely canonically isomorphic to the original space but also definitely not equal to it, because a general element of the original space is a vector and a general element of the double dual is a function which induced by a vector).

When I see computer scientists asking about things like equality of functors my initial instinct is to regard what they are doing as a dubious approach. But now on reading stuff like this I'm wondering whether there are some people who are also using category theory in their work but who in practice are using a different notion of what it means for two categories to be "the same", or maybe don't even have to wrestle with what it means for two different categories to be "the same" because they are only actually interested in an explicit collection of categories which they can write down and are not attempting to prove that any of them are "the same as" any of the others. If this concept of categories being "the same" is not relevant in certain areas, then it would not surprise me if stuff like equality of functors started to play a far more prominent role.

Is there anything in this or am I just completely off track here?

[James E Hanson]

Kevin Buzzard said:

for dumb set-theoretic reasons

Are they really dumb 'set-theoretic' reasons when the exact same thing would happen in Lean?

[James E Hanson]

Or rather it would be independent of Lean whether the resulting type are equal.

[Chris Henson]

@Kevin Buzzard I think this makes some sense to me? In the context of doing categorical semantics in Lean, I am thinking about a category as roughly a type with enough structure posited by typeclasses to ensure it can interpret my lambda calculus syntax. I don't necessarily care about the same notion of "sameness" as standard category theory. And in this thread at least, it seems people have found being at least a little evil unavoidable in this application.

[Fernando Chu]

Kevin Buzzard said: ...

I think the approach you described is also used by people doing categorical logic and type theory. E.g., when HoTT people reason about $\infty$-toposes, they also care about stuff only up to (some notion of) equivalence, but have to use strict equalities when setting things up. Once these are set up, you can just proceed to forget about them completely.

I'm not following this part:

...and because we have been careful not to be evil we can deduce deep theorems about $C$ via concrete calculations in $D$.

If we were evil somehow, say consider equality of functors in $D$, then the conclusion in $C$ is an isomorphism of functors, which is anyways the "right" notion. I guess my point is that there are no problems on being evil on the category that is being used to compute, this is roughly what is happening in categorical logic too. The category that is being used to compute is the syntactic category, which is very very evil, but once you do a bit of setup you can forget about this.

[Fernando Chu]

Chris Henson said:

...it seems people have found being at least a little evil unavoidable in this application.

I don't think this is quite right. You can avoid evilness completely by modelling judgemental equality only up to iso. This, to me, seems a bit weird since (usually) the categories usually have all the structure necessary to model the theory strictly, so it seems to me it's an unnecessary loss of information. An example of this, for dependent type theory, is replacing C-systems by display map categories. I'd believe one can do the same for STLC and CCC.

[Fernando Chu]

James E Hanson said:

Or rather it would be independent of Lean whether the resulting type are equal.

For the double dual example he suggested, these are independent , since a vector space is equal to its double dual in HoTT. (I could be wrong but I think this is the case)

[James E Hanson]

Fernando Chu said:

For the double dual example he suggested, these are independent , since a vector space is equal to its double dual in HoTT. (I could be wrong but I think this is the case)

Right but Lean has UIP, so you can show that a type is not equal to itself along a non-trivial automorphism, right? I think this means you can define two double-dual functors, $F_0$ and $F_1$, on the category of finite-dimensional vector spaces such that Lean proves '$F_0$ and $F_1$ are naturally isomorphic but not equal.' It's just independent whether either of them is equal to the identity functor.

[Chris Henson]

Fernando Chu said:

You can avoid evilness completely by modelling judgemental equality only up to iso... I'd believe one can do the same for STLC and CCC.

I think this makes sense to me, though you still have to take care to avoid talking about equality of objects for composition? (e.g. the way @Adrian Marti revised my code earlier in the thread)

[Fernando Chu]

@James E Hanson right, my bad; too used to Agda. I'm not sure if its independent but yeah that would also be my guess.

[Fernando Chu]

@Chris Henson For composition instead of using the equality of objects you use an isomorphism in between, which was anyways what you had to do in ⟦d1⟧ᵈ ≫ eqToHom (Γ.to_ty_eq) ≫ ⟦d2⟧ᵈ, as eqToHom is an iso.

[Chris Henson]

Making sure I understand this idea of "judgemental equality up to iso". For instance, how would the statement of soundness change?

[Adrian Marti]

I can't speak for other people, but here is my take on this. I do not think that there really is any dispute in equivalence of categories being the right mathematical notion of sameness for categories. Two equivalent categories satisfy the same properties (this can be made logically precise!).

So the categories $C$ and $D$ in your example are the same and we can use $D$ to prove properties about $C$. However, there is one key difference between $C$ and $D$, which is how it behaves computationally (which the mathematician also does care about!). As you said, it might be hopeless to compute with $C$, but it might be possible to use $D$ for it.

I am specifically interested in exploring whether we can state our definitions in such a way that certain computations in categories is easy and even easy to automate. For example, if $D$ was a category of certain representations and we have an understanding of the irreducible ones, if we were really careful of how we defined everything, we it might be possible to check whether two objects in $D$ are the same (isomorphic) by simply running an algorithm that heavily borrows from our formalization.

While this is a different setting than the categorical logic we are talking about above, I think that it illustrates the point why we might want to building a sort of computational library to make our lives as easy as possible when working with categories.

In fact, one could even imagine that you could tackle problems that are not easy to tackle by humans. For instance, if our objects are big, we might get decompositions into irreducibles that have 100+ terms. But since we are working with Lean, there might be ways to compute and work with these things in the same way that algebraic identities (with no additional free variables, n fixed) in $\mathbb{Z}/n\mathbb{Z}$ become trivial in Lean, because you can find a computational solution (trying all numbers out).

These ideas are fairly vague, but I think that there is definitely room for exploring these things.

Of course, there is also the issue that strictness/equality concerns can actually come up when we want to interpret logical formulas (such as from type theories, as @Fernando Chu mentions) in certain categories. There can be some evil-looking technical details involved in this, but I don't think that is because people do have a different notion of sameness of categories.

[Fernando Chu]

Chris Henson said:

Making sure I understand this idea of "judgemental equality up to iso". For instance, how would the statement of soundness change?

So you model everything up to iso, e.g. ⟦A, B⟧ᶜ is an object $X$ with an isomorphism $X \cong ⟦A⟧ᶜ \times ⟦B⟧ᶜ$, similarly for types. Substitution is then the same diagram as here, except that the endo-arrow is a (possibly non-refl) isomorphism, and the triangle only commutes up to iso
image.png

[Floris van Doorn]

@Johannes Folttmann is a bachelor student in Bonn that is currently formalizing toposes and (some) internal logic of a topos here for his bachelor's thesis, in a fork of @Charlie Conneen's repository.

[Adrian Marti]

Nice, this is pretty useful! Looking at it superficially, I do not think that he got to the logic part yet, but he's probably working on foundations.

It also would be nice if we could eventually gather the results in one place with consistent naming conventions and some basic documentation. If I start playing with things on my own we would have yet another repository :sweat_smile: My original aim was to do the different fragments of geometric logic, but the simply typed lambda calculus or even dependent versions (or other forms of HOL) would also be a 'nice-to-have'. However, one should be aware that this is a bit separate from the geometric logic topic.

We would have to agree on some specific common aims though (and this should be clarified much more, if there actually is any interest in this).

• Are we interested in metaprogramming?
• Are we broadly collecting categorical facts that are useful (i.e. topos theory and similar facts) or should the focus be more on logic and semantics?

There is also the question of whether any of this is relevant for mathlib, since @Johannes Folttmann 's repo seems to claim that these things may go to mathlib at some point.

[Floris van Doorn]

The conjunction is here: https://github.com/johannesfoltt/topos/blob/main/Topos/ClassifierMeet.lean, stated for both the subobject classifier and power objects (so there is also already machinery to translate between those two formulations). The other propositional connectives are forthcoming. (Higher-order) quantification is likely out of scope of his thesis project.

[Adrian Marti]

Ah, makes sense. Is there any plan to define formulas with inductive types and interpret those?

[Fernando Chu]

Adrian Marti said:

...My original aim was to do the different fragments of geometric logic, but the simply typed lambda calculus or even dependent versions (or other forms of HOL) would also be a 'nice-to-have'.

Would be nice if we could develop a very general notion of logic such that most logics can just be a subtype/class on the wffs of this. It would have to be at least some notion of linear multi-mode modal infinitary dependent type theory...

[Floris van Doorn]

Adrian Marti said:

Ah, makes sense. Is there any plan to define formulas with inductive types and interpret those?

Those plans existed at one point, but we had to limit the scope of the thesis to make it feasible. So there are no such plans anymore.

[Adrian Marti]

Fernando Chu said:

Would be nice if we could develop a very general notion of logic such that most logics can just be a subtype/class on the wffs of this. It would have to be at least some notion of linear multi-mode modal infinitary dependent type theory...

I gave it some thought, and there are essentially 4 types of objects we are constructing.

• Sorts (or types in type theory), these have constructors such as function types or cartesian products or even simple inductive types like coproducts. Semantics are the objects of a category.
• Terms (or terms in context in type theory). These arise from composing (and possibly renaming by mapping Fin n \to Fin m) different given function symbols. These produce arrows between objects in a category. Substructural logics like in monoidal categories may have more restrictive ways of constructing terms (maybe we can leave this aside in the beginning). A very nice example for terms is @Chris Henson 's simple type theory interpretation.
• Formulas. These do not arise in type theory, since we build formulas in Prop, as a special case of the previous two cases. They might have a wide variety of constructors, such as the ones found in FOL or even infinitary versions of conjunction and disjunction. These interpret to subobjects of objects in a category and different operations in the subobject lattice.
• Sequents. These interpret to statements of inclusion in subobject lattices, they are mostly relevant for intuitionistic logic (I am not referring to the type-theoretical version of sequents here).

Arguably, one could also add a fifth category, of equations, which take two terms and state that they are equal. They simply interpret to the fact that two arrows are equal in a category (this might be relevant when working in purely algebraic settings, where there might not always be subobjects to interpret the formula $t= s$.).

It would be nice to design a deduction systems that work in for these different logics. Some thought needs to be put into how one would handle deduction in algebraic logics with proof rules like cut, substitution, etc. in such a way that both type theory and the different fragments of geometric logic extend this. If one wants to add monoidal (instead of cartesian) variants of terms eventually in such a way that we have a hierarchy where formulas, proof rules and semantics get progressively extended, this might get more complex.

[Fernando Chu]

Related to the above, I was hoping that the Flypitch authors (e.g. @Floris van Doorn) could comment on the set up of categorical logic, given their experience with FOL. In particular,

1. Even for the FOL case, is there anything that you think could have been designed better? E.g., change the definition of language, (pre)terms, (pre)formulas, etc.
2. Do you think the partially applied terms/formulas approach would be a good fit for categorical logic? Since it is multisorted the indexing type would have to be somewhat more complicated, and not just ℕ.
3. Were there any approaches you tried and decided they were not good approaches?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Chris Henson said: ...

I haven't looked too carefully at what you're doing, but could this be resolved by having two separate judgment forms: $\Delta ⊢_s σ : \Gamma$ for well-formed substitutions, and $\Gamma ⊢ t : τ$ for well-typed terms? Then the former can be interpreted into $\mathcal C(⟦\Delta⟧_{Ctx}, ⟦\Gamma⟧_{Ctx})$, the latter into $\mathcal C(⟦\Gamma⟧_{Ctx}, ⟦τ⟧_{Ty})$, and you don't need the $\widehat \Gamma$ operation.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Fernando Chu said:

I've been told that 𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 Is working on this kind of metaprograming applications, though I don't know the specifics. (This also seem like a good opportunity to find out)

My personal belief is that if you want to use the internal language of any category in practice, you pretty much need a proof assistant for it; nobody wants to write down deeply embedded proof terms by hand. So we've been implementing that in the groupoid project (see also our TYPES talk by @joseph hua). In our case the internal language is intentionally designed to be a dependent type theory very close to Lean so that the proof assistant can just be Lean. We then use some metaprogramming magic to translate the outputs of Lean elaboration into objects in the model (the model is a natural model/CwF). This is all WIP.

[Chris Henson]

The separate judgement should work. I have some interest in how things play out if you aren't able to alter your syntax or judgements, say someone hands you an already complete formalization, this is what I was describing.

Yes, I listened to the talk and took a look at the repo, it looks really interesting! Especially in having a very "concrete" syntax to implement a proof mode. I noticed you mention Autosubst and thought that was interesting. I have been playing around with the idea of some Lean metaprogramming inspired by their MetaCoq implementation to generate locally nameless syntaxes.

[Adrian Marti]

This is a really cool project! I've long had in the back of my mind that this (or at least similar things) should be done. There are so many uses for it. Here are some thoughts.

• Having the structural identity principle internally enables us to (at least in theory) rewrite along isomorphic structures, which is something that is really cool to see. Especially because (from what I've seen) it can be annoying to transfer properties along isomorphic structures in Lean. Also, we can synthetically reason, not only about structures, but about collections (groupoids) of structures in an isolated (synthetic) environment.
• I especially look forward to interpretations in general presheaf toposes or even sheaf toposes (or their (2,1)-variations). In this way, we can use classifying topos constructions to model type theories that may contain additional, axiomatically introduced, structures, such as a type theory that additionally contains a generic type that is a group (or a ring). In this way, we can prove generic statements about structures.
• Given a logical geometric morphisms we should be able to transfer statements across different settings. If your geometric morphism doesn't happen to be logical, no worries. The dependent type theory conservatively extends the fragment of the logic that is geometric (doesn't contain pi-types, sigma-types should be allowed, at least I think). This means that we can use the power of the embedded proof assistant to prove a geometric statement and then transfer it along a geometric morphism to a different setting (As in Olivia Caramello's ideas).
• You could use this to prove that there are (2,1)-stacks classifying certain classes of objects (as you would like to do in some areas of mathematics) by providing logical formulas for them in the appropriate (classifying) topos(keep in mind that the any representability statements for those stacks are not free, if you really want those).

I realize that probably not all the machinery for this is in place (interpretations in (2,1)-stacks?), but this definitely brings us one good step closer to it. I apologize for writing a lot about ideas, a not so much about concrete mathematics/formalization. I'm just glad that there is work in this direction.

[Adrian Marti]

Related to the original question: Did anyone do operads/multicategories?

[Bas Spitters]

To be sure, are you aware of the HoTT Lean project? It formalizes the semantics of HoTT in Lean.
@Sina Hazratpour is involved and is an expert on geometric logic.

[Bas Spitters]

There's also recent work by Ulrik Buchholz on geometric type theory, unfortunately google is currently not very helpful finding it... (I believe it was in the TYPES proceedings)

[Bas Spitters]

@Yiming Xu @Kyod thanks for the nice abstract! This is cool. Are you aware of Steve Vickers' work on Geometric type theory? It may be more convenient for formalization. https://sjvickers.github.io/LocTopSpaces.pdf

Your work is also reminiscent of the line of work on universal algebra in type theory.

[Tom de Jong]

Bas Spitters said:

There's also recent work by Ulrik Buchholz on geometric type theory, unfortunately google is currently not very helpful finding it... (I believe it was in the TYPES proceedings)

There's an early abstract from the HoTT/UF 2025 workshop: https://hott-uf.github.io/2025/abstracts/HoTTUF_2025_paper_25.pdf

[Bas Spitters]

@Tom de Jong better than Google :sunglasses:

[Tom de Jong]

See also this recent talk at a CIRM conference by Ulrik: https://library.cirm-math.fr/Record.htm?idlist=1&record=19394786124911129689

[Yiming Xu]

Bas Spitters said:

To be sure, are you aware of the HoTT Lean project? It formalizes the semantics of HoTT in Lean.
Sina Hazratpour is involved and is an expert on geometric logic.

I am also a collaborator in HoTTLean :-) . On the theory of implementing syntax + a sound semantics and use that to do something useful, @𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 is an expert on that.

[Yiming Xu]

Our HoTTLean is formalizing Martin-Löf theories, and it is more ambitious in the sense that we want a dual-mode theorem prover. And we should be able to give definitions in the level of the particular model, not only from the syntax, as well.

[Yiming Xu]

Bas Spitters said:

Yiming Xu Kyod thanks for the nice abstract! This is cool. Are you aware of Steve Vickers' work on Geometric type theory? It may be more convenient for formalization. https://sjvickers.github.io/LocTopSpaces.pdf

Your work is also reminiscent of the line of work on universal algebra in type theory.

Thank you for the link! I am very interested in work by Steve Vickers in general because I think his writting involve a strong intention of treating the geometric intuition. I will read it in more details.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

In response to a related discussion, I can share an update on our progress.

HoTTLean now contains a module called SynthLean (for 'synthetic mathematics in Lean') which interprets terms in (a very stripped down fragment of) Lean's type theory in any model belonging to an abstract class of category-theoretic models (natural models; these carry the same data as categories with families). We are going to present this at CPP 2026 in January, and you can read the preprint here. This is an early prototype and our next step is to actually make constructions in specific models using this technology, but feel free to try out some of our demos. Importantly, SynthLean gives you all the usual proof assistant tooling so that internal language arguments can be developed using standard (constructive unless your model happens to validate a lot of axioms!) tactics.

CC @Bhavik Mehta

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Bhavik Mehta said:

how to translate Lean's structure defeqs into being explicit rewrites

If I understand you correctly, this is the "strictness problem" for categorical interpretations of type theory, and the modern solution is to axiomatize a class of categorical models in which we know how to interpret all the type-theoretic constructs s.t. it is always the case that defeqs are semantically validated, e.g. ⟦(λx. b) t⟧ = ⟦b[t]⟧ for β-reduction. The tradeoff is whether the class of models is closer to the syntax, so that interpreting syntax in any model is trivial, but constructing actual models is harder, or further away from the syntax so that it takes more work to show that all the type-theoretic defeqs hold, but maybe it's easier to assemble a model from mathematical objects. The first page of "Type Theory in Type Theory using a Strictified Syntax" has a nice depiction of the various choices along this spectrum.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Bhavik Mehta said:

can we automatically derive equalities in the category which correspond to this theorem?

I implemented this here. The main components are

empty def aux1 {A B : Type} (x : A) (y : B) := myPi (myPair x y)
empty def aux2 {A B : Type} (x : A) (y : B) := x

Here the empty stands for 'empty theory': we are doing this in MLTT with no additional axioms. aux2 has some spurious arguments in order to make the two sides have equal contexts; otherwise it doesn't make sense to ask whether they're equal. Then we do

open Qq in
example :
    (emptyInterp s).interpTm aux1.wf_val =
    (emptyInterp s).interpTm aux2.wf_val := by
  apply interpTm_eq -- Reduce to internal judgmental equality
  run_tac do -- Run the typechecker
    let pf ← TypecheckerM.run <| equateWfTms
      q(Axioms.empty Lean.Name) q([]) q(aux1.l) q(aux1.val) q(aux2.val) q(aux1.tp)
    Lean.Elab.Tactic.closeMainGoal `equateTms q($pf TpEnvEqCtx.nil aux1.wf_val aux2.wf_val)

Note that this targets models-of-MLTT rather than CCCs.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Bhavik Mehta said:

ideally we should be able to interpret in any category with enough structure, so eg convert the natural number game automatically into a topos with NNO, and convert any fully polymorphic constructive proof in mathlib into a topos, and convert any proof in mathlib into a category satisfying ETCS.

This is indeed the folklore, but afaict turning this into actual Lean theorems/tactics would require making things quite a bit more precise. In the context of SynthLean, one would have to construct a natural model (or something related that we are now calling an UnstructuredModel) out of a given "nice" category (a topos). This requires constructing a "universe", which is a "universal type-in-context"; all types-in-context (of a given size) that we care about should arise as pullbacks of this. There is a note of Streicher on "Universes in Toposes", various constructions in LCCCs, as well as some constructions specific to Grothendieck toposes (e.g. "Strict universes for Grothendieck topoi").