TIL I can define equality like this:

data _≡_ {ℓ} {A : Set ℓ} (a : A) : A → Set where
refl : a ≡ a

I'm not sure why it's letting me put the equality in a smaller universe than the type it's quantifying over. Seems suspicious

@ionchy i read something about this!!
there are type theories where this is perfectl sound afaik

@ionchy actually now that i think about this, i'm not sure if this would be OK in HoTT since paths are predictive and there are "larger" path universes than in the base universe
but it's OK with K since this could just be part of an impredictive Prop, right?

@pounce idk, I just wrote it in Agda and it type checked
lemme try turning off K

@pounce yep, it's fine to put it in Set and have --without-K

@ionchy hmm that sounds inconsistent to me but what do i know

@pounce I think the reason it's okay (if it is...) is because you can't project out the thing in the larger universe
Or at least, the thing itself is already in the type, so you're just retrieving information you already had
I'm guessing problems only start when you store big things in the constructors and its type is blind to it

@pounce this would be a nice little question to ask about when the proof assistants stackexchange is up lol

@ionchy yeah you can't "project out" (except for doing operations on paths, like finding the fundamental group)
but that doesn't mean there aren't problems that it could cause

consider HoTT with HITs
HITs give suspensions, so for every type A we have ΣA with a path space just as complicated as A. If somehow all of these path spaces could live in the same universe, then you could have infinitely complicated path types.
you could have a groupoid that matches any (inaccessible) set

like ik u can't project out, but you can't project out of Prop and that doesn't mean that inconsistencies in Prop stay there

sorry if im making absolutely no sense, just the bonkers resident HoTT dork speaking

@pounce 🤔 maybe you could get an inconsistency this way then in cubical agda
...although this inductive type would evidently not be cubical's equality derived from path types, and the equalities that HITs construct wouldn't be this either

@pounce I think as long as the "real" identity type you have doesn't behave like this (living in smaller universes), you can't get an inconsistency in the way you describe

@ionchy @treppenverstand said that any equality is equivalent to any other equality in the same type theory

anyway i ran this in my agda 2.6.2 and it stopped working if I added

{-# OPTIONS --without-K #-}


@pounce ?? what else did I have on that without-K still worked 😵‍💫

@pounce strange that without-K toggles this... thought it mostly dealt with when you could no longer unify metavars

Sign in to participate in the conversation

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.