[moi2388]

Yes, I found the same and was very pleasantly surprised when I first learned about the ideas of cubical type theory.