Yiyun Liu yiyunliu · he/him
0 followers · 0 following
Repositories
4
 Projects Packages Public activity Starred repositories
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-10 01:15:53 -05:00
26e3c1c42a Add some cases for regularity
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-10 00:17:06 -05:00
c8e84ef93c Finish morphing
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-09 23:32:20 -05:00
2c47d78ad6 Add stub for morphing
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-09 20:41:35 -05:00
ea1fba8ae9 Finish syntactic renaming
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-09 17:05:49 -05:00
881b2e3825 Add missing premise
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-09 17:05:40 -05:00
df5c6bf0b1 Minor
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-09 16:46:24 -05:00
20bf38a3ca Fix the fundamental theorem yet again
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-09 16:34:43 -05:00
5b925e3fa1 Add beta and eta rules to syntactic typing
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-09 16:25:46 -05:00
133968dd23 Add semantic eta laws for pair
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-09 16:13:34 -05:00
ab1bd8eef8 Add semantic rules for function beta and eta
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-08 22:56:51 -05:00
4396786701 Reformulate renaming
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-08 22:52:56 -05:00
932662d5d9 Finish soundness proof
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-08 22:45:19 -05:00
0c83044d72 Update the typing rules with projections
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-08 22:38:35 -05:00
5996c45526 Finish the semantic projection rules
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-08 22:15:16 -05:00
02e6c9e025 Add pi and sig subtyping semantic rules
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-08 21:07:29 -05:00
916e0bcd75 Change the conversion rules to use Sub instead of Eq
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-08 20:37:59 -05:00
f483d63f01 Fix the definition of semleq
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-07 16:46:05 -05:00
0746e9a354 Finish subtyping semantics
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-07 01:19:27 -05:00
4bc08e1897 Add one interpuniv sub case
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-07 00:43:19 -05:00
707483d401 Add injectivity for subtyping