Continued from Path product and fundamental groupoids

(Associativity). Let be a fibrant simplicial set and let , and be paths in such that and . Then

Let be a point. Denote as the constant simplicial map for .

(Path Inverse). Let be a fibrant simplicial set and let be a path in . Then there exists a path such that .