Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix univalence and displayed cat stuff #59

Merged
merged 5 commits into from
Oct 16, 2024
Merged

Fix univalence and displayed cat stuff #59

merged 5 commits into from
Oct 16, 2024

Commits on Oct 14, 2024

  1. chores 

    * tidy up arguments for notation classes
* do justice to `is-invertible`, now it's called `quasi-inverse`
* uniform quantifier syntax + display forms
    Your Name committed Oct 14, 2024
    Configuration menu
    Copy the full SHA
    3d2e85b View commit details
    Browse the repository at this point in the history

  2. * generalize a few lemmas about quasi-inverses 

    * add bi-invertibility notation
* tweak foundations, move congruence definition out
* bi-invertibility is a proposition
  for any structure with a notion of morphism
  and an associative and unital composition
  on any universe level
    Your Name committed Oct 14, 2024
    Configuration menu
    Copy the full SHA
    8f05b3d View commit details
    Browse the repository at this point in the history

Commits on Oct 15, 2024

  1. convert biinv to a record, add extensionality instance

    Your Name committed Oct 15, 2024
    Configuration menu
    Copy the full SHA
    5e2098b View commit details
    Browse the repository at this point in the history

  2. cat: displayed equivalences, univalence, displayed univalence

    Your Name committed Oct 15, 2024
    Configuration menu
    Copy the full SHA
    fa56e87 View commit details
    Browse the repository at this point in the history

Commits on Oct 16, 2024

  1. simplify + performance optimisation 

    146 (!) seconds faster
    Your Name committed Oct 16, 2024
    Configuration menu
    Copy the full SHA
    5ce76fa View commit details
    Browse the repository at this point in the history