Null maps, null types and null type families

[fredrik-bakke]

Defines Y-null maps, Y-null types and Y-null type families, and establishes a few basic properties of these. Also formalizes the fiber condition for orthogonal maps. Part of #930. Depends on #1086.

• If A is a retract of B and S is a retract of T then diagonal-exponential A S is a retract of diagonal-exponential B T.
• Null types
  • Null types are closed under equivalences in the base and exponent
  • Null types are closed under retracts in the base and exponent
  • A type is Y-null if and only if the terminal projection of Y is orthogonal to the terminal projection of A
• Null families
  • Null families are closed under equivalences in the family and exponent
  • Null families are closed under retracts in the family and exponent
• Null maps, equivalence of
  • Fiber condition
  • Pullback condition
  • Right orthogonal map to terminal projection condition
  • Local at terminal projection condition
• Fiber condition for orthogonal maps

[fredrik-bakke]

I think this PR is mostly ready for review now, so I've marked it as such. 😁 I might end up wanting to use some of this in #1118 soon.