Archived tweet #9200 from the @leastfixedpoint Twitter Archive

What is a good mathematical notation for existential packages? Say I have a type ∃τ.(F_τ × τ). How would I write an inhabitant of that type? Say τ=𝐍 and I have an f ∈ F_τ. Would an inhabitant be written (f, 123)? No mention of τ=𝐍?