Skip to main content
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
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
9 votes

When is hProp equivalent to the subobject classifier?

$\newcommand{\Type}{\mathsf{Type}}$ $\newcommand{\hProp}{\mathsf{hProp}}$ $\newcommand{\isEmbedding}{\mathsf{isEmbedding}}$ Recall from HoTT book Definition 4.6.1 that $f : A \to B$ is an embedding ...
Andrej Bauer's user avatar
  • 9,553
8 votes
Accepted

Unnecessary premises in a congruence rule of homotopy type theory?

The premises 1. and 2. are called presuppositions (although the terminology is not fixed), as they are needed only to ensure that the judgements appearing in the rule are well-formed (more formally, ...
Andrej Bauer's user avatar
  • 9,553
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
7 votes
Accepted

What is the state of the art in proof automation in HoTT/CuTT?

Coq uses type classes to infer h-levels in some simple cases automatically (see Sect. 3.2). Agda does not have an automatic way to manage or infer h-levels. I agree that one has to do quite a bit of ...
Maximilian Doré's user avatar
6 votes
Accepted

Can I specify `refl`'s parameter explicitly in Agda?

You absolutely can. Given the default definition of the identity type data _≡_ {a} {A : Set a} (x : A) : A → Set a where refl : x ≡ x we have that ...
Matthew McQuaid's user avatar
5 votes
Accepted

In HoTT, what is the hlevel of $S^1$?

If you want a cubical solution, then here it is. It is straightforward to obtain a similar HoTT solution. As a reminder, the h-level hierarchy goes ...
Trebor's user avatar
  • 4,015
4 votes

When is hProp equivalent to the subobject classifier?

The precise answer is going to depend on exactly what formulation you are using of the two definitions, but there are a few things to be aware of in any case. For any universe $U$ the projection map $\...
aws's user avatar
  • 301
4 votes
Accepted

Is there any universe polymorphic version of univalence?

At least in papers on cubical type theory, 'respecting equivalence' is somewhat independent of universes. There is a judgmental notion of paths: $$Γ,i ⊢ T\ \mathsf{type} \\ Γ,i ⊢ t : T$$ The top being ...
Dan Doel's user avatar
  • 982
4 votes

What is the intuition behind the `Glue` type in Cubical Type Theories

I would say Glue types are the "in-between" part of a path equality. For instance, take the Booleans. We can construct a type $$\mathsf{Glue}^i_{\color{brown}{\mathbb B}}\begin{cases} (i=0) \...
Trebor's user avatar
  • 4,015
4 votes
Accepted

When is hProp equivalent to the subobject classifier?

In Proposition 11.3 of All (∞,1)-toposes have strict univalent universes I proved that the interpretation of type theory in any $(\infty,1)$-topos — with the universes interpreted by object ...
Mike Shulman's user avatar
  • 3,180
3 votes
Accepted

Can Hyperreal exist a axiom-free implementation in HoTT?

For a survey of formalizations of real numbers you can look at Formalization of real analysis: a survey of proof assistants and libraries by Sylvie Boldo, Catherine Lelay and Guillaume Melquiond. ...
Andrej Bauer's user avatar
  • 9,553
3 votes

Benefits of HoTT compared with dependent type theory like what Lean does?

My non-expert take is the main benefits of HoTT outside of homotopy theory are related to isomorphism invariance. Specifically, in many dependent type theories (but not in Lean's), all constructions ...
Sebastian Reichelt's user avatar
3 votes

Parametricity and data kinds

I'm not sure there's any ready made system for precisely this (at least, I haven't seen/understood it yet). There's lots of adjacent work, though. Cavallo & Harper isn't it, because it's modelling ...
Dan Doel's user avatar
  • 982
2 votes

Parametricity and data kinds

If you just want to avoid having a case on MonoMaybeS, you should be able to parametrize over it and use any version of parametricity that handles dependent types. ...
Jason Gross's user avatar
  • 1,537
2 votes
Accepted

Higher Observational Type Theory: variables becoming free in reduction rules

I would guess the issue comes from the $\Delta$ you assumed was missing. As far as I can tell, when living over a general telescope, already $$ Id_{Δ.(Π (x : A) B)}^δ(f, g) ≡ \Pi (u, v : A). \Pi(p: ...
Meven Lennon-Bertrand'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

What is the state of the art in proof automation in HoTT/CuTT?

I'm surprised that the other answer poster Maximilian Doré did not mention their own work Automating Kan composition which is automation for cubical type theories: https://europroofnet.github.io/...
ice1000's user avatar
  • 6,256
1 vote

How does Prop relate to h-prop and double negation?

You have a looot of questions. It's a bit hard to see how many are there, but let me write something that I believe to answer your questions. A type A is said to ...
ice1000's user avatar
  • 6,256

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