I'm studying Cubical Type Theory and I see the word "Kan operations" (ref1, ref2, ref3, and there are many more), which is related to "adding a cap to a tube" (can be also explained as "given a path between
b, and two paths that are between
d respectively, we can use Kan operations to get a path between
I wonder if there's any references that can explain where this "Kan" word come from -- what does it mean? Is that "Kan extensions" in Category theory?