← Feed

Posts

• View post

  If A is subtype of A', let a : A, and define f : A' := a, should f : A hold judgmentally? How would you implement this? (subtyping can show up if you have subtyping-based cumulative universe)

• View post

  @jesper In definitional proof-irrelevance without K, how did you setup this beautiful Rocq code syntax highlighting?

• View post

  Cobisimulation

• View post

  where's the new pl minus context