  We investigate gradual variations on the Calculus of Inductive Construction
(CIC) for swifter prototyping with imprecise types and terms. We observe, with
a no-go theorem, a crucial tradeoff between graduality and the key properties
of normalization and closure of universes under dependent product that CIC
enjoys. Beyond this Fire Triangle of Graduality, we explore the gradualization
of CIC with three different compromises, each relaxing one edge of the Fire
Triangle. We develop a parametrized presentation of Gradual CIC (GCIC) that
encompasses all three variations, and develop their metatheory. We first
present a bidirectional elaboration of GCIC to a dependently-typed cast
calculus, CastCIC, which elucidates the interrelation between typing,
conversion, and the gradual guarantees. We use a syntactic model of CastCIC to
inform the design of a safe, confluent reduction, and establish, when
applicable, normalization. We study the static and dynamic gradual guarantees
as well as the stronger notion of graduality with embedding-projection pairs
formulated by New and Ahmed, using appropriate semantic model constructions.
This work informs and paves the way towards the development of malleable proof
assistants and dependently-typed programming languages.
