Extra stuff about constant transport and equality.
Added interval HIT.
Function extensionality using inverval type.
Fix ambiguity from introducing positive sigma.
Added new lemma about transport.
Transport lemmas are in another module.
Simplify a function in PathStructure.Sigma.
Simplify a function in PathStructure.Sigma even more.