This should follow from the identical metatheoretic principle.

• define Y-combinator
• show that it is computationally equivalent to its one-step unfolding
• then I should be able to use meta-level löb induction to establish that this fixed point program has the right type

It's come to the point (#12) where it is necessary to implement substitution for the external language, so that we can state rules about dependent types. It will be necessary to implement this substitution, which is not so hard, but what will be a bit annoying is the following:

• carry over all the bureaucratic lemmas that I proved about substitution and renaming for the internal syntax

• relate external substitution to internal substitution in some suitable way. I expect that most of the external rules that talk about substitutions will need some lemmas that yank an external substitution outside the interpretation brackets, by composing the substitution with the interpretation map.

I think that all this will be very bureaucratic to prove, but it's a prerequisite for getting the rest of this done. It would be so nice if this could have been done automatically... That would be possible if instead I had developed a general notion of second-order abstract syntax, but that is a separate project which I don't have time to work on right now.

The names of many different constructs have changed in the draft paper over the past week; the coq formalization should be updated to reflect this.

Things like "extensionality" and "cper_valued" etc. seem like ideal uses of coq's type classes. Right now I just treat these as theorems and then add unification hints for them (Hint Resolve...). I think that type classes would work a bit better here, using the style from the Iris development.

I had intended not to formalize this just yet, but I think it's worth doing, and may be easier than I thought. (Note that there is still no need for indexing universes in clock contexts; by design, we intend this quantifier to not be irrelevant, since the whole point of it is to capture the notion of a clock-indexed family of types, which may of course vary in the clock in a non-trivial way.)

Need to go through and fix all the layout issues.

This is a grab-bag of random facts which should be reorganized and moved into the appropriate place; it also should use the notations that are now in Sequent.v.

Now that I've formalized sigma types, it's time to formalize dependent function types. Then, we can establish that these interact correctly with the later modality, giving us the final rules that we need.

This would help make some examples more convincing.

This clever operator I defined in order to validate the later modality rules without power objects being total can also be used to validate the intersection type rules, without using AUC. This would clean up some proofs and make them more systematic. I've already tried it out when proving that intersection commutes with sigma, and it worked really nicely there.

The latest version of Coq has ssreflect bundled with it; it would be good to get this building with that, and then the setup process for this development will be simpler.

https://github.com/coq/coq/releases/tag/V8.8.0

This module takes long enough to refine that it makes sense to break it up into multiple files (to take advantage of caching).

1. basic definitions about refinement matrices and behaviors
2. definition of monotone operator, and its least fixed point; rolling lemmas.
3. definition of universe hierarchy
4. refinement matrix functionality lemmas, culminating in theorem for the full hierarchy
5. proofs of closed "rules"

Now that I've defined the meaning of sequents, I can now proceed to give a version of them that use the raw/formal syntax. Then, I can write down and validate rules of inference in generality.

@jonsterling Why is the fact that the type of terms is inhabited stated as an axiom?
https://github.com/jonsterling/coq-guarded-type-theory/blob/c497808e6a3c8b1c3c4cbcdf16a7ce6cfbfe1689/theories/Term.v#L238

Why not prove it?

Lemma inh_tm : Later.Inh (Tm.t 0).
Proof.
  by exists Tm.unit.
Qed.

Currently, (external) open type equality factors through the internal open type equality: basically, if the two equands are equal types at equal total substitutions, then they are equal as open types.

This is a perfectly sensible notion of type equality, but it doesn't seem to work that well for some things. In particular, it is not necessarily the case that we can conclude /\k. A[k] = /\k. B[k] type from forall k, A[k] = B[k] type, so it does not seem possible (or at least easy) for us to prove the naïve formation rule for the intersection type. On the other hand, I have proved the version of this rule that uses equality in a universe, rather than general typehood. This version actually suffices for all applications, fwiw; just like how in Nuprl, you can't even state type equality without a universe.

Why does this happen? Remember that the judgments are interpreted with respect to the join of the type system hierarchy. So, ultimately the meaning of forall k, A[k] = B[k] type is something like forall k, there exists level i such that τ[i] != A[k] ~ B[k]. So, when we make the judgment generic in the clock, we have at each clock a level at which the equality holds, but we don't necessarily have a uniform such level. It seems like we ought to have one (some kind of "continuity" principle), but if it is even true, it would be very hard to prove.

We can get around the problem by simply defining the external type equality judgment so that it fixes a level outside the quantification over clocks: basically, we get around the problem of commuting those quantifiers by just changing a definition. This would be equivalent to just using equality-in-the-universe everywhere, but it might lead to easier-to-use rules. I may experiment with this at some point soon.

Right now it is not an emergency, since it is possible to just use equality in the universe for everything.

It's currently really awful to do induction on the type system as implemented by the least fixed point of this monotone operator... I wonder if there is a way to define another type by Coq's inductive type mechanism which can act as a "handle" for doing induction on this object.

(This ticket isn't super well-defined, but I want to think about it a bit.)

We need to define the open judgments in Coq, but I think that a first step would be to just give the version where you are open in a single variable; if we can prove the rule in question for this version, then we can surely prove it for the proper one.

To get this fired up, I need to implement simultaneous substitutions for the internal terms, and probably prove a few things about that. I know how to do that properly now, I just have to do it. I've been a little delayed in my progress because of the amount of time I've been having to put into the Systems and Constructive Logic courses.