Contractible Types

Definition: A type A is contractible if it comes equipped with an element of type $\Sigma_{(c:A)} \Pi_{(x:A)} c=x$.

isContractible : (A : Type) -> Type
isContractible A = Σ A (λ c -> (x : A) -> x ≡ c )

Remark: Contraction is Homotopy from constant function to identity function

-- definition of unit type
data Unit : Type where
  tt : Unit

-- induction principle
ind_Unit : {P : Unit -> Type} -> P tt -> (x : Unit) -> P x
ind_Unit p tt = p

-- proof that unit type is contractible
UnitContractible : isContractible Unit
UnitContractible = tt , ind where
  ind : (x : Unit) -> x ≡ tt
  ind = ind_Unit {P = λ y -> y ≡ tt} refl

-- for any `a : A`the the type $\Sigma_(x:A)(a=x)$ is contractible

from_a_Contractible : {A : Type} (a : A) -> isContractible (Σ A (λ x -> a ≡ x))
from_a_Contractible x = (x , refl) , {!!}

Singleton induction

Definition A Type A satisfies singleton induction if for every type family B over A, the map $$ \text{ev-pt} : ( \Pi_{(x:A)} B(x)) \to B(a), \quad \text{ev-pt} (f) := f(a)$$ has a section.

ev-pt : {A : Type} {B : A -> Type} {a : A} -> (( x : A ) -> B x) -> B a
ev-pt {A} {B} {a} f = f a

-- identity type
id : {A : Type} -> (A -> A)
id a = a

-- compose
_∘_ : {A B C : Type} -> (B -> C) -> (A -> B)  -> (A -> C)
f ∘ g = λ x -> f (g x)

-- type of homotopies
_~_ = {A : Type} {B : A -> Type} -> (f g : (x : A) -> (B x)) -> (x : A) -> ((f x) ≡ (g x))

sec : {A B : Type} (f : A -> B) -> Σ (B -> A) (λ g -> ((f ∘ g) ~ (id B)))

dependent function $\Pi_(x:A)B(x)$

dep-fun = {A : Type} -> (A -> Type)