I'm struggling sooo much because accessibility predicates aren't definitionally equal and I can't FORCE them to be equal in Agda as;ldhskdajga

yeah, I can transport along propositional equalities. but then what? my proofs are littered with the corpses of abandonded congs

@totbwf I can't rewrite by ∀ {k} {p q : Acc k} → p ≡ q 😩​

@totbwf not for accessibility, it seems
I also do induction on Acc and putting it in Prop would prevent me from eliminating to anything useful

@ionchy In that case, welcome to transport hell, enjoy your stay

Sign in to participate in the conversation

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.