We consider the category Grpd (Asm (A) ) of groupoids defined internally to the category of assemblies on a partial combinatory algebra A. In this thesis we exhibit the structure of a π-tribe on Grpd (Asm (A) ) showing the category to be a model of type theory. We also show that Grpd (Asm (A) ) has W-types with reductions and univalent object classifier for assemblies and modest assemblies, where the latter is an impredicative object classifier. Using the W-types with reductions, we show that Grpd (Asm (A) ) has a model structure. Finally, we construct pGrpd (Asm (A) ), the full subcategory of partitioned groupoid assemblies, and show that pGrpd (Asm (A) ) has finite bilimits and bicolimits as well as showing that the homotopy category of the full subcategory of the 0-types of pGrpd (Asm (A) ) is RTA, the realizability topos of A.
Anthony Agwu (Mon,) studied this question.