Reorganize proof that discrete types are Segal

[TashiWalde]

Currently there are two completely independent proofs that every discrete type is Segal:

• The original proof from RS17 (Prop 7.3).
• Using the general setup of right orthogonality, a proof (which is essentially the one implicit in the proof of RS17, Thm 8.8) that every left fibration is an inner fibration. From this it follows that every left fibrant type (=discrete type) is inner fibrant (=Segal).

The second proof has many advantages over the first:

• Since most of the general machinery is abstracted out, the key computation steps are very transparent.
• It does not rely on a a long series of direct manipulations of extensions types.
• It proves a much stronger statement (the inner horn is left anodyne, rather than just weakly left anodyne).
• It directly implies other useful results such as Theorem 8.8.

I have therefore made the following changes:

• Moved the definition of left/right fibration and the proof of left fibration -> inner fibration to 07-discrete. This mirrors how inner anodyne shape inclusions are defined in 05-segal-types.
• Since it is a direct corollary, also moved the "categorical" version of Theorem 8.8 formulated with fibrations there. (The actual statement of Thm. 8.8 deals with covariant type families and remains in 08-covariant.)
• As a direct corollary, deduce that discrete types are Segal.
• Kept the original proof from RS17 in its own separate section renamed to Discrete types are Segal types (original proof of RS17). The constructed term is renamed to is-segal-is-discrete'. We can consider deleting it unless some of the intermediate calculations are deemed to still be useful.

[emilyriehl]

@TashiWalde this is great. I'll look at everything more detail this evening.

I'm the one who wrote the original formalization of [RS17, 7.3] and don't mind if that proof is replaced by the improved one. What do others think @jonweinb?

One more question: will this cause problems for @StiephenPradal 's open PR? If so, I'd appreciate guidance on how best to merge them.

[TashiWalde]

@TashiWalde this is great. I'll look at everything more detail this evening.

I'm the one who wrote the original formalization of [RS17, 7.3] and don't mind if that proof is replaced by the improved one. What do others think @jonweinb?

One more question: will this cause problems for @StiephenPradal 's open PR? If so, I'd appreciate guidance on how best to merge them.

All of the changes to 07-discrete are in one big chunk moved from 08-covariant with a few additions. I did not mess with any of the existing code (except adding a ' to the former is-segal-is-discrete). Therefore I don't expect any merging issues unless @StiephenPradal made any breaking changes to the terms that were there before.

[emilyriehl]

@TashiWalde I may have messed something up by merging your later pull request before this one. Let me know if you'd like me to revert that.

I was delaying this because I wanted to give others a chance to weigh in on the duplicated proof. Maybe we merge a version with both proofs now and then open a new PR to cut the old one? Or you can go ahead and cut that out now if you prefer.

[TashiWalde]

@emilyriehl I have resolved the merge conflict. It was not your fault; I had made a non-compatible change in another pull-request.

From my side the PR is now ready to be merged. I'll leave it up to you if you want to keep or discard the original proof. There is also no real hurry in merging this PR, so we can leave time for others to weigh in.

[emilyriehl]

Let's merge this now and we can make further changes later. I'm glad to hear the merge conflict wasn't my fault this time ;)