Jean Abou Samra (new account) on Nostr: Reference request: The truth value of a sentence φ in a topos (a morphism 1 → Ω) ...

Reference request:

The truth value of a sentence φ in a topos (a morphism 1 → Ω) can be defined by interpreting φ viewed as a λ-term into the topos as a cartesian closed category, where the constructs specific to higher-order logic are translated by: {x ∈ X | ψ[x]} is a notation for λ x ⋅ ψ[x]; x ∈ S is a notation for S(x); 𝒫(X) is a notation for X → Ω; ⊤, ⊥ : 1 → Ω and ∧, ∨, ⇒ : Ω → Ω → Ω come from the topos structure and ∀ x ∈ X, P[x] is ∀_X(λ x ⋅ P[x]) and ∃ x ∈ X, P[x] is ∃_X(λ x ⋅ P[x]) where ∀_X, ∃_X : (X → Ω) → Ω also come from the topos structure.

I'd like to put a precise account of the internal language on https://en.wikipedia.org/wiki/Topos#Elementary_topoi_(topoi_in_logic), and I think this is the simplest way to go about it, but on Wikipedia even a proof doesn't replace a reference, and the books I checked do it in a more complicated way.