representing that the shape of is contractible (axiom R0?), and let be a closed interval or open interval in . Because the shape of is contractible, the shape of any closed or open interval in is contractible. Given a mapping , let us define the graph of the mapping as
in the product type . is continuous if the shape of is contractible: