Univalence

• Glue Type
• 0, 1, 2, W Types
• Coequalizer Type
• Hub-Spokes Disc Type
• Infinitesimal Shape Modality
• Univalence, Unimorphism, Minivalence
• Fibre Bundles
• Homotopy (Co)Limits, Suspension, Sphere, Truncations, Quotients
• Propositions
• K(G,n)