Yannick Forster

Regarding 3 and 4 I can say that they are considered in my CSL paper discussing CT, and also cover them extensively in the thesis. I would say the reason...

Yes, I meant many-one reducibility with ` ~ LPO` (see my CSL paper for references) Lemma 2: `Funext /\ K LPO` Proof: Assume Fext and a many-one reduction function `F`...

Indeed, you need to use WLPO, but then Lemma 2 is easy to prove: ``` Definition K (f : nat -> bool) := exists n, f n = true. Goal...

Sorry, wrong button, I wanted to comment, not comment & close.

Yes, exactly. And since we know that funext does not imply WLPO (by a model of Coq in constructive set theory) and that CT together with funext does not imply...

> I agree it can be confusing but it is also interesting (see above). @mrhaandi do you agree on keeping `MM n` (maybe renaming it?) by putting `MMA n` upfront...

I don't think disabling CI on push in genral is the way to go. We want the CI to check our main branches (if only just for the badges in...

> Instead of `no-ci` keyword, maybe we could use the opposite `ci` keyword for commits on branches that are not PR which would then force the CI? That's not possible,...

Alternative: We disable CI if the branch name contains `no-ci` or the following are both true: the branch name is not `coq-*` and the commit message contains `no-ci`.

Logic is hard :) I'm trying again: We disable CI on `push` if either (1) `the branch names contains `no-ci` or (2) the branch name is not `coq-*` and the...