A type dependent on a value

Stream: Is there code for X?

[Mingli Yuan]

I am a newbie, I had checked the docs and only found this topic was mentioned in https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#dependent-types , but the vec example seems only for education purpose, so I want to found a working inductive type example like vec which have a type param of size, or something similar.

[Eric Wieser]

The vec example is a toy version of docs#Vector

[Mingli Yuan]

Aha, just a function, I find it, thanks

[Eric Wieser]

docs#Fin is another common one

[Mingli Yuan]

My problem at hand is to formalize a path group in some geometry space, but we know the 1 in a group is unique, so I need fix the paths in a group to a base point. So I think I need to create a dependent type to a point. Is my understanding correct? Or any advice?

[Jireh Loreaux]

Are you looking for the docs#FundamentalGroupoid ?

[Mingli Yuan]

Thanks, Jireh, it is a groupoid, but a little bit strength, for any two point, there is a path connecting them. Its purpose seems not to be the same with fundamental groupoid ...

[Jireh Loreaux]

Can you state more precisely what you want? Do you want homotopy classes of paths?