Skip to main content
19 votes
Accepted

Is there any example of a dependent product that makes sense in a non-type-theory context?

Dependent products appear explicitly in many places in mathematics, long predating category theory and type theory. The terminology they most often appear under is “the product of a family of sets” (...
Peter LeFanu Lumsdaine's user avatar
18 votes
Accepted

What is Artin gluing, and how is it useful in proving meta-theoretic properties?

Here is my attempt at a bird's eye view of what gluing is about. I will not go into the details of the actual gluing construction, and instead refer to the various surveys for this. Proving meta-...
Loïc Pujet's user avatar
  • 1,479
17 votes
Accepted

What are the motivations for different variants of categorical models of dependent type?

I would divide these models into three general groups. Structures that are more "categorical", arising naturally from categories "in nature" without the need for strictification ...
Mike Shulman's user avatar
  • 3,180
14 votes
Accepted

What are "fibration/cofibration" in type theory and what are their intuitions?

So, first, the origin of this term in the context of cubical type theory comes from its intended semantics, which are in turn inspired by the model-categorical semantics of homotopy type theory. Let's ...
daniel gratzer's user avatar
13 votes

Is there any example of a dependent product that makes sense in a non-type-theory context?

Dependent products exist in set theory, and are used routinely in this setting. The trick is that they are typically used without mentioning that they are indeed dependent products. Two examples that ...
Pierre-Marie Pédrot's user avatar
11 votes

Is there any example of a dependent product that makes sense in a non-type-theory context?

A very elementary example is the rule for multiplying out brackets: $$\prod_{i\in I}\sum_{j\in J_i}x_{ij}=\sum_{f\in\prod_iJ_i}\prod_{i\in I}x_{if(i)}$$ where the dependent product appears in the ...
Oscar Cunningham's user avatar
11 votes
Accepted

What is realignment and is it useful in non-univalent theories?

This is a very good question. What is realignment for? One application of realignment that is particularly useful is to construct a cumulative hierarchy of universes; what cumulativity means in the &...
Jonathan Sterling's user avatar
10 votes

What are "fibration/cofibration" in type theory and what are their intuitions?

Let me provide a slightly watered up supplement of Gratzer's answer. In the beginning, mathematicians need to study spaces by considering how other spaces cover(*) them. For example, if you have a ...
Trebor's user avatar
  • 4,015
10 votes

What is Artin gluing, and how is it useful in proving meta-theoretic properties?

I would like to post an example that I hope will be illuminating to understanding some concepts in topos theory, and especially Artin gluing. This is a translation and polishing of my own answer a few ...
Trebor's user avatar
  • 4,015
8 votes
Accepted

Ergonomic use of multicategories in proof assistants

[I'm posting this by proxy for Astra, who is having technical difficulties posting on this site.] Hey! I recently completed a large scale formalisation in which I independently rediscovered cartesian ...
8 votes
Accepted

Seven Trees in One, or How to formalize the Semiring of Types?

The main subtlety is that it doesn't seem easy to automate the semigroup equational reasoning required by Seven Trees in One, but if we put that process aside (like, accepting to do it by hand, which ...
Li-yao Xia's user avatar
  • 1,792
6 votes

Are there proof assistants whose core uses category theory?

It only makes sense to embed a certain aspect of mathematics into the core of a proof assistant if that has a significant advantage over defining the same aspect on top of the core. For example, it ...
Andrej Bauer's user avatar
  • 9,553
6 votes
Accepted

Semantics of type theory

There are many tools regarding the semantics of type theory. On one hand, we may organize the structure of substitutions explicitly, resulting in notions such as CwFs, CwAs, natural models, display ...
daniel gratzer's user avatar
5 votes
Accepted

Interpretation of dependent types: Coherence

I have commented with Curien's 1990 work on substitution up to isomorphisms, but you said it's too old. Here's a quite new reference, by Lumsdaine and Warren: https://arxiv.org/abs/1411.1736 It was ...
ice1000's user avatar
  • 6,256
5 votes

Is there any example of a dependent product that makes sense in a non-type-theory context?

In formal semantics of natural languages we do have examples too: https://ncatlab.org/nlab/show/dependent+type+theoretic+methods+in+natural+language+semantics
Alexandre Rademaker's user avatar
5 votes

Is there any example of a dependent product that makes sense in a non-type-theory context?

I'm really interested in a good explanation too but I'll give my little bit. I prefer thinking in terms of spans rather than slice categories. Recall composition of spans is basically dependent sum. ...
Ms. Molly Stewart-Gallus's user avatar
5 votes

Examples of formalisation of abelian categories

The UniMath library has a formalization on abelian categories and homological algebra (done by Tommi Pannila). See: Abelian categories Short exact sequences Five lemma The documentation can be found ...
Niels's user avatar
  • 51
4 votes

What are the motivations for different variants of categorical models of dependent type?

I think they are here to show a particular thing of interest, because they're all very similar. There is always a category for contexts whose pullbacks correspond to substitutions, there's always a ...
ice1000's user avatar
  • 6,256
4 votes

Reasoning about CwFs in a proof assistant

I am really sorry to inflict this upon you but could you not use a parametrised module instead of a record together with an ...
gallais's user avatar
  • 1,256
4 votes

Formal proof of “functional” / purposive law

As a preamble, let me point out that complete (logical) formalization of a legal system is a very long-standing dream. Back in 1987 at the first international conference on Artificial intelligence and ...
Alex Chichigin's user avatar
3 votes

Reasoning about CwFs in a proof assistant

Coq has a notion of a hint database which can contain either equalities or proofs of an equivalence relation other than equality, and an "autorewrite" tactic which repeatedly rewrites ...
Patrick Nicodemus's user avatar
2 votes

Formalization of a model of ∞-category in a proof assistant

Much of current research is aimed at developing a nice theory in which one can reason about higher categories directly, as opposed to taking traditional models of higher categories and verifying them ...
Maximilian Doré's user avatar
2 votes

Formalization of a model of ∞-category in a proof assistant

I believe rzk is the Proof Assistant and sHoTT is the formalisation. :) On the other hand, they work with synthetic ∞-categories, not a model, so maybe this doesn't really answer your question...
Alex Chichigin's user avatar
2 votes
Accepted

Is every type-theoretic function ℕ → A extensionally equal to one written in terms of the ℕ-eliminator

With function extensionality this is trivially true, because f = elim (f 0) (\n _ -> f (suc n)). Without function extensionality I suspect it is not true, but ...
Trebor's user avatar
  • 4,015
2 votes

Stacks versus universes

I am not a topos theorist, but here are my 2cts as a type theorist, so take it with a grain of salt. If you have universes in your ambient topos, whatever it is, then you can define internally there ...
Pierre-Marie Pédrot's user avatar
2 votes

Is there any example of a dependent product that makes sense in a non-type-theory context?

I was unsure about giving another answer because this is sort of shaky. You know how I mentioned adjoints to composition (which is basically pullback) are dependent producty? A concrete example I ran ...
Ms. Molly Stewart-Gallus's user avatar
1 vote
Accepted

Proving that applicative functors compose

I would like to know how this is actually carried out in a tactic-based approach The theorem functor.comp.is_lawful_applicative in Lean's ...
Jason Rute's user avatar
  • 8,835

Only top scored, non community-wiki answers of a minimum length are eligible