mevenlennonbertrand

mevenlennonbertrand, 23 days ago to random

I just realised that inductively defining an indexed inductive family T : B -> Type and then quotienting each T x by a family of relations R : Π x : B, T x -> T x -> Type is not the same as the corresponding quotient inductive type: if R is not a congruence, then the quotient-after-the-fact is not right, because it does not know that you also want to quotient the other fibers by their relation.

Is this the whole point of QITs that had completely gone over my head until now?

mevenlennonbertrand, 1 month ago to random

Hi Mastodon! It seems there's quite a bit of fun discussions happening around here, so here I come.

Probably some of you know me already. For those who don't, I'm a post-doc at Cambridge, playing with proof assistants – mostly trying to convince them that they are reasonable pieces of software.

Anyway, I hope to enjoy it around here 🙂