Add unit and sigma types

[Vtec234]

I worked on this for my master's thesis. The PR adds a contractible unit type and dependent sums with an extensionality principle.

[mr-ohman]

Thank you @Vtec234 for contributing to this project. Great work! I like how you were able to reuse the definition of Π in the logical relation and generalize it to work with both Π and Σ. The other changes and refactoring are also welcome. The only thing I found confusing was the naming choice of star for the value of Unit, I would have preferred tt or <> as those are more standard. Other than that, everything looks good.

[Vtec234]

Thanks for your comments, I'm happy to contribute! Regarding star, I was going by the name used in the Lean standard library. I see that both Coq and Agda do use tt, so I tried changing the term to that just now. But then it causes naming conflicts with Agda's own constructor! And for me, <> only brings to mind Haskell monoids or OCaml inequality. Perhaps the slightly offbeat naming is acceptable to avoid conflicts - what do you think?

[mr-ohman]

Yes, while it is possible use tt for both simultaneously with qualified names, it may be annoying and inelegant to have to keep referring to them that way. For <> I was thinking of it as a substitute for () from Haskell and ML, but I forgot about <> being Haskell mappend and OCaml inequality. I wasn't aware of star in the Lean standard library, so I think it is fine to use that name, both to avoid conflicts as you said and since it is at least standard in one language.

Since that was my only objection, I will go ahead and merge this. Thanks again for your contribution!