UniAgda.Core.SetsAndLogic.ContrPropSet1Type

Table of Contents

1 Prelude

2 Definition

2.1 Contractible Types

A contractible type is one which has a point and a path from every other point to that point.

isContr :  {i}
          (A : Type i)
            Type i
isContr A = Σ[ a  A ] ((x : A)  a  x)

2.2 Propositions

A proposition is a type with a path between any two terms.

isProp :  {i}
         (A : Type i)
          Type i
isProp A = (x y : A)  x  y

We define the type of propositions to be the Sigma type of types that are propositions.

Prop_ : (i : Level)
         Type (lsuc i)
Prop i =  Σ[ A  Type i ] (isProp A)

2.3 Sets

A set is a type with all path spaces propositions.

isSet :  {i}
        (A : Type i)
         Type i
isSet A = (x y : A) (p q : x  y)  p  q
sets-have-prop-ids :  {i}
                     (A : Type i)  isSet A
                      (x y : A)  isProp (x  y)
sets-have-prop-ids A H x y = H x y

A set is then a type with a proof that it is a set. This is how we define the type of sets.

Set_ : (i : Level)
        Type (lsuc i)
Set_ i = Σ[ A  Type i ] (isSet A)

2.4 1-Types

We can extend this higher and we get a tower of \(n\)-types. We just define 1-types here.

is1type :  {i}
          (A : Type i)
           Type i
is1type A = (a b : A)  isSet (a  b)

Author: James Leslie

Created: 2021-03-27 Sat 10:47