\begin{code}

{-# OPTIONS --without-K #-}

module tiny-library where

Type = Set 

_∘_ : {X Y : Set} {Z : Y  Set}  ((y : Y)  Z y)  (f : X  Y)  (x : X)  Z(f x)
g  f = λ x  g(f x)

data _+_ (X₀ X₁ : Type) : Type where
 in₀ : X₀  X₀ + X₁
 in₁ : X₁  X₀ + X₁

record Σ {I : Type} (X : I  Type) : Type where
  constructor _,_
  field
   π₀ : I
   π₁ : X π₀

open Σ public

data  : Type where
  : 
  : 

data _≡_ {X : Type} (x : X) : X  Type where
 refl : x  x



J : {X : Type}  (A : (x x' : X)  x  x'  Type)
    ((x : X)  A x x refl)
     {x x' : X} (r : x  x')  A x x' r
J A f {x} refl = f x

J' : {X : Type} (A : {x y : X}  x  y  Type)
    ({x : X}  A (refl {X} {x}))  {x y : X} (p : x  y)  A p
J' {X} A φ = J {X}  x y p  A {x} {y} p)  x  φ {x})

transport : {X : Type} {P : X  Type} {x y : X}  x  y  P x  P y
transport {X} {P} refl p = p

ap : {X Y : Type} (f : X  Y) {x₀ x₁ : X}  x₀  x₁  f x₀  f x₁
ap f refl = refl

ap-functorial : {X Y Z : Type} (f : X  Y) (g : Y  Z) {x₀ x₁ : X}  (p : x₀  x₁) 
                 ap g (ap f p)  ap (g  f) p
ap-functorial f g refl = refl

apd : {X : Set} {Y : X  Set} (f : (x : X)  Y x) {x x' : X} (p : x  x')  transport p (f x)  f x'
apd f refl = refl 

undo'-Σ-≡ : {X : Type} {Y : X  Type} (w w' : Σ \(x : X)  Y x) 
      w  w'  Σ \(p : π₀ w  π₀ w')  transport {X} {Y} p (π₁ w)  π₁ w'
undo'-Σ-≡  w .w refl = refl , refl

undo-Σ-≡ : {X : Type} {Y : X  Type} (x x' : X) (y : Y x) (y' : Y x')
      (_≡_ {Σ \x  Y x} (x , y) (x' , y'))  Σ \(p : x  x')  transport p y  y'
undo-Σ-≡  x x' y y' = undo'-Σ-≡ ((x , y)) (x' , y')

Σ-≡ : {X : Type} {Y : X  Type} (x x' : X) (y : Y x) (y' : Y x')
      (p : x  x')  transport p y  y'  _≡_ {Σ \x  Y x} (x , y) (x' , y') 
Σ-≡ .x' x' .y y refl refl = refl

_•_ : {X : Type}  {x y z : X}   x  y    y  z    x  z
refl  p = p

_⁻¹ : {X : Type}  {x y : X}  x  y  y  x
_⁻¹ refl = refl

sym-is-inverse : {X : Type} {x y : X} (p : x  y)  refl  p ⁻¹  p
sym-is-inverse refl = refl

refl-is-right-id : {X : Set} {x y : X} (p : x  y)  p  p  refl
refl-is-right-id refl = refl

hprop : Type  Type
hprop X = (x y : X)  x  y

hset : Type  Type
hset X = (x y : X)  hprop(x  y)

contractible : Type  Type
contractible X = Σ \(x : X)  (y : X)  x  y

paths-from : {X : Set} (x : X)  Set
paths-from {X} x = Σ \(y : X)  x  y

end-point : {X : Type} {x : X}  paths-from x  X
end-point = π₀ 

trivial-loop : {X : Set} (x : X)  paths-from x
trivial-loop x = (x , refl)

path-from-trivial-loop : {X : Type} {x x' : X} (r : x  x')  trivial-loop x  (x' , r)
path-from-trivial-loop {X} = J {X} A  x  refl)
 where 
  A : (x x' : X)  x  x'  Type
  A x x' r = _≡_ {Σ \(x' : X)  x  x'} (trivial-loop x) (x' , r) 

paths-from-is-contractible : {X : Type} (x₀ : X)  contractible(paths-from x₀)
paths-from-is-contractible x₀ = trivial-loop x₀ ,  t  path-from-trivial-loop (π₁ t))

contractible-is-hprop : {X : Type}  contractible X  hprop X
contractible-is-hprop (x , f) y z = (f y)⁻¹  f z

paths-from-is-hprop : {X : Set} (x : X)  hprop(paths-from x)
paths-from-is-hprop x = contractible-is-hprop (paths-from-is-contractible x)

constant : {X Y : Type}  (X  Y)  Type
constant {X} {Y} f = (x y : X)  f x  f y

collapsible : Type  Type
collapsible X = Σ \(f : X  X)  constant f

path-collapsible : Type  Type
path-collapsible X = {x y : X}  collapsible(x  y)

path-collapsible-is-hset : {X : Type}  path-collapsible X  hset X
path-collapsible-is-hset {X} pc _ _ p q = claim₂
 where
  f : {x y : X}  x  y  x  y
  f = π₀ pc
  g : {x y : X} (p q : x  y)  f p  f q
  g = π₁ pc
  claim₀ : {x y : X} (r : x  y)  r  (f refl)⁻¹  f r
  claim₀ = J'  r  r  (f refl)⁻¹  f r) (sym-is-inverse(f refl))
  claim₁ : (f refl)⁻¹  f p  (f refl)⁻¹  f q
  claim₁ = ap  h  (f refl)⁻¹  h) (g p q)
  claim₂ : p  q
  claim₂ = claim₀ p  claim₁  (claim₀ q)⁻¹

hprop-is-path-collapsible : {X : Type}  hprop X  path-collapsible X
hprop-is-path-collapsible h {x} {y} = ((λ p  h x y) ,  p q  refl))

hprop-is-hset : {X : Type}  hprop X  hset X
hprop-is-hset h = path-collapsible-is-hset(hprop-is-path-collapsible h)

paths-from-is-hset : {X : Set} (x : X)  hset(paths-from x)
paths-from-is-hset x = hprop-is-hset (paths-from-is-hprop x)

data  : Type where
 -- no cases

∅-rec : {X : Type}    X
∅-rec ()

empty : Type  Type
empty X = X  

decidable : Type  Type
decidable X = X + empty X

inhabited-is-collapsible : {X : Type}  X  collapsible X
inhabited-is-collapsible x = ((λ y  x) , λ y y'  refl)

empty-is-collapsible : {X : Type}  empty X  collapsible X
empty-is-collapsible u = ((λ x  x) ,  x x'  ∅-rec(u x)))

decidable-is-collapsible : {X : Type}  decidable X  collapsible X
decidable-is-collapsible (in₀ x) = inhabited-is-collapsible x
decidable-is-collapsible (in₁ u) = empty-is-collapsible u

discrete : Type  Type
discrete X = {x y : X}  decidable(x  y)

discrete-is-path-collapsible : {X : Type}  discrete X  path-collapsible X
discrete-is-path-collapsible d = decidable-is-collapsible d

discrete-is-hset : {X : Type}  discrete X  hset X
discrete-is-hset d = path-collapsible-is-hset(discrete-is-path-collapsible d)

₂-discrete : discrete 
₂-discrete {} {} = in₀ refl
₂-discrete {} {} = in₁  ())
₂-discrete {} {} = in₁  ())
₂-discrete {} {} = in₀ refl

₂-hset : hset 
₂-hset = discrete-is-hset ₂-discrete

infixr 2 _≡_
infixr 1 _+_
infixr 1 _,_
infixl 3 _∘_ 
infixl 3 _•_ 

\end{code}