Closed TashiWalde closed 1 year ago
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.
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.
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).
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
, souses (naiveextext)
is not needed. Once you remove that, everything typechecks on my machine withrzk-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)
.
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 familyC : A -> U
is a left fibration (regardless of whetherA
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 typeA
, the total type∑ C
is also Segal. This addresses #12 (dare I say closes?) unless @cesarbm03 (or anyone else) still wants to implement an alternative proof.Notes:
naiveextext
, since it relies onis-right-orthogonal-to-shape-×
, which does; see #91.is-naive-left-fibration-iff-is-covariant
could probably be refactored and shortened now, since the only hard part thereof should be a consequence ofextension-weakening
.