Add types for the "fiber of El at A under \phi"

Open jonsterling opened this issue 5 years ago • 1 comments

This will be needed to satisfactorily implement #26 / #25.

In particular, what I want is to be able to write something like a : Univ such that under phi, el(a) = A. This is not currently expressible as a cubical subtype of Univ, but it is semantically sensible and maybe even operationalizable.

Apr 29 '20 19:04 jonsterling

I have thought about it some more and I am not certain that the pay-off is big enough to justify this ticket being implemented just now. I will continue to ponder a bit.

Apr 29 '20 21:04 jonsterling