prop

-- Ω, the universe of mere propositions (docs/NovaFoundation.txt).
--
-- Propositions are Ω-valued; Prf decodes one to a (realizer-irrelevant)
-- type; ∥T∥ squashes an arbitrary type into a proposition; ⋆ is the
-- canonical proof.

-- el-squash-i: ⋆ inhabits the squash of any inhabited type.
def truth : Prf ∥𝟙∥ ≔ ⋆
def eqSquash : (a : ℕ) → Prf (a ≡ a ∈ ℕ) ≔ λa. ⋆

-- el-prf-prop: proof irrelevance — any two proofs of a proposition are
-- judgementally equal.
def irrel : (p : Ω) (x : Prf p) (y : Prf p) → x ≡ y ∈ Prf p ≔ λp. λx. λy. ⋆

-- code-prop-eq (propositional extensionality): mutually implied
-- propositions are equal codes at Ω. Both squashees are inhabited, so
-- the two proposition codes are equal.
def propext : ∥𝟙∥ ≡ (Z ≡ Z ∈ ℕ) ∈ Ω ≔ ⋆

-- squashed reflection: a squashed equality reflects into a judgemental
-- equality (el-squash-e-eq + el-reflect).
def reflectSquash : (A : 𝕌) (a : El A) (b : El A) (h : Prf (a ≡ b ∈ _)) → Prf (a ≡ b ∈ _) ≔
  λA. λa. λb. λh. ⋆

-- ty-quot-cong: quotients by iff-equal Ω relations are the SAME type,
-- so a variable of one moves to the other with no coercion.
def quotIff : (A : 𝕌) (v : El A / (n m. ∥𝟙∥)) → El A / (n m. (Z ≡ Z ∈ _)) ≔ λA. λv. v

-- Impredicative connectives (Ω section, docs/NovaFoundation.txt): ⊤, ⊥,
-- ∧, ⊃ are the squashed types the theory itself names in its notes.
-- Nova has no primitive sum type, so even ∨ is impredicative — it
-- quantifies over ALL of Ω to pick out the least prop implied by both
-- disjuncts (the standard System F / CoC "encode through the
-- impredicative universe itself" trick). Introducing/eliminating these
-- needs `⋆ ⟨witness⟩` (el-squash-i, general form) and `squash-elim`
-- (el-squash-e-prf) — the squashees here are Π/Σ-shaped, not the
-- evident 𝟙-/≡-shapes bare ⋆ handles.
def ⊥ : Ω ≔ ∥𝟘∥
def ⊤ : Ω ≔ ∥𝟙∥
infixr 5 ∧
def ∧ : Ω → Ω → Ω ≔ λp. λq. ∥Prf p ⨯ Prf q∥
infixr 3 ⊃
def ⊃ : Ω → Ω → Ω ≔ λp. λq. ∥Prf p → Prf q∥
def ¬ : Ω → Ω ≔ λp. p ⊃ ⊥
infixr 4 ∨
def ∨ : Ω → Ω → Ω ≔ λp. λq. ∥(r : Ω) → (Prf p → Prf r) → (Prf q → Prf r) → Prf r∥

def andIntro : (p : Ω) (q : Ω) → Prf p → Prf q → Prf (p ∧ q) ≔
  λp. λq. λx. λy. ⋆ (x , y)
def andFst : (p : Ω) (q : Ω) → Prf (p ∧ q) → Prf p ≔
  λp. λq. λh. squash-elim h (u. u .π₁)
def andSnd : (p : Ω) (q : Ω) → Prf (p ∧ q) → Prf q ≔
  λp. λq. λh. squash-elim h (u. u .π₂)
def andElim : (p : Ω) (q : Ω) (x : Ω) → Prf (p ∧ q) → (Prf p → Prf q → Prf x) → Prf x ≔
  λp. λq. λx. λi. λf. squash-elim i (u. f (u .π₁) (u .π₂))

def impIntro : (p : Ω) (q : Ω) → (Prf p → Prf q) → Prf (p ⊃ q) ≔
  λp. λq. λf. ⋆ f
def impApply : (p : Ω) (q : Ω) → Prf (p ⊃ q) → Prf p → Prf q ≔
  λp. λq. λh. λx. squash-elim h (f. f x)

def orInl : (p : Ω) (q : Ω) → Prf p → Prf (p ∨ q) ≔
  λp. λq. λx. ⋆ (λr. λf. λg. f x)
def orInr : (p : Ω) (q : Ω) → Prf q → Prf (p ∨ q) ≔
  λp. λq. λy. ⋆ (λr. λf. λg. g y)
def orElim : (p : Ω) (q : Ω) (c : Ω) → Prf (p ∨ q) → (Prf p → Prf c) → (Prf q → Prf c) → Prf c ≔
  λp. λq. λc. λh. λf. λg. squash-elim h (u. u _ f g)

-- Logical equivalence, as a pair of implications (∧ + ⊃ already
-- give this for free — ↔ names it so callers stop re-deriving it)
infixr 2 ↔
def ↔ : Ω → Ω → Ω ≔ λp. λq. (p ⊃ q) ∧ (q ⊃ p)

def iffIntro : (p : Ω) (q : Ω) → (Prf p → Prf q) → (Prf q → Prf p) → Prf (p ↔ q) ≔
  λp. λq. λf. λg. andIntro _ _ (impIntro _ _ f) (impIntro _ _ g)
def iffLeft : (p : Ω) (q : Ω) → Prf (p ↔ q) → Prf p → Prf q ≔
  λp. λq. λh. impApply _ _ (andFst _ _ h)
def iffRight : (p : Ω) (q : Ω) → Prf (p ↔ q) → Prf q → Prf p ≔
  λp. λq. λh. impApply _ _ (andSnd _ _ h)

-- Curry/uncurry as a logical equivalence (each direction its own
-- lemma, rather than a literal code-prop-eq equality — code-prop-eq's
-- automatic search is still 𝟙-/≡-shaped only; only el-squash-i/
-- el-squash-e-prf were generalized).
def curry : (p : Ω) (q : Ω) (c : Ω) → Prf ((p ∧ q) ⊃ c) → Prf (p ⊃ q ⊃ c) ≔
  λp. λq. λc. λh. impIntro _ _ (λx. impIntro _ _ (λy. impApply _ _ h (andIntro _ _ x y)))
def uncurry : (p : Ω) (q : Ω) (c : Ω) → Prf (p ⊃ q ⊃ c) → Prf ((p ∧ q) ⊃ c) ≔
  λp. λq. λc. λh. impIntro _ _ (λpq. impApply _ _ (impApply _ _ h (andFst _ _ pq)) (andSnd _ _ pq))


-- Weak/intuitionistic excluded middle: ¬¬(p ∨ ¬p) holds constructively
-- for every proposition, no case split needed — a genuine stress test
-- of the restricted eliminators (elimination reaches only equations
-- and further props, never arbitrary types, yet this chains three
-- levels of squash-elim/⋆ and still lands exactly on Prf ⊥).
def notNotLem : (p : Ω) → Prf (¬ (¬ (p ∨ ¬ p))) ≔
  λp. impIntro _ _ (λk.
    impApply _ _ k
      (orInr _ _ (impIntro _ _ (λhp.
        impApply _ _ k (orInl _ _ hp)))))

-- Impredicative equivalence closure (the Ω section's flagship payoff
-- note: "least relations by intersection — e.g. an equivalence closure
-- r⁺ of an arbitrary relation r, defined by quantifying over all
-- Ω-valued relations containing r — with no inductive machinery").
-- rClosure r is the intersection of every equivalence relation
-- containing r, picked out by a single impredicative Π over Ω itself.
def rClosure : (A : 𝕌) → (El A → El A → Ω) → El A → El A → Ω ≔
  λA. λr. λa. λb. ∥ (R : El A → El A → Ω)
    → ((x : El A) (y : El A) → Prf (r x y) → Prf (R x y))
    → ((x : El A) → Prf (R x x))
    → ((x : El A) (y : El A) (z : El A) → Prf (R x y) → Prf (R y z) → Prf (R x z))
    → ((x : El A) (y : El A) → Prf (R x y) → Prf (R y x))
    → Prf (R a b) ∥

-- containment: instantiate the universal at the caller's own R
def rClosureContains : (A : 𝕌) (r : El A → El A → Ω) (a : El A) (b : El A) →
  Prf (r a b) → Prf (rClosure _ r a b) ≔
  λA. λr. λa. λb. λh. ⋆ (λR. λcont. λrefl. λtrans. λsymm. cont _ _ h)

-- reflexivity, symmetry, transitivity: rClosure r is itself an
-- equivalence relation, again by instantiating the universal
def rClosureRefl : (A : 𝕌) (r : El A → El A → Ω) (a : El A) → Prf (rClosure _ r a a) ≔
  λA. λr. λa. ⋆ (λR. λcont. λrefl. λtrans. λsymm. refl _)

def rClosureSymm : (A : 𝕌) (r : El A → El A → Ω) (a : El A) (b : El A) →
  Prf (rClosure _ r a b) → Prf (rClosure _ r b a) ≔
  λA. λr. λa. λb. λh.
    squash-elim h (u. ⋆ (λR. λcont. λrefl. λtrans. λsymm. symm a b (u _ cont refl trans symm)))

def rClosureTrans : (A : 𝕌) (r : El A → El A → Ω) (a : El A) (b : El A) (c : El A) →
  Prf (rClosure _ r a b) → Prf (rClosure _ r b c) → Prf (rClosure _ r a c) ≔
  λA. λr. λa. λb. λc. λhab. λhbc.
    squash-elim hab (uab.
      squash-elim hbc (ubc.
        ⋆ (λR. λcont. λrefl. λtrans. λsymm.
            trans _ _ _ (uab _ cont refl trans symm) (ubc _ cont refl trans symm))))

-- least-ness: rClosure r implies membership in ANY equivalence
-- relation containing r — unsquash the hypothesis and apply its
-- universal directly at the caller's Q, no induction, no recursion
def rClosureLeast : (A : 𝕌) (r : El A → El A → Ω) (Q : El A → El A → Ω)
  → ((x : El A) (y : El A) → Prf (r x y) → Prf (Q x y))
  → ((x : El A) → Prf (Q x x))
  → ((x : El A) (y : El A) (z : El A) → Prf (Q x y) → Prf (Q y z) → Prf (Q x z))
  → ((x : El A) (y : El A) → Prf (Q x y) → Prf (Q y x))
  → (a : El A) (b : El A) → Prf (rClosure _ r a b) → Prf (Q a b) ≔
  λA. λr. λQ. λcontQ. λreflQ. λtransQ. λsymmQ. λa. λb. λh.
    squash-elim h (u. u _ contQ reflQ transQ symmQ)