feat(kernel/inductive): add API for retrieving the number of indices in an inductive datatype
feat(kernel/inductive): expose 'get_elim_name' API
feat(kernel/inductive): add get_num_minor_premises and get_num_type_formers APIs
feat(library/definitional/rec_on): automatically generate rec_on function for inductive datatypes
feat(library/definitional/induction_on): automatically add 'induction_on'
refactor(library/data/unit): make unit universe polymorphic

Motivation: we need it for "padding".
Example 1: defining a n-ary tuple type.
Example 2: defining cases-on for mutually recursive datatypes
feat(library/hott) add adjointification proof up to two gaps
fix(library/hott) close gaps and clean up adjointification proof
feat(library/hott) add the proof that the inverse of an equivalence is an equivalence

This is done by changing the order of theorems and using the adjointification.