A is local w.r.t Δ¹, i.e. the canonical map A -> (Δ¹ -> A) is an equivalence
A is left local, i.e. right orthogonal to {0} ⊂ Δ¹.
A is right local, i.e. right orthogonal to {1} ⊂ Δ¹.
Notes
~Marked as draft until #115 is merged.~
Since I already proved that every left fibration is inner (this was the heart of Thm 8.8), one could use this characterization together with #110 to obtain an alternative and arguably more conceptual proof of is-segal-is-discrete.
The following are equivalent to
is-discrete A:Ais local w.r.tΔ¹, i.e. the canonical mapA -> (Δ¹ -> A)is an equivalenceAis left local, i.e. right orthogonal to{0} ⊂ Δ¹.Ais right local, i.e. right orthogonal to{1} ⊂ Δ¹.Notes
is-segal-is-discrete.