Comments (13)
Soon transp
will actually compute for inductive families, which should indeed make the equality from Agda.Builtin.Equality no lesser than Swan's Id.
from cubical.
you are truly dedicated scholars! :-)
from cubical.
Here's a small example.
open import Agda.Builtin.Equality
open import Agda.Primitive.Cubical renaming (primTransp to transp)
coerce : ∀ {A B : Set} → A ≡ B → A → B
coerce refl x = x
data D : Set where
d : D
test = coerce (transp (\ _ → D ≡ D) i0 refl) d
{-
C-c C-n test
Time: 2ms
coerce (transp (λ _ → D ≡ D) i0 refl) d
-}
from cubical.
from cubical.
Also using this trick of yours (which I tried myself to be able to do pattern atching on refl as you say) breaks computation, and this is a reason for not using the Agda builtin equality with cubical Agda.
from cubical.
That'd be great.
from cubical.
It will mean that I have to do nothing to port my development from Agda to cubical Agda.
from cubical.
@martinescardo: could you elaborate your comment about it breaking computation? (an example?)
from cubical.
In principle I could. But I will not try as I can't come up with a quick example. The way we discovered this, with Chuangjie, was when porting his PhD thesis Agda code to cubical.
http://www.cs.bham.ac.uk/~mhe/chuangjie-xu-thesis-cubical/
The first thing we tried was precisely your trick. Then when we tried to compute a modulus of uniform continuity, which should have been zero, we instead got a pattern matching runtime error.
We then instead used Swan's identity type and converted all definitions by pattern matching to uses of J, which took 10 hours.
from cubical.
I think it is enough to use an example that uses funext to compute a number, such as the one I gave in this file https://github.com/agda/cubical/blob/master/Cubical/Foundations/HoTT-UF.agda
from cubical.
@Saizan : I am puzzled how being able to compute with inductive families will make the above example work.
from cubical.
@amp12 To elaborate a bit, what happens is that Agda computes by matching on refl, but then instead of seeing a refl it sees something injected in the identity type by the equivalence you describe, which is not a refl, and then Agda doesn't know what to do.
from cubical.
@martinescardo In the future, coerce
will be automatically given extra clauses that will be able to deal with the residual transports on the index, as those too will be canonical elements, given that they cannot be represented by refl
.
from cubical.
Related Issues (20)
- Release version v0.5 while changing the release process HOT 12
- Citation.cff HOT 4
- Where should `π₁(RP²)` be? HOT 1
- Duplication of code in the library HOT 3
- Note licence exceptions HOT 2
- Slightly more generalized universes HOT 1
- Remove `isSet` accessors for algebraic structures? HOT 3
- Change the Constructor Name of Sequential Colimits HOT 2
- CI workflow with current agda master HOT 5
- Additions to the powerset module HOT 2
- Some Files are never checked HOT 6
- Suggested heap size for CI HOT 1
- SumMap in Algebra.Ring.BigOps should come from Semirings /Monoids HOT 1
- `make` fails on macOS Sonoma 14.2.1 with Apple Silicon HOT 1
- Algebraic geometry HOT 2
- Figure out why the CommRingSolver doesn't work in this case HOT 5
- Make the CommRingSolver work better with concrete rings
- More elegant construction of ZariskiLattice HOT 2
- Solver for wild categories
- arithmetic operations of Cubical.Data.Rationals is super slow 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 cubical.