2LTT, External Cubes and Cube Filling Macros

[kangrongji]

This PR contains macros that allow users to fill cubes, for both non-dependent and dependent, provided assumption of h-levels. To achieve this, I choose the approach that using 2LTT to define the external cubes and relate them to internal ones, that means I have to mess up with SSet stuff (though only very basics are needed).

It's done, but I think the organization of files demands some discussions. The library has almost nothing about 2LTT, so I collect a few things in a new file Cubical.Foundations.2LTT. But I'm not sure if it's the right place. What's the maintainers opinion? @mortberg @ecavallo @felixwellen

Also, should I place all the macros inside the fold Cubical.Tactics? There are some in Cubical.Foundations.Cubes.Macros, and one in Cubical.Foundations.2LTT transforming internal natural numbers to external ones.

[kangrongji]

I add new terms to .gitignore for better working in VSCode.

[ecavallo]

Before we merge, we should have a plan for the changes coming in Agda 2.6.3. In 2.6.2, the interval is in your Typeᵉ, but in the development version it lives in its own sort, which in particular isn't closed under data types. This will be a problem for your Iˣ and ∂Iˣ.

We discussed adding products to the interval sort in agda/agda#5439. But as I understand it, @plt-amy plans to rework the interval implementation to be closer to cooltt, which I think would make Iˣ and ∂Iˣ even more impossible. @plt-amy, any thoughts on how best to proceed?

[kangrongji]

@ecavallo Is your proposal in agda/agda#5439 a way to implement the 2LTT-style cofibrant types? That sounds great. I'm not familiar with cooltt. Don't they support manipulation on intervals?

[plt-amy]

Thanks for the ping @ecavallo.

This code will essentially be invalid with the changes I want to make to the interval type, and how it's handled in Agda. In particular, to fix agda/agda#6016 (which I consider to be a critical bug in Agda's implementation of cubical type theory), we need something akin to what Jon Sterling calls the cubical phase distinction. The specific details of how the cubical phase restriction will be handled aren't particularly important (but you can bug me about them on Discord if you'd like to hear my current thoughts — they're always evolving) but the gist of it is the following maxim:

Cofibrations can only refer to explicit i : I-typed variables.

While it won't be literally like this, an approximation of the phase distinction is:

Every function into the interval is judgementally constant.

So, in particular, this won't be allowed:

∂Iˣ : {n : ℕᵉ} → Iˣ n → I
∂Iˣ {n = 0ᵉ} _ = i0
∂Iˣ {n = 1ᵉ} i = i ∨ ~ i
∂Iˣ {n = suc (suc n)} (i , φ) = i ∨ ~ i ∨ ∂Iˣ φ

More accurately, the definition itself will be allowed, but this won't:

∂Cubeᵉ : (n : ℕᵉ) (A : Type ℓ) → Typeᵉ ℓ
∂Cubeᵉ 0ᵉ _ = Unit*ᵉ
∂Cubeᵉ (suc n) A = (φ : Iˣ (suc n)) → Partial (∂Iˣ φ) A

When I get around to doing my changes (not in time for 2.6.3, but I will make them), the term Partial (∂Iˣ φ) A won't be well-typed, and there will be no way of making it typed. The reason for this (very strong) restriction is that cubical type theory, in the form of checking under cofibrations, comes with a limited form of equality reflection; and, to type-check that, we need that the equational theory of cofibrations be decidable.

With ∂Iˣ, we have a cofibration which depends on a natural number, and while this specific case is fairly benign, the only sensible way to forbid all the problematic cases is to ban such things outright.

[kangrongji]

With ∂Iˣ, we have a cofibration which depends on a natural number, and while this specific case is fairly benign, the only sensible way to forbid all the problematic cases is to ban such things outright.

It is weird to make cofibrations depend on internal natural number, but it also absolutely makes sense to have them depend on external natural numbers. If I got it right, one cannot have cofibrations depend on any parameters, even if it's from pretypes in SSet. That means the 2LTT in agda will be incapable of doing anything non-trivial about boundary restrictions, partial elements and cubical subtypes. I'm not sure if it's a proper direction. In particular it will be much harder or even impossible to deal with more involved homotopy-theoretic notions like simplicial types in a cubical way.

[plt-amy]

Whether or not they're in SSet doesn't matter: type checking will still be undecidable if you have non-interval-stuff in your interval. Strictly speaking the interval shouldn't even be a type, fibrant or not, since interval binders are semantically their own thing, distinct from lambda binders.

[ecavallo]

I suppose it would still be possible to use reflection to build the Partial (i₁ ∨ ~ i₁ ∨ ... ∨ iₙ ∨ ~ iₙ) A types?

[plt-amy]

Right.

[kangrongji]

The macro could still work by more reflections, just without well-typed intermediate steps. (In fact it cannot even now due to lacking of funExt in the external level)

[kangrongji]

But I still feel bad that we haven't find good ways to combine cubical stuffs and 2LTT. They're really cool things and we can't get everything cool we want.

[ecavallo]

@kangrongji, are you willing to rewrite to move the dependency on natural numbers into the reflection?

Alternatively, a stopgap solution that would work for 2.6.3 (but not the glorious future) would be to use the fact that the interval sort is still a subsort of SSet. So you could define

record Iᵉ : SSet where
  field
    ival : I

(or however you want to call it) and use that instead of I inside your SSet constructions.

[kangrongji]

@ecavallo The ad-hoc solution can be done much quicker, at least before the release of 2.6.3. I'm not sure how far things may work if natural numbers dependency is removed. It's a bit technical to convince agda's typechecker on boundary constrains, as you can see from those helper functions at the beginning of the Cubes.External file. We can just leave this PR open for a while before I figure out what I could do.

[ecavallo]

OK, thanks!

[ice1000]

The macro could still work by more reflections, just without well-typed intermediate steps. (In fact it cannot even now due to lacking of funExt in the external level)

There is a quick way of rescue: we create a fibrant Bool alias as IFibrant and we pretend it's I, and use reflection to translate it into real I.

[ice1000]

@plt-amy I have a minor question: since you said ∂Iˣ is allowed but Partial (∂Iˣ n) A isn't -- can we actually allow Partial x A : SSet where x is neutral, and require u : Partial x A where x must be judgmentally variables?

I understand that from a philosophical perspective one shouldn't do this, but I think you only need such strong restriction when you want to put the cofibration into the lhs of the turnstile. In Partial x A itself, I think it's fine.

(I think it probably does not make sense to allow the same for PartialP though)

[jonsterling]

Unless I misunderstand @ice1000, this doesn’t really make sense to me as you cannot ask for something to be neutral or a variable “judgmentally”, since all judgments are by definition closed under substitution. If you control the binding site though, there might be more that you can do.

[ice1000]

Unless I misunderstand @ice1000, this doesn’t really make sense to me as you cannot ask for something to be neutral or a variable “judgmentally”, since all judgments are by definition closed under substitution. If you control the binding site though, there might be more that you can do.

What if I say syntactically?

Semantically, I think of functions eliminating SSet/Type types into ISet as meta level functions which works similarly to tactics, but written in a language similar to the object language.

What do you mean by "control the binding site"? In particular I'm not sure what is a "binding site", is it where you introduce or use the binding?

[ice1000]

Looks soooo wacky. I feel giving up on that.

Edit: no, I think this feature should be useful.

[kangrongji]

@jonsterling I'm by no means expert of implementation, so I can only make sense of a small part of you guys' discussion. But I'm very curious if the following phenomenon relevant: If one want to define partial element on φ ∨ ψ, it needs to provide one element on φ and another on ψ. But only in very restrictive cases the compatible condition on φ ∧ ψ could be automatically checked. I think it's even impossible to figure out what is φ ∧ ψ. I mean, it could even be just 0 or 1 but not able to be deduced by machines. Similar things happen when pattern matching on HIT when one want to define, say, a square and its boundary is given. Another example is when one have a function f : I → I, which depends on some parameters in twisting way, and it could be just f i ≡ i, but still it cannot be checked if λ i → p (f i) is just p itself. I guess these are examples of what people call equality reflection? I'm sorry I don't really understand this word.