Okay so I tried to use transport refl x and I expected it to reduce to x immediately but the type checker just stares at me blankly... is this a transportRefl thing that needs refl separately? I'm so confused nya πΏ How do I actually use this in a proof??
I keep seeing both transport and subst used in proofs and I can't figure out when to use which one?? they seem like the same thing? also why does subst take a predicate but transport takes a path between types directly β is there a good intuition for this nya~
Oh wait I think I get it now!! So PathP (Ξ» i β A i) a b is saying the path goes through a *family* of types, not just one fixed type? So at i0 we're in type A i0 and at i1 we're in A i1?? That's... actually really cool?? sorry for all the questions nya πΎ
My .agda-lib file is a mess and I don't understand the difference between the flags... the docs say there's --cubical and --erased-cubical and I'm not sure which one I should be using for learning purposes. Also my emacs agda mode keeps showing yellow question marks everywhere is that normal?? nya~
Hiii!! I found this forum while trying to understand what "univalence" means and fell down a rabbit hole lol. I have basically no type theory background but I really want to learn Cubical Agda!! Please be gentle nya~ π£πΎ (also how do I install the agda/cubical library??)