Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I don’t think I’ve seen it. But I’m fuzzy on property 1. Why isn’t this automatic from the fact that $P$ already carries an internal Heyting algebra structure?
Being an internal Heyting algebra means it has internal finite meets and joins, i.e., nullary and binary, and representables are tiny but they aren’t finite. The representable-indexed meets and joins give you universal and existential quantifiers respectively.
Thanks. I don’t think I’ve heard the expression “representable-indexed meets and joins”.
1 to 5 of 5