New answers tagged

2 votes

Is there a way to incorporate K's axiom while keeping the system consistent with univalence?

It looks like Meven's answer is what you want, but just to answer the core question as stated: I'm seeking methods akin to Streicher's K Axiom, which asserts the uniqueness of identity proofs, but ...
Joey Eremondi's user avatar
5 votes
Accepted

Is there a way to incorporate K's axiom while keeping the system consistent with univalence?

The question seems to boil down to the implicit assumption that pattern-matching needs uniqueness of identity proofs to work "well" (I will refrain from calling it "axiom K", ...
Meven Lennon-Bertrand's user avatar
3 votes

Is there a way to incorporate K's axiom while keeping the system consistent with univalence?

The Equations package for Coq/Rocq provides pattern matching without K, as described by Cockx, Devriese, and Piessens and comparable to Agda --without-K, for all ...
James Wood's user avatar

Top 50 recent answers are included