Amélia

Keep in mind that the results of `freeIn` on uninstantiated terms are.. dubious, at best, even when they aren't explosive: if we have a solved meta `?0 := λ x...

@ncfavier Can you change this so it does full normalization? Then I'm happy to merge it as a fix for the issue of thunks incorrectly being seen as escaping, even...

Because of the different scoping (visibility) rules. You could use Foo.constructor to get at Foo's constructor even if it's named and unexported (e.g. Foo lives in a private module which...

Having (finally! my apologies) looked at it, the issue is that the extended lambda is added to the "declares" set of the unfolding block, but *not* the unfolds set. That's...

Ah, there are two bugs here. One I didn't know of: The case split tactic should refuse to split on a type with at least one constructor not in scope....

I'm not in a situation where I can easily compile Agda today, but I believe this is my fault. Check out the normal form of `transportRefl (cong F (merid a)`...

Yeah, that one's _still_ on me — just more recently :sweat_smile: PathP does not take a line of levels, and `l` has to be made into a lambda, so the...

> I've rebased on current master (and pushed it to my branch) Thanks! I'll investigate.

@jespercockx I filed my fix at #6515; sorry about the merge conflict, but this time I can say it works. Or, at least, it doesn't not-work because of `transp` for...

A cubical `Sub A φ p` type can also be a definitional singleton, when `φ = i1`, with "center" `p 1=1`.