Empty Type Properties
Table of Contents
1 Empty type properties
module Lib.Prop.Empty where
This file contains some results on the empty type.
1.1 Packages imports
The imported packages can be accessed via the following links:
import Stdlib.Prelude import Lib.FunExt import Lib.Data.Empty import Lib.Prop.Equiv
1.2 Dependent product over empty type
If B : Empty → U, then Πx: EmptyB x is contractible.
Empty/dependent-property/center (B : Empty → U) : (x : Empty) → B x = λx. ex-falso (B x) x Empty/dependent-property/contr (B : Empty → U) (f : (x : Empty) → B x) : Path ((x : Empty) → B x) (Empty/dependent-property/center B) f = eq-htpy Empty B ( Empty/dependent-property/center B) f ( λx. ex-falso ( Path (B x) ( Empty/dependent-property/center B x) ( f x)) x) Empty/dependent-property (B : Empty → U) : is-contr ((x : Empty) → B x) = ( Empty/dependent-property/center B, Empty/dependent-property/contr B)
As well, any type dependent type over a type that is equivalent to the empty type is contractible.
Empty/dependent-property-Equiv/center (A : U) (B : A → U) (e : Equiv A Empty) : (x : A) → B x = λx. ex-falso (B x) (Equiv/map A Empty e x) Empty/dependent-property-Equiv/contr (A : U) (B : A → U) (e : Equiv A Empty) (f : (x : A) → B x) : Path ((x : A) → B x) (Empty/dependent-property-Equiv/center A B e) f = eq-htpy A B ( Empty/dependent-property-Equiv/center A B e) f ( λx. ex-falso ( Path (B x) ( Empty/dependent-property-Equiv/center A B e x) ( f x)) ( Equiv/map A Empty e x)) Empty/universal-dependent-property (A : U) (B : A → U) (e : Equiv A Empty) : is-contr ((x : A) → B x) = ( Empty/dependent-property-Equiv/center A B e, Empty/dependent-property-Equiv/contr A B e)