Naive left fibrations vs covariant families

[TashiWalde]

1) For an arbitrary map p : C -> A define the notion of being a naive left fibration, capturing homotopy-unique lifting along {0} -> \Delta^1.

2) Prove RS17, Theorem 8.5: a type family C : A -> U is covariant if and only if the projection \Sigma C --> A is a naive left fibration.

Notes:

• resolves #11.
• As a work-around for the lack of local variables in rzk, I have prepended the name of certain helper-terms with the random identifier "temp-b9wX" to avoid clashes in the global name space
• Ideally, this section/theorem should be a very special case of a general situation, where the inclusion {0} -> \Delta^1 is replaced by an arbitrary subshape \Phi -> \Psi. The proofs should be essentially the same, except that a lot of the helper notation (such as hom, dhom, coslice, etc) would have to be introduced first.
• Considerably simplified the proof compared to the previous version of this pull request using fiber induction.

[emilyriehl]

@fizruk just alerting you to @TashiWalde's use of local term names.

[TashiWalde]

@TashiWalde, this looks great.

One suggestion: immediately before defining is-naive-left-fibration-iff-is-covariant I'd define terms for the one way implications, eg is-naive-left-fibration-is-covariant proves covariance implies the naive left fibration condition. Then combine these terms to prove your if and only if.

The rationale is to sacrifice a bit of brevity here for usability later. @nimarasekh was recently applying the corresponding equivalence between is-covariant and has-unique-fixed-domain-lifts but because we'd just defined the iff he had to call first is-covariant-iff-has-unique-fixed-domain-lifts and second is-covariant-iff-has-unique-fixed-domain-lifts making for unreadable code.

Makes sense. Done!