module foundation.subtype-identity-principle where
open import foundation-core.subtype-identity-principle public