A Universe of Sorts

Key idea: define a notation called Γ => Δ iff the conjunction of sentences in gamma implies the disjunction of terms in delta.
Why would anybody do this? isn't this weird?
It's because we first note what we need to think about consequence, validity, and unsatisfiability.
d1 is a consequence of Γ iff g1 /\ g2 .. /\ gn => d1
d1 is valid iff empty => d1, or written differently, 0 => {d1}.
Γ is unsatisfiable iff g1 /\ ... /\ gn => False, or written differently, Γ => 0
Thus, see that on the RHS, we need a set with 0 or 1 inhabitant. We can think of this as Maybe, smooshed together with \/, since we want the empty set to represent False.
Recall that haskell teaches us to replace failure with a list of successes!
Thus we should use Γ => Δ where on the RHS, we have a list that is smooshed together by or ( \/)!
Great, we have successfully invented sequents.
Another motivation is that given a sequent like { A_i } => { B_j }, we can have this mean one of four things: (1) ΠA_i => ΠB_j, (2) ΠA_i => ΣB_j, (3) ΣA_i => ΠB_j, and (4) ΣA_i => ΣB_j.
We should rule out any ΣA_i => X, since these maps can be further decomposed into a family of maps f_i: A_i => X.
We should rule out any Y => ΠB_j, since these can be decomposed into a family of maps g_j : Y => B_j.
The only indecomposable map left is ΠA_i => ΣB_j, which is exactly the structure that sequents have!

§ You Could Have Invented Sequents