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

Show the univalent sub-universe structure of UFin #55

Closed
vikraman opened this issue Jan 25, 2021 · 0 comments · Fixed by #60
Closed

Show the univalent sub-universe structure of UFin #55

vikraman opened this issue Jan 25, 2021 · 0 comments · Fixed by #60
Assignees
@vikraman
Labels
proof
Projects
Pi+

Comments

@vikraman
Copy link
Owner

No description provided.

@vikraman vikraman created this issue from a note in Pi+ (To do) Jan 25, 2021
@vikraman vikraman added the proof label Jan 25, 2021
@vikraman vikraman self-assigned this Jan 25, 2021
vikraman added a commit that referenced this issue Jan 26, 2021
@vikraman
Prove the univalent subuniverse structure of UFin
91bbc86 
Fixes #55
@vikraman vikraman mentioned this issue Jan 26, 2021
Merged
@vikraman vikraman moved this from To do to In progress in Pi+ Jan 26, 2021
vikraman added a commit that referenced this issue Jan 26, 2021
@vikraman
Prove the univalent subuniverse structure of UFin
856e9b0 
Fixes #55
vikraman added a commit that referenced this issue Jan 26, 2021
@vikraman
Prove the univalent subuniverse structure of UFin
fd08634 
Fixes #55
vikraman added a commit that referenced this issue Jan 26, 2021
@vikraman
Prove the univalent subuniverse structure of UFin
eaf3792 
Fixes #55
vikraman added a commit that referenced this issue Jan 26, 2021
@vikraman
Prove the univalent subuniverse structure of UFin
911baa7 
Fixes #55
Pi+ automation moved this from In progress to Done Jan 26, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@vikraman vikraman

Labels
proof
Projects
Pi+
Done
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Prove the univalent subuniverse structure of UFin vikraman/2DTypes
1 participant
@vikraman