Christian Sattler
Christian Sattler
Before I used master, I used 5.1.0 (I was not able to compile 5.2.0 due to #250). However, that did not even pass this check: ```terminal ~$ proot true proot...
Corollary 8.4 from the cited paper is not relevant here (as explained by Jasper). Prop is fully compatible with cubical type theory (as mentioned by @Saizan in #5897). If we...
> However, this cannot be deduced merely from identities of De Morgan Algebra. That's right. But it's not needed. The implication `i ∨ j = 1 → P constant` holds...
> In that case, should `qux` and `quux` be definitionally equal? They are the same except for the second argument in `transp`, and the second argument is only used to...
They have different reduction behaviour: when the proposition encoded by the second argument is true, the transport is guaranteed to evaluate to the third argument. So they cannot be identified.
> While we are at it, is it sound to reason in the real interval [0;1] with min, max, and (1-) to derive theorems of a free de Morgan algebra?...
> But both `(i ∧ k) ∨ ~ (i ∨ k) = 1` and `(i ∨ ~ k) ∧ (~ i ∨ k) = 1` iff `i = 0, j...
> True but it seems like we only care about the condition when they are equal to `1`. Why?
> What if we use [0;1] ^ n instead? Probably.
@howsiyu I think I understand now what you mean. You are asking why we take an interval variable `i` as second argument instead of the proposition encoded by `i =...