Indexed and fibred categorical concepts are widely used in computer science as models of logical systems and type theories. Here we focus on Hoare logic and show that a comprehensive categorical analysis of its axiomatic ...