9
$\begingroup$

One of the frequent criticisms of HoTT is that it requires a lot of lemmata keeping track of which types are sets/propositions etc. And a frequent counterpoint is "It can be automated."

However, internet searches don't seem to yield many results. Are there actually automation work going on?

Also, proof automation / proof search in cubical type theories seems to require new mechanisms. Is there any literature discussing this?

Improve this question
$\endgroup$
3
  • $\begingroup$ I don't think that HoTT, or even CuTT for that matter, is very different from CIC / MLTT in this aspect. Any automation technique that works for them will pretty much transport easily to the univalent case... For instance, proving hProp instances can be discharged by typeclasses or canonical structures. $\endgroup$
    – Pierre-Marie Pédrot
    Commented Feb 22, 2022 at 10:24
  • 1
    $\begingroup$ @Pierre-MariePédrot The most brain-twisting part of coding in CuTT is to keep track of boundary conditions, which, MLTT/CIC solvers cannot do without significant changes. For instance, Agda currently gives up on non-trivial boundary conditions. $\endgroup$
    – Trebor ♦
    Commented Feb 22, 2022 at 13:10
  • $\begingroup$ @Trebor can you say more about this (the type of automation you think is most needed for HoTT, or the problems in HoTT which are most “brain-twisting”) in your question? $\endgroup$
    – Jason Rute
    Commented Feb 22, 2022 at 13:29

2 Answers 2

Reset to default
7
$\begingroup$

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 bookkeeping to carry around proofs that something is of a certain h-level; and proving that newly introduced data types preserve a certain h-level requires quite lengthy encode-decode proofs (see for instance this proof that lists preserve the h-level of the carrier)

It's important to keep in mind that current formalizations of HoTT are still quite prototypical and based on proof assistants which had been devised before the idea of h-levels came to type theory. Future theorem provers will likely give more support to work with h-levels, possibly by introducing h-levels judgmentally like Arend does (thereby giving an orthogonal stratification of types to universe levels).

Automating the bookkeeping should be an engineering task, deriving automated proofs about the h-level of a type or filling cubes in Cubical Agda is in general undecidable. I'm not aware of any work in this direction, but there are lots of interesting things to be done. Similarly to, e.g., termination checking, there are probably lots of things that can be done automatically even if the problem can't be solved in general.

Improve this answer
$\endgroup$
12
  • $\begingroup$ Do you know if Arend’s built in support for h-levels is similar to what you had in mind? $\endgroup$
    – Jason Rute
    Commented Feb 22, 2022 at 13:01
  • $\begingroup$ I believe so, homotopy levels in Arend share many characteristics with truncation levels as studied in the HoTT book. However, I do not understand the theory behind Arend and can't say what is actually going on there. $\endgroup$
    – Maximilian Doré
    Commented Feb 22, 2022 at 16:06
  • $\begingroup$ Filling-cubes is actually undecidable even for squares since one can represent words problem of groups by using paths and squares. But it seems possible if your type has very simple fundamental group, it's kind of algebraic topology's business. $\endgroup$
    – KANG Rongji
    Commented Feb 22, 2022 at 18:44
  • $\begingroup$ I'm not sure what post of mine you're referring to either. I'm generally quite happy with the way that h-levels are inferred using typeclasses in Coq. I don't use Agda as much, but in talking to people who do, I definitely notice that they're missing out on this automation and it's causing them pain. Typeclasses can't infer everything, and there are probably some ways that the typeclass system could be improved, but by and large I think they infer most of what could reasonably be expected to be automatically inferrable. $\endgroup$
    – Mike Shulman
    Commented Mar 4, 2022 at 23:20
  • 1
    $\begingroup$ Although Agda does have "instance arguments" which I think could be used in the same way in principle. $\endgroup$
    – Mike Shulman
    Commented Mar 4, 2022 at 23:21
2
$\begingroup$

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/assets/wg6/stockholm-kickoff-slides/dore-europroofnet-stockholm-slides.pdf

It brute forces all possible hcomps by enumerating "compatible" faces.

Edit: paper is out: https://arxiv.org/abs/2402.12169

Improve this answer
$\endgroup$
2
  • 2
    $\begingroup$ Thanks for mentioning this--I've been meaning to update my answer once a preprint is out (which is hopefully soon). The solver now works for different cubical type theories, and in the case of Dedekind cubes can do something a bit more clever than enumerating all faces. $\endgroup$
    – Maximilian Doré
    Commented Dec 14, 2023 at 15:14
  • $\begingroup$ @MaximilianDoré Could you please ping me when the preprint is out? Excited to see it $\endgroup$
    – ice1000 ♦
    Commented Dec 14, 2023 at 18:06

Not the answer you're looking for? Browse other questions tagged or ask your own question.