Move torsoriality of the identity type to foundation-core.torsorial-type-families

[EgbertRijke]

This PR moves the torsoriality of the identity types to foundation-core.torsorial-type-families. Previously it was in contractible-types. I also slightly updated the prose, and fixed imports wherever they were broken because of this move.

[fredrik-bakke]

Super!

[fredrik-bakke]

Would it be nice to also mention in the ## Idea section that the identity type family is the motivating example of the definition?

[EgbertRijke]

Question: When running make website I get the following error. What should I do to make it go away?

Traceback (most recent call last):
  File "/Users/egbertrijke/Repositories/agda-unimath/./scripts/preprocessor_citations.py", line 8, in <module>
    import pybtex
ModuleNotFoundError: No module named 'pybtex'

[fredrik-bakke]

Question: When running make website I get the following error. What should I do to make it go away?

Traceback (most recent call last):
  File "/Users/egbertrijke/Repositories/agda-unimath/./scripts/preprocessor_citations.py", line 8, in <module>
    import pybtex
ModuleNotFoundError: No module named 'pybtex'

You have to install the latest requirements. What you're missing is the pybtex module

[VojtechStep]

I'd expect this property to be recorded in foundation.identity-types - are there circular dependency issues with that?

[fredrik-bakke]

Question: When running make website I get the following error. What should I do to make it go away?

Traceback (most recent call last):
  File "/Users/egbertrijke/Repositories/agda-unimath/./scripts/preprocessor_citations.py", line 8, in <module>
    import pybtex
ModuleNotFoundError: No module named 'pybtex'

You have to install the latest requirements. What you're missing is the pybtex module

The command would be pip3 install -r scripts/requirements.txt unless you've recently updated python with brew. If so, the command is pip3 install -r scripts/requirements.txt --break-system-packages

[EgbertRijke]

I'd expect this property to be recorded in foundation.identity-types - are there circular dependency issues with that?

You're right, and yes that leads to cyclic module dependencies that I don't want to solve now.

[EgbertRijke]

Would it be nice to also mention in the ## Idea section that the identity type family is the motivating example of the definition?

On it.

[EgbertRijke]

I removed "chore" from the title of this PR because I wrote a somewhat substantial amount of text and that should definitely count as content creation.