When messing around with some ideas that @cangiuli had regarding records, I came across the following crash:
import prelude
import hlevel
-- Equivalences.
def fiber (A : type) (B : type) (f : A β B) (b : B) : type := (a : A) Γ path B {f a} b
def is-equiv (A : type) (B : type) (f : A β B) : type := (b : B) β is-contr {fiber A B f b}
def equiv (A : type) (B : type) : type := (f : A β B) Γ is-equiv A B f
def equiv/id (A : type) : equiv A A :=
[ x => x,
x => [
[ x , i => x ],
fib i =>
let aux : π β A := j =>
hcom A 1 j {β i} {j _ => [
| j=1 β¨ i=0 => x
| i=1 => {snd fib} j
]
}
in [ aux 0, aux ]
]
]
#normalize {equiv/id {(x : type) Γ x}}
This crashes with:
[DEBUG] dispatch_rigid_hcom: lam[clo[lam[<anon>, el/out[ap[ap[var[2], var[1]], var[0]]]] ; [
[
] ; [ <let-sym> ]]]]
Core.Semantics.NbeFailed("Invalid arguments to dispatch_rigid_hcom")
I suspect that there's something fishy going on here with hcom_sg... It's worth noting this is fine for say, (x : type) Γ nat
When messing around with some ideas that @cangiuli had regarding records, I came across the following crash:
This crashes with:
I suspect that there's something fishy going on here with
hcom_sg... It's worth noting this is fine for say,(x : type) Γ nat