Bidirectional typing for dependent types: Why are Sigma, Pi synthesized? According to the Pfenning philosphy of bidirectional typing, as also explained by Dunfield and Krishnaswamy 2013, constructors should be checked, while eliminators should be synthesized. Cconvention is followed for the most part in the tutorial Checking Dependent Types with Normalization by Evaluation: A Tutorial
by David Christiansen. I cannot explain some choices in the tutorial according to the Pfenning philosophy:
The types Sigma x A B and Pi x A B, Nat, Eq A from to, Trivial, and Absurd are all checked in synthesis mode. However, these are kind constructors, as they let us construct values that live in Univ. Why are they checked in synthesis mode?
Can we view these as eliminators of some object that I am unaware of? As an example of what I mean by this, recall that identifiers such as x are also run in synthesis mode. With a bit of squinting, one can convince themselves that identifiers are projections on the context Γ
, and thus deserve to be run in synthesis mode.
Is there a similar explanation for why Pi, Simga, Eq, Trivial, Absurd are typed in synthesis mode? what rule-of-thumb does one use to decide whether these should be typed  in checking or synthesis mode?
IMHO, it's not like constructors are checked, but introduction rules (including tuples, lambdas, data constructors, etc.) are checked (while elimination rules are synthesized). The kind constructors you mentioned are called formation rules, which are not introduction rules. You can also think this way: if a constructor is checked, then it has a corresponding eliminator which is synthesized. If type constructors should be checked, there should be a corresponding thing synthesized. But there's no such thing (you can't pattern match on $\cal U$).