Rename std-qc-open-prop to contains-invertible-prop

[felixwellen]

I think our definition of open propositions is wrong. is-qc-open says that a proposition P is open iff there are $n\in\mathbb N$ and a vector v of length n such that there is an i such that $P$ is equivalent to v i being invertible. But we should ask P to be equivalent to the existence of an i such that v i is invertible. This means that the proof that open propositions are double negation stable does not work as it is now. Don't know if this affects anything else.

[MatthiasHu]

It looks right to me: https://github.com/felixwellen/synthetic-geometry/blob/927e3414e3e520d0b52fbc9e1bff8429cd98c3cb/SyntheticGeometry/Open.lagda.md?plain=1#L48

[felixwellen]

Ah. I misread... I thought std- means standard in the sense of standard open.... Should we rename that?

[MatthiasHu]

Right, the name std-qc-open-prop is not very good. But I don't know what to call it right now.

[MatthiasHu]

By the way the D(f) should I think be called "basic open" to be clear (not "standard open").

[MatthiasHu]

Maybe call std-qc-open-prop just contains-invertible-prop!

[felixwellen]

Yes. I guess then it is all good and it's just me ;-) Standard open in the sense we have now actually fits well with standard finite.

[felixwellen]

Maybe call std-qc-open-prop just contains-invertible-prop!

That would have prevented me from misreading.

[felixwellen]

Not sure about the -prop, but I think it is a good name.

[MatthiasHu]

Not sure about the -prop

Yes, I see. An alternative would be to bundle the hProp right away and just have:

contains-invertible : {n : ℕ} → FinVec ⟨ k ⟩ n → hProp _
contains-invertible v = ∥ Σ[ i ∈ Fin _ ] (v i) ∈ k ˣ ∥ₚ

(Or with ∃ and isPropPropTrunc.)

[felixwellen]

Yes, I think this (with ∃) should be the best way to do it (unless we use the non-prop version a lot, but I don't think we do or will).