We present an internalization of the 2-groupoid (or rather groupoidoid) interpretation of the calculus of construction that allows to realize proof irrelevance, reasoning modulo and a weak form of the univalence axiom. As an example, we show that in our setting, the type of Church integers is equal to the inductive type of natural numbers.