Comments (6)
I think this is okay for pretypes, but I don't think it naively works for Kan types.
from sml-redprl.
Since the Enlightenment of Kinds, this of course works for discrete types. What do we want except embedding the entire Nuprl type theory?
from sml-redprl.
@favonia Indeed!
By the way, Mark Bickford has proved that some version of family intersections are Kan for the CCHM type theory; see the bottom of http://www.nuprl.org/wip/Mathematics/cubical!type!theory/.
I wonder if we can get such a result in our setting (low priority, but interesting).
/cc @cangiuli
from sml-redprl.
At least, I think he is proved this; I'm not familiar enough with that development to really understand it.
from sml-redprl.
Just to update the public record, Mark Bickford has defined family intersections for CCHM cubical sets, but has not proven they are Kan.
from sml-redprl.
Mark Bickford has defined family intersections for CCHM cubical sets, but has not proven they are Kan.
Alright. It should be possible to add them for discrete Kan types and stable ones to RedPRL, and that more or less matches Mark's progress, I guess.
from sml-redprl.
Related Issues (20)
- Eta and EqCap of fcom types
- Eta for V types
- Auto tactic should peek into the equations in coe/hcom instead trying all rules in sequence
- Better freshing/renaming? HOT 5
- Change the syntax of Thm? HOT 2
- Make U^pre and U^hcom Kan again! HOT 3
- donβt require uppercase operator names HOT 8
- Sync .mlb and .cm
- Typed binders for theorems and definitions?
- Bug in HCom.Eq HOT 2
- Bug in the logic of Restriction.restrict? HOT 3
- Inductive types in multiverses
- Better handling of stuck terms?
- Remove aliases VV and WU?
- Handling of meta variables in Restriction.restrict HOT 1
- Add typed beta rules for (vproj x (vin x...)) etc. HOT 2
- Coe of V is wrong
- Recursor for parametric type seems broken HOT 2
- "Compile SML raised: Option" on initial build HOT 4
- link to picture in README.md is invalid HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
π Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. πππ
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google β€οΈ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from sml-redprl.