Theorem 8.8

[TashiWalde]

1. Introduce the notions of left fibration and inner fibration as right orthogonal maps wrt {0} ⊂ Δ¹ and Λ ⊂ Δ², respectively.

2. Show that the notions of naive left fibration and left fibration agree. In particular, every projection ∑ A, C -> A of a covariant family C : A -> U is a left fibration (regardless of whether A is Segal).

3. Use the calculus of left orthogonal shapes to give a slick proof that every left fibration is an inner fibration.

4. Deduce that for every covariant family C : A -> U over a Segal type A, the total type ∑ C is also Segal. This addresses Formalise Theorem 8.8 of RS17 paper #12 (dare I say closes?) unless @cesarbm03 (or anyone else) still wants to implement an alternative proof.

Notes:

• Relies on Extension types up to homotopy #88.
• Relies on naiveextext, since it relies on is-right-orthogonal-to-shape-×, which does; see Refactor is-right-orthogonal-to-shape-× #91.
• The proof of is-naive-left-fibration-iff-is-covariant could probably be refactored and shortened now, since the only hard part thereof should be a consequence of extension-weakening.

[jonweinb]

For a possible proof of 2.) that doesn't assume the base to be Segal see [BW23, Proposition 6.1.1.

Edit: More precisely, the statement referred to is that any covariant family is inner.

[TashiWalde]

For a possible proof of 2.) that doesn't assume the base to be Segal see [BW23, Proposition 6.1.1.

Edit: More precisely, the statement referred to is that any covariant family is inner.

The proof I implemented also does not use that the base is Segal.

[jonweinb]

That looks great!

[fizruk]

Currently this does not properly compile for what seems to be a very weird reason: rzk complains that the variable naiveextext is declared as used but is actually unused. This is not true; and in fact rzk complains about the very same undeclared variable if I omit the uses (naiveextext). @fizruk, what am I missing here?

First, currently you get the following error:

unused variables
  naiveextext
declared as used in definition of
  is-segal-domain-inner-fibration-is-segal-codomain

This is because this definition does not actually rely on naiveextext, so uses (naiveextext) is not needed.
Once you remove that, everything typechecks on my machine with rzk-0.6.6 (I did not push any fixes for that).

[TashiWalde]

Currently this does not properly compile for what seems to be a very weird reason: rzk complains that the variable naiveextext is declared as used but is actually unused. This is not true; and in fact rzk complains about the very same undeclared variable if I omit the uses (naiveextext). @fizruk, what am I missing here?

First, currently you get the following error:

unused variables
  naiveextext
declared as used in definition of
  is-segal-domain-inner-fibration-is-segal-codomain

This is because this definition does not actually rely on naiveextext, so uses (naiveextext) is not needed. Once you remove that, everything typechecks on my machine with rzk-0.6.6 (I did not push any fixes for that).

Thanks! I must have gotten confused and removed the wrong instance of uses (naiveextext).

The merge-base changed after approval.