For completeness I have added to discrete infinity-groupoid a section on “discrete principal -bundles” and how they are modeled by simplicial principal bundles, using material given there and at other places on the Lab
]]>I have edited discrete infinity-groupoid a little bit more in an attempt to slightly polish the exposition further.
]]>I have added a section a s a cohesive (oo,1)-topos
]]>for completeness I think there is a point in having an entry discrete infinity-groupoid. So I have created it.
(We already had discrete group with the same purpose.)
]]>