Definition
In homotopy type theory, a fibrant type is a type equipped with the structure of a Kan Complex. We formally specify this by requiring operations for generalized transport and homogeneous composition. These operations ensure that we can extend any partial boundary of a higher-dimensional cube into a full cube, rendering path equality computationally well-behaved.