Naive 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) Make progress towards proving 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 2.1) Define maps in both direction between the corresponding extension types (one is strict, one is weak) 2.2) One composite is definitionally the identity, yielding the easy direction of the theorem (<-)

Notes:

• Partially addresses #11.
• Relies on #46, which is not yet merged.
• As a work-around for the lack of local variables in rzk, I have prepended the name of certain helper-terms with "temp-Z7hl" 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 helpes notation (such as hom, dhom, coslice, etc) would have to be introduced first.

[jonweinb]

• 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 helpes notation (such as hom, dhom, coslice, etc) would have to be introduced first.

For the general context, in Synthetic fibered (infty,1)-category theory @UlrikBuchholtz and I call them "j-orthogonal" fibrations, see Observation 2.4.1 and Proposition 3.1.1.