Fix #7529: treat LevelUniv in Cubical Agda
#7534
Conversation
| Prop _ -> pure Nothing | ||
| SSet _ -> pure Nothing | ||
| Inf _ _ -> pure Nothing | ||
| LevelUniv -> pure Nothing |
There was a problem hiding this comment.
Yes, this matches isCoFibrantSort, we only return Just here for the True cases there: that's when a pi type should support kan operations.
There was a problem hiding this comment.
Perhaps it would make sense to tie this code more closely to isCofibrantSort (or at least to add some documentation of the connection).
| IntervalUniv -> noTranspSort | ||
| Prop{} -> noTranspSort | ||
| _ -> noTranspError b' | ||
| LevelUniv -> noTranspSort |
| Univ _ _ -> pure Nothing | ||
| Inf _ _ -> pure Nothing | ||
| IntervalUniv -> pure Nothing | ||
| LevelUniv -> pure Nothing |
| Prop _ -> pure Nothing | ||
| Inf _ _ -> pure Nothing | ||
| IntervalUniv -> pure Nothing -- ClosedType? (See comment on CType.) | ||
| LevelUniv -> pure Nothing -- TODO: Or some ClosedType? |
There was a problem hiding this comment.
Oh, actually IntervalUniv should have the check that's at SSet atm. I suppose that got overlooked when IntervalUniv got introduced. OTOH it seems then that the whole ClosedType thing might not actually be needed then.
I think it was meant to support path constructors for HITs, but those needed special care anyway?
There was a problem hiding this comment.
I raised this as #7542.
|
I have not dived into the issue, but from what I remember, there already were some known issues with regards to mixing |
| _ -> noTranspError (Abs "i" (unDom t)) | ||
| t <- open $ Abs "i" (unDom t) | ||
| Univ UType l -> Just <$> open (lam_i (Level l)) | ||
| Univ _ _ -> pure Nothing |
There was a problem hiding this comment.
This change of the behavior for Prop (from exception to Nothing) makes the failing test for #6060 pass.
However the test passes when we have Propω instead of Prop, see #7535.
Shouldn't Prop be treated like SSet here? If not, why not?
I think this case distinction deserves a comment on what the intended behavior is on a higher level, in particular, when to return Nothing and when to throw an exception.
It also feels this should not be an adhoc pattern matching, but a function to be called with a proper documentation. There are similar matches allover the Cubical Agda code base.
70f52ae to
f2baffb
Compare
Issue #7529 demonstrates that
--level-universeis not (fully) integrated with--cubical(yet).In this PR, I expand some catch-alls for sorts to fill in some speculative values for the new sort
LevelUniv.I need some experts to look over this: @arthur-adjedj @plt-amy @mortberg @Saizan @sattlerc
One should probably check the Cubical Agda code for more such matches on sorts, e.g. grep for
Type lorgetSort.Related are also:
Commits: