#hott — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #hott, aggregated by home.social.
-
Delooping generated groups in homotopy type theory. ~ Camil Champin, Samuel Mimram, Emile Oleon. https://arxiv.org/abs/2405.03264v1 #Agda #ITP #HoTT
-
This week the #HoTTEST seminar presents:
Freek Geerligs
Synthetic Stone duality
The talk is at 11:30am EDT (15:30 UTC) on Thursday, April 16. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract:
In this talk, we will give an overview of Synthetic Stone duality (https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.3). We will then discuss some related work in progress.
Synthetic Stone duality is an extension of homotopy type theory with four axioms. These axioms are strong enough to decide Bishop's omniscience principles. We introduce a (synthetic) topology on any type, such that all functions are continuous. We are interested in Stone spaces and compact Hausdorff spaces, where the topology behaves as one would expect. In particular, we can define the (topological) interval and show that all functions are continuous in the epsilon-delta sense.
Currently, we are working on a paper with a method for calculating cohomology with countably presented coefficients for compact Hausdorff spaces. We are also interested in a correspondence between homotopical concepts defined using traditional topology (using paths from the topological interval) and homotopy type theory (using identity types).
This talk will contain joint work with Reid Barton, Felix Cherubini, Thierry Coquand, and Hugo Moeneclaey.
-
This week the #HoTTEST seminar presents:
Freek Geerligs
Synthetic Stone duality
The talk is at 11:30am EDT (15:30 UTC) on Thursday, April 16. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract:
In this talk, we will give an overview of Synthetic Stone duality (https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.3). We will then discuss some related work in progress.
Synthetic Stone duality is an extension of homotopy type theory with four axioms. These axioms are strong enough to decide Bishop's omniscience principles. We introduce a (synthetic) topology on any type, such that all functions are continuous. We are interested in Stone spaces and compact Hausdorff spaces, where the topology behaves as one would expect. In particular, we can define the (topological) interval and show that all functions are continuous in the epsilon-delta sense.
Currently, we are working on a paper with a method for calculating cohomology with countably presented coefficients for compact Hausdorff spaces. We are also interested in a correspondence between homotopical concepts defined using traditional topology (using paths from the topological interval) and homotopy type theory (using identity types).
This talk will contain joint work with Reid Barton, Felix Cherubini, Thierry Coquand, and Hugo Moeneclaey.
-
This week the #HoTTEST seminar presents:
Freek Geerligs
Synthetic Stone duality
The talk is at 11:30am EDT (15:30 UTC) on Thursday, April 16. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract:
In this talk, we will give an overview of Synthetic Stone duality (https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.3). We will then discuss some related work in progress.
Synthetic Stone duality is an extension of homotopy type theory with four axioms. These axioms are strong enough to decide Bishop's omniscience principles. We introduce a (synthetic) topology on any type, such that all functions are continuous. We are interested in Stone spaces and compact Hausdorff spaces, where the topology behaves as one would expect. In particular, we can define the (topological) interval and show that all functions are continuous in the epsilon-delta sense.
Currently, we are working on a paper with a method for calculating cohomology with countably presented coefficients for compact Hausdorff spaces. We are also interested in a correspondence between homotopical concepts defined using traditional topology (using paths from the topological interval) and homotopy type theory (using identity types).
This talk will contain joint work with Reid Barton, Felix Cherubini, Thierry Coquand, and Hugo Moeneclaey.
-
This week the #HoTTEST seminar presents:
Freek Geerligs
Synthetic Stone duality
The talk is at 11:30am EDT (15:30 UTC) on Thursday, April 16. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract:
In this talk, we will give an overview of Synthetic Stone duality (https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.3). We will then discuss some related work in progress.
Synthetic Stone duality is an extension of homotopy type theory with four axioms. These axioms are strong enough to decide Bishop's omniscience principles. We introduce a (synthetic) topology on any type, such that all functions are continuous. We are interested in Stone spaces and compact Hausdorff spaces, where the topology behaves as one would expect. In particular, we can define the (topological) interval and show that all functions are continuous in the epsilon-delta sense.
Currently, we are working on a paper with a method for calculating cohomology with countably presented coefficients for compact Hausdorff spaces. We are also interested in a correspondence between homotopical concepts defined using traditional topology (using paths from the topological interval) and homotopy type theory (using identity types).
This talk will contain joint work with Reid Barton, Felix Cherubini, Thierry Coquand, and Hugo Moeneclaey.
-
This week the #HoTTEST seminar presents:
Freek Geerligs
Synthetic Stone duality
The talk is at 11:30am EDT (15:30 UTC) on Thursday, April 16. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract:
In this talk, we will give an overview of Synthetic Stone duality (https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.3). We will then discuss some related work in progress.
Synthetic Stone duality is an extension of homotopy type theory with four axioms. These axioms are strong enough to decide Bishop's omniscience principles. We introduce a (synthetic) topology on any type, such that all functions are continuous. We are interested in Stone spaces and compact Hausdorff spaces, where the topology behaves as one would expect. In particular, we can define the (topological) interval and show that all functions are continuous in the epsilon-delta sense.
Currently, we are working on a paper with a method for calculating cohomology with countably presented coefficients for compact Hausdorff spaces. We are also interested in a correspondence between homotopical concepts defined using traditional topology (using paths from the topological interval) and homotopy type theory (using identity types).
This talk will contain joint work with Reid Barton, Felix Cherubini, Thierry Coquand, and Hugo Moeneclaey.
-
This week the #HoTTEST seminar presents:
Szumi Xie
The groupoid-syntax of type theory is a set
The talk is at 11:30am EDT (15:30 UTC) on Thursday, April 2. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks. (This should be back to the "usual" time for Europeans who are now on summer time.)
All are welcome!
Abstract:
Categories with families (CwFs) have been used to define the semantics of type theory in type theory. In the setting of homotopy type theory, one of the limitations of the traditional notion of CwFs is the requirement to set-truncate types, which excludes models based on univalent categories, such as the standard set model. To address this limitation, I will introduce the notion of groupoid categories with families (GCwFs), which truncates types at the groupoid level and incorporates coherence equations.
I will demonstrate that the initial GCwF for a type theory with some type formers is set-truncated, using a technique called α-normalization. This allows us to utilize the conventional intrinsic syntax of type theory while enabling interpretations in semantically richer and more natural models.
I will also present a generalization of GCwFs and discuss its relation to comprehension categories.
This talk is based on joint work with Thorsten Altenkirch and Ambrus Kaposi (https://doi.org/10.4230/LIPIcs.CSL.2026.40).
-
This week the #HoTTEST seminar presents:
Szumi Xie
The groupoid-syntax of type theory is a set
The talk is at 11:30am EDT (15:30 UTC) on Thursday, April 2. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks. (This should be back to the "usual" time for Europeans who are now on summer time.)
All are welcome!
Abstract:
Categories with families (CwFs) have been used to define the semantics of type theory in type theory. In the setting of homotopy type theory, one of the limitations of the traditional notion of CwFs is the requirement to set-truncate types, which excludes models based on univalent categories, such as the standard set model. To address this limitation, I will introduce the notion of groupoid categories with families (GCwFs), which truncates types at the groupoid level and incorporates coherence equations.
I will demonstrate that the initial GCwF for a type theory with some type formers is set-truncated, using a technique called α-normalization. This allows us to utilize the conventional intrinsic syntax of type theory while enabling interpretations in semantically richer and more natural models.
I will also present a generalization of GCwFs and discuss its relation to comprehension categories.
This talk is based on joint work with Thorsten Altenkirch and Ambrus Kaposi (https://doi.org/10.4230/LIPIcs.CSL.2026.40).
-
This week the #HoTTEST seminar presents:
Szumi Xie
The groupoid-syntax of type theory is a set
The talk is at 11:30am EDT (15:30 UTC) on Thursday, April 2. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks. (This should be back to the "usual" time for Europeans who are now on summer time.)
All are welcome!
Abstract:
Categories with families (CwFs) have been used to define the semantics of type theory in type theory. In the setting of homotopy type theory, one of the limitations of the traditional notion of CwFs is the requirement to set-truncate types, which excludes models based on univalent categories, such as the standard set model. To address this limitation, I will introduce the notion of groupoid categories with families (GCwFs), which truncates types at the groupoid level and incorporates coherence equations.
I will demonstrate that the initial GCwF for a type theory with some type formers is set-truncated, using a technique called α-normalization. This allows us to utilize the conventional intrinsic syntax of type theory while enabling interpretations in semantically richer and more natural models.
I will also present a generalization of GCwFs and discuss its relation to comprehension categories.
This talk is based on joint work with Thorsten Altenkirch and Ambrus Kaposi (https://doi.org/10.4230/LIPIcs.CSL.2026.40).
-
This week the #HoTTEST seminar presents:
Szumi Xie
The groupoid-syntax of type theory is a set
The talk is at 11:30am EDT (15:30 UTC) on Thursday, April 2. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks. (This should be back to the "usual" time for Europeans who are now on summer time.)
All are welcome!
Abstract:
Categories with families (CwFs) have been used to define the semantics of type theory in type theory. In the setting of homotopy type theory, one of the limitations of the traditional notion of CwFs is the requirement to set-truncate types, which excludes models based on univalent categories, such as the standard set model. To address this limitation, I will introduce the notion of groupoid categories with families (GCwFs), which truncates types at the groupoid level and incorporates coherence equations.
I will demonstrate that the initial GCwF for a type theory with some type formers is set-truncated, using a technique called α-normalization. This allows us to utilize the conventional intrinsic syntax of type theory while enabling interpretations in semantically richer and more natural models.
I will also present a generalization of GCwFs and discuss its relation to comprehension categories.
This talk is based on joint work with Thorsten Altenkirch and Ambrus Kaposi (https://doi.org/10.4230/LIPIcs.CSL.2026.40).
-
This week the #HoTTEST seminar presents:
Szumi Xie
The groupoid-syntax of type theory is a set
The talk is at 11:30am EDT (15:30 UTC) on Thursday, April 2. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks. (This should be back to the "usual" time for Europeans who are now on summer time.)
All are welcome!
Abstract:
Categories with families (CwFs) have been used to define the semantics of type theory in type theory. In the setting of homotopy type theory, one of the limitations of the traditional notion of CwFs is the requirement to set-truncate types, which excludes models based on univalent categories, such as the standard set model. To address this limitation, I will introduce the notion of groupoid categories with families (GCwFs), which truncates types at the groupoid level and incorporates coherence equations.
I will demonstrate that the initial GCwF for a type theory with some type formers is set-truncated, using a technique called α-normalization. This allows us to utilize the conventional intrinsic syntax of type theory while enabling interpretations in semantically richer and more natural models.
I will also present a generalization of GCwFs and discuss its relation to comprehension categories.
This talk is based on joint work with Thorsten Altenkirch and Ambrus Kaposi (https://doi.org/10.4230/LIPIcs.CSL.2026.40).
-
This week the #HoTTEST seminar presents:
Astra Kolomatskaia
Displayed Type Theory, intervals, and analytic higher categorical structures
The talk is at 11:30am EDT (15:30 UTC) on Thursday, March 19. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks. (Note that we recently started daylight time in North America, so the local time may have changed for you.)
All are welcome!
Abstract:
I have historically encountered a number of difficulties in communicating my work to others. The process of preparing this talk has thus involved engaging with throughlines in the type theory literature and has helped me identify places in which building bridges was necessary.
My joint work with Mike Shulman introduced Displayed Type Theory [dTT], which syntactically admits a construction of semi-simplicial types in a way that then semantically admits interpretation into arbitrary Grothendieck (∞,1)-topoi. This result is not novel as stated: First, it is not a syntactic construction in Book HoTT. Second, syntactic constructions of SSTs were a foremost consideration in the development of 2LTT, and Elif Üsküplü's analysis shows that the inner layer of 2LTT, when enriched with an axiom of cofibrant exo-nats, is general with respect to Grothendieck (∞,1)-topos semantics. [...]
[Full abstract too long for even two toots, so follow the link to the seminar page to see it all.]
-
This week the #HoTTEST seminar presents:
Astra Kolomatskaia
Displayed Type Theory, intervals, and analytic higher categorical structures
The talk is at 11:30am EDT (15:30 UTC) on Thursday, March 19. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks. (Note that we recently started daylight time in North America, so the local time may have changed for you.)
All are welcome!
Abstract:
I have historically encountered a number of difficulties in communicating my work to others. The process of preparing this talk has thus involved engaging with throughlines in the type theory literature and has helped me identify places in which building bridges was necessary.
My joint work with Mike Shulman introduced Displayed Type Theory [dTT], which syntactically admits a construction of semi-simplicial types in a way that then semantically admits interpretation into arbitrary Grothendieck (∞,1)-topoi. This result is not novel as stated: First, it is not a syntactic construction in Book HoTT. Second, syntactic constructions of SSTs were a foremost consideration in the development of 2LTT, and Elif Üsküplü's analysis shows that the inner layer of 2LTT, when enriched with an axiom of cofibrant exo-nats, is general with respect to Grothendieck (∞,1)-topos semantics. [...]
[Full abstract too long for even two toots, so follow the link to the seminar page to see it all.]
-
This week the #HoTTEST seminar presents:
Astra Kolomatskaia
Displayed Type Theory, intervals, and analytic higher categorical structures
The talk is at 11:30am EDT (15:30 UTC) on Thursday, March 19. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks. (Note that we recently started daylight time in North America, so the local time may have changed for you.)
All are welcome!
Abstract:
I have historically encountered a number of difficulties in communicating my work to others. The process of preparing this talk has thus involved engaging with throughlines in the type theory literature and has helped me identify places in which building bridges was necessary.
My joint work with Mike Shulman introduced Displayed Type Theory [dTT], which syntactically admits a construction of semi-simplicial types in a way that then semantically admits interpretation into arbitrary Grothendieck (∞,1)-topoi. This result is not novel as stated: First, it is not a syntactic construction in Book HoTT. Second, syntactic constructions of SSTs were a foremost consideration in the development of 2LTT, and Elif Üsküplü's analysis shows that the inner layer of 2LTT, when enriched with an axiom of cofibrant exo-nats, is general with respect to Grothendieck (∞,1)-topos semantics. [...]
[Full abstract too long for even two toots, so follow the link to the seminar page to see it all.]
-
This week the #HoTTEST seminar presents:
Astra Kolomatskaia
Displayed Type Theory, intervals, and analytic higher categorical structures
The talk is at 11:30am EDT (15:30 UTC) on Thursday, March 19. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks. (Note that we recently started daylight time in North America, so the local time may have changed for you.)
All are welcome!
Abstract:
I have historically encountered a number of difficulties in communicating my work to others. The process of preparing this talk has thus involved engaging with throughlines in the type theory literature and has helped me identify places in which building bridges was necessary.
My joint work with Mike Shulman introduced Displayed Type Theory [dTT], which syntactically admits a construction of semi-simplicial types in a way that then semantically admits interpretation into arbitrary Grothendieck (∞,1)-topoi. This result is not novel as stated: First, it is not a syntactic construction in Book HoTT. Second, syntactic constructions of SSTs were a foremost consideration in the development of 2LTT, and Elif Üsküplü's analysis shows that the inner layer of 2LTT, when enriched with an axiom of cofibrant exo-nats, is general with respect to Grothendieck (∞,1)-topos semantics. [...]
[Full abstract too long for even two toots, so follow the link to the seminar page to see it all.]
-
This week the #HoTTEST seminar presents:
Astra Kolomatskaia
Displayed Type Theory, intervals, and analytic higher categorical structures
The talk is at 11:30am EDT (15:30 UTC) on Thursday, March 19. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks. (Note that we recently started daylight time in North America, so the local time may have changed for you.)
All are welcome!
Abstract:
I have historically encountered a number of difficulties in communicating my work to others. The process of preparing this talk has thus involved engaging with throughlines in the type theory literature and has helped me identify places in which building bridges was necessary.
My joint work with Mike Shulman introduced Displayed Type Theory [dTT], which syntactically admits a construction of semi-simplicial types in a way that then semantically admits interpretation into arbitrary Grothendieck (∞,1)-topoi. This result is not novel as stated: First, it is not a syntactic construction in Book HoTT. Second, syntactic constructions of SSTs were a foremost consideration in the development of 2LTT, and Elif Üsküplü's analysis shows that the inner layer of 2LTT, when enriched with an axiom of cofibrant exo-nats, is general with respect to Grothendieck (∞,1)-topos semantics. [...]
[Full abstract too long for even two toots, so follow the link to the seminar page to see it all.]
-
This week the #HoTTEST seminar presents:
Ayberk Tosun (@ayberkt)
Constructive and predicative locale theory in univalent foundations
The talk is at 11:30am EST (16:30 UTC) on Thursday, March 5. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract in the next post (because of the character limit)
-
This week the #HoTTEST seminar presents:
Ayberk Tosun (@ayberkt)
Constructive and predicative locale theory in univalent foundations
The talk is at 11:30am EST (16:30 UTC) on Thursday, March 5. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract in the next post (because of the character limit)
-
This week the #HoTTEST seminar presents:
Ayberk Tosun (@ayberkt)
Constructive and predicative locale theory in univalent foundations
The talk is at 11:30am EST (16:30 UTC) on Thursday, March 5. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract in the next post (because of the character limit)
-
This week the #HoTTEST seminar presents:
Ayberk Tosun (@ayberkt)
Constructive and predicative locale theory in univalent foundations
The talk is at 11:30am EST (16:30 UTC) on Thursday, March 5. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract in the next post (because of the character limit)
-
This week the #HoTTEST seminar presents:
Ayberk Tosun (@ayberkt)
Constructive and predicative locale theory in univalent foundations
The talk is at 11:30am EST (16:30 UTC) on Thursday, March 5. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract in the next post (because of the character limit)
-
This week the #HoTTEST seminar presents:
Bastiaan Cnossen
Synthetic category theory in CaTT
The talk is at 11:30am EST (16:30 UTC) on Thursday, February 19. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract:
Up to now, most approaches to a synthetic theory of categories are based on Martin-Löf type theory (e.g. directed/simplicial type theory). In this talk, I discuss some first explorations for using the type theory CaTT as a basis for synthetic category theory.
The type theory CaTT, developed by Finster and Mimram, captures the internal language of a weak ω-category: a categorical structure with n-morphisms for every n with operations satisfying the weakest possible form of coherence laws. Unlike HoTT, CaTT may be interpreted directly within any (∞,1)-category, without need for intricate strictification results. In particular, CaTT has a model given by the (∞,1)-category Cat of small (∞,1)-categories.
The long-term goal of our project is to enhance CaTT with additional rules capturing the internal language of Cat. In this talk I will focus on a first step: after explaining the basics of CaTT, I will formulate additional rules in CaTT that force its models to be (∞,1)-categories with products, pullbacks and/or internal homs. I will further explain how we hope to extend this in the future. Everything is joint with Ivan Kobe.
-
This week the #HoTTEST seminar presents:
Bastiaan Cnossen
Synthetic category theory in CaTT
The talk is at 11:30am EST (16:30 UTC) on Thursday, February 19. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract:
Up to now, most approaches to a synthetic theory of categories are based on Martin-Löf type theory (e.g. directed/simplicial type theory). In this talk, I discuss some first explorations for using the type theory CaTT as a basis for synthetic category theory.
The type theory CaTT, developed by Finster and Mimram, captures the internal language of a weak ω-category: a categorical structure with n-morphisms for every n with operations satisfying the weakest possible form of coherence laws. Unlike HoTT, CaTT may be interpreted directly within any (∞,1)-category, without need for intricate strictification results. In particular, CaTT has a model given by the (∞,1)-category Cat of small (∞,1)-categories.
The long-term goal of our project is to enhance CaTT with additional rules capturing the internal language of Cat. In this talk I will focus on a first step: after explaining the basics of CaTT, I will formulate additional rules in CaTT that force its models to be (∞,1)-categories with products, pullbacks and/or internal homs. I will further explain how we hope to extend this in the future. Everything is joint with Ivan Kobe.
-
This week the #HoTTEST seminar presents:
Bastiaan Cnossen
Synthetic category theory in CaTT
The talk is at 11:30am EST (16:30 UTC) on Thursday, February 19. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract:
Up to now, most approaches to a synthetic theory of categories are based on Martin-Löf type theory (e.g. directed/simplicial type theory). In this talk, I discuss some first explorations for using the type theory CaTT as a basis for synthetic category theory.
The type theory CaTT, developed by Finster and Mimram, captures the internal language of a weak ω-category: a categorical structure with n-morphisms for every n with operations satisfying the weakest possible form of coherence laws. Unlike HoTT, CaTT may be interpreted directly within any (∞,1)-category, without need for intricate strictification results. In particular, CaTT has a model given by the (∞,1)-category Cat of small (∞,1)-categories.
The long-term goal of our project is to enhance CaTT with additional rules capturing the internal language of Cat. In this talk I will focus on a first step: after explaining the basics of CaTT, I will formulate additional rules in CaTT that force its models to be (∞,1)-categories with products, pullbacks and/or internal homs. I will further explain how we hope to extend this in the future. Everything is joint with Ivan Kobe.
-
This week the #HoTTEST seminar presents:
Bastiaan Cnossen
Synthetic category theory in CaTT
The talk is at 11:30am EST (16:30 UTC) on Thursday, February 19. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract:
Up to now, most approaches to a synthetic theory of categories are based on Martin-Löf type theory (e.g. directed/simplicial type theory). In this talk, I discuss some first explorations for using the type theory CaTT as a basis for synthetic category theory.
The type theory CaTT, developed by Finster and Mimram, captures the internal language of a weak ω-category: a categorical structure with n-morphisms for every n with operations satisfying the weakest possible form of coherence laws. Unlike HoTT, CaTT may be interpreted directly within any (∞,1)-category, without need for intricate strictification results. In particular, CaTT has a model given by the (∞,1)-category Cat of small (∞,1)-categories.
The long-term goal of our project is to enhance CaTT with additional rules capturing the internal language of Cat. In this talk I will focus on a first step: after explaining the basics of CaTT, I will formulate additional rules in CaTT that force its models to be (∞,1)-categories with products, pullbacks and/or internal homs. I will further explain how we hope to extend this in the future. Everything is joint with Ivan Kobe.
-
This week the #HoTTEST seminar presents:
Bastiaan Cnossen
Synthetic category theory in CaTT
The talk is at 11:30am EST (16:30 UTC) on Thursday, February 19. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract:
Up to now, most approaches to a synthetic theory of categories are based on Martin-Löf type theory (e.g. directed/simplicial type theory). In this talk, I discuss some first explorations for using the type theory CaTT as a basis for synthetic category theory.
The type theory CaTT, developed by Finster and Mimram, captures the internal language of a weak ω-category: a categorical structure with n-morphisms for every n with operations satisfying the weakest possible form of coherence laws. Unlike HoTT, CaTT may be interpreted directly within any (∞,1)-category, without need for intricate strictification results. In particular, CaTT has a model given by the (∞,1)-category Cat of small (∞,1)-categories.
The long-term goal of our project is to enhance CaTT with additional rules capturing the internal language of Cat. In this talk I will focus on a first step: after explaining the basics of CaTT, I will formulate additional rules in CaTT that force its models to be (∞,1)-categories with products, pullbacks and/or internal homs. I will further explain how we hope to extend this in the future. Everything is joint with Ivan Kobe.
-
The 2026 website for the annual autumn school Proof and Computation is now up at https://www.mathematik.uni-muenchen.de/~schwicht/pc26.php
I'm excited to give a short course introducing homotopy type theory / univalent foundations, and look forward to participating in this very enjoyable school once more!
-
The 2026 website for the annual autumn school Proof and Computation is now up at https://www.mathematik.uni-muenchen.de/~schwicht/pc26.php
I'm excited to give a short course introducing homotopy type theory / univalent foundations, and look forward to participating in this very enjoyable school once more!
-
The 2026 website for the annual autumn school Proof and Computation is now up at https://www.mathematik.uni-muenchen.de/~schwicht/pc26.php
I'm excited to give a short course introducing homotopy type theory / univalent foundations, and look forward to participating in this very enjoyable school once more!
-
The 2026 website for the annual autumn school Proof and Computation is now up at https://www.mathematik.uni-muenchen.de/~schwicht/pc26.php
I'm excited to give a short course introducing homotopy type theory / univalent foundations, and look forward to participating in this very enjoyable school once more!
-
The 2026 website for the annual autumn school Proof and Computation is now up at https://www.mathematik.uni-muenchen.de/~schwicht/pc26.php
I'm excited to give a short course introducing homotopy type theory / univalent foundations, and look forward to participating in this very enjoyable school once more!
-
I forgot to announce this week's #HoTTEST seminar ahead of time, but the talk is now live on YouTube, so you can watch it there: https://youtu.be/dCOZGKbSQSo
Talk info:
Benedikt Ahrens
A type theory for comprehension categories
Abstract:
Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial morphisms between types; these morphisms are not used in the standard interpretation of Martin-Löf type theory in comprehension categories.
We develop a type theory that internalizes morphisms between types, reflecting this semantic feature back into syntax. Our type theory comes with Π-, Σ-, and identity types. We discuss how it can be viewed as an extension of Martin-Löf type theory with coercive subtyping, as sketched by Coraglia and Emmenegger. We furthermore define semantic structure that interprets our type theory and prove a soundness result. Finally, we exhibit many examples of the semantic structure, yielding a plethora of interpretations.
This talk is based on joint work with Niyousha Najmaei, Niels van der Weide, and Paige Randall North published in doi:10.1145/3776725.
-
I forgot to announce this week's #HoTTEST seminar ahead of time, but the talk is now live on YouTube, so you can watch it there: https://youtu.be/dCOZGKbSQSo
Talk info:
Benedikt Ahrens
A type theory for comprehension categories
Abstract:
Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial morphisms between types; these morphisms are not used in the standard interpretation of Martin-Löf type theory in comprehension categories.
We develop a type theory that internalizes morphisms between types, reflecting this semantic feature back into syntax. Our type theory comes with Π-, Σ-, and identity types. We discuss how it can be viewed as an extension of Martin-Löf type theory with coercive subtyping, as sketched by Coraglia and Emmenegger. We furthermore define semantic structure that interprets our type theory and prove a soundness result. Finally, we exhibit many examples of the semantic structure, yielding a plethora of interpretations.
This talk is based on joint work with Niyousha Najmaei, Niels van der Weide, and Paige Randall North published in doi:10.1145/3776725.
-
I forgot to announce this week's #HoTTEST seminar ahead of time, but the talk is now live on YouTube, so you can watch it there: https://youtu.be/dCOZGKbSQSo
Talk info:
Benedikt Ahrens
A type theory for comprehension categories
Abstract:
Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial morphisms between types; these morphisms are not used in the standard interpretation of Martin-Löf type theory in comprehension categories.
We develop a type theory that internalizes morphisms between types, reflecting this semantic feature back into syntax. Our type theory comes with Π-, Σ-, and identity types. We discuss how it can be viewed as an extension of Martin-Löf type theory with coercive subtyping, as sketched by Coraglia and Emmenegger. We furthermore define semantic structure that interprets our type theory and prove a soundness result. Finally, we exhibit many examples of the semantic structure, yielding a plethora of interpretations.
This talk is based on joint work with Niyousha Najmaei, Niels van der Weide, and Paige Randall North published in doi:10.1145/3776725.
-
I forgot to announce this week's #HoTTEST seminar ahead of time, but the talk is now live on YouTube, so you can watch it there: https://youtu.be/dCOZGKbSQSo
Talk info:
Benedikt Ahrens
A type theory for comprehension categories
Abstract:
Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial morphisms between types; these morphisms are not used in the standard interpretation of Martin-Löf type theory in comprehension categories.
We develop a type theory that internalizes morphisms between types, reflecting this semantic feature back into syntax. Our type theory comes with Π-, Σ-, and identity types. We discuss how it can be viewed as an extension of Martin-Löf type theory with coercive subtyping, as sketched by Coraglia and Emmenegger. We furthermore define semantic structure that interprets our type theory and prove a soundness result. Finally, we exhibit many examples of the semantic structure, yielding a plethora of interpretations.
This talk is based on joint work with Niyousha Najmaei, Niels van der Weide, and Paige Randall North published in doi:10.1145/3776725.
-
I forgot to announce this week's #HoTTEST seminar ahead of time, but the talk is now live on YouTube, so you can watch it there: https://youtu.be/dCOZGKbSQSo
Talk info:
Benedikt Ahrens
A type theory for comprehension categories
Abstract:
Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial morphisms between types; these morphisms are not used in the standard interpretation of Martin-Löf type theory in comprehension categories.
We develop a type theory that internalizes morphisms between types, reflecting this semantic feature back into syntax. Our type theory comes with Π-, Σ-, and identity types. We discuss how it can be viewed as an extension of Martin-Löf type theory with coercive subtyping, as sketched by Coraglia and Emmenegger. We furthermore define semantic structure that interprets our type theory and prove a soundness result. Finally, we exhibit many examples of the semantic structure, yielding a plethora of interpretations.
This talk is based on joint work with Niyousha Najmaei, Niels van der Weide, and Paige Randall North published in doi:10.1145/3776725.
-
This week the #HoTTEST seminar presents:
Matteo Spadetto
Different descriptions of the semantics of computation axioms
The talk is at 11:30am EST (16:30 UTC) on Thursday, December 4. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract:
We discuss three ways of formulating the semantics of type theory (syntactic, (higher) categorical, and homotopy theoretic) and the relationships between them, focusing on concrete examples provided by axiomatic type constructors.
#HoTT @carloangiuli @emilyriehl -
Emily Riehl: How I became seduced by Univalent Foundations
[tbh I think shes only disclosing her theoretical motivations her; I recall she was posting questions about Linux distros a few years ago, and if we're honest being a nerd is the actual reason 99% of people get into HoTT]
https://www.youtube.com/watch?v=XIYoI5j5Flo&t=486s -
I enjoyed listening to this lecture, or at least the first half by Emily Riehl. About computer proof and mathematics. And scary vibe proofs and why they are nonsense
-
I enjoyed listening to this lecture, or at least the first half by Emily Riehl. About computer proof and mathematics. And scary vibe proofs and why they are nonsense
-
I enjoyed listening to this lecture, or at least the first half by Emily Riehl. About computer proof and mathematics. And scary vibe proofs and why they are nonsense
-
I enjoyed listening to this lecture, or at least the first half by Emily Riehl. About computer proof and mathematics. And scary vibe proofs and why they are nonsense
-
Readings shared November 7, 2025. https://jaalonso.github.io/vestigium/posts/2025/11/08-readings_shared_11-07-25 #AI #Agda #AlphaEvolve #FormalVerification #FunctionalProgramming #Haskell #HoTT #ITP #LLM #LeanProver #Math #Rocq
-
Polynomial universes in Homotopy Type Theory. ~ C.B. Aberlé, David I. Spivak. https://arxiv.org/abs/2409.19176 #ITP #Agda #HoTT
