-
Notifications
You must be signed in to change notification settings - Fork 59
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.
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
Add BAut types and two equivalent types of finite sets #29
Conversation
FinSet= = Subtype=-out FinSet-prop | ||
|
||
FinFS : ℕ → FinSet | ||
FinFS n = Fin n , [ n , idp ] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What does the middle F
stand for?
Thanks! This is great. Some lemmas in Pigeonhole.agda and FinSet.agda look quite essential and I might move them in to |
Oops sorry for the long delay. |
Let me create a separate issue for this. |
Since the FinSet equivalence requires ConstantToSetExtendsToProp, I've put FinSet.agda in theorems/homotopy, but that's not ideal. Perhaps it would be better to move ConstantToSetExtendsToProp to core and then put FinSet in core/lib/types?