{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}

module HoTT where

open import Universes public

variable
 ๐“ค ๐“ฅ ๐“ฆ ๐“ฃ : Universe

data ๐Ÿ™ : ๐“คโ‚€ ฬ‡  where
 โ‹† : ๐Ÿ™

๐Ÿ™-induction : (A : ๐Ÿ™ โ†’ ๐“คโ€Šฬ‡ ) โ†’ A โ‹† โ†’ (x : ๐Ÿ™) โ†’ A x
๐Ÿ™-induction A a โ‹† = a

๐Ÿ™-recursion : (B : ๐“คโ€Šฬ‡ ) โ†’ B โ†’ (๐Ÿ™ โ†’ B)
๐Ÿ™-recursion B b x = ๐Ÿ™-induction (ฮป _ โ†’ B) b x

!๐Ÿ™' : (X : ๐“คโ€Šฬ‡ ) โ†’ X โ†’ ๐Ÿ™
!๐Ÿ™' X x = โ‹†

!๐Ÿ™ : {X : ๐“คโ€Šฬ‡ } โ†’ X โ†’ ๐Ÿ™
!๐Ÿ™ x = โ‹†

data ๐Ÿ˜ : ๐“คโ‚€โ€Šฬ‡  where

๐Ÿ˜-induction : (A : ๐Ÿ˜ โ†’ ๐“ค ฬ‡ ) โ†’ (x : ๐Ÿ˜) โ†’ A x
๐Ÿ˜-induction A ()

๐Ÿ˜-recursion : (A : ๐“ค ฬ‡ ) โ†’ ๐Ÿ˜ โ†’ A
๐Ÿ˜-recursion A a = ๐Ÿ˜-induction (ฮป _ โ†’ A) a

!๐Ÿ˜ : (A : ๐“ค ฬ‡ ) โ†’ ๐Ÿ˜ โ†’ A
!๐Ÿ˜ = ๐Ÿ˜-recursion

is-empty : ๐“ค ฬ‡ โ†’ ๐“ค ฬ‡
is-empty X = X โ†’ ๐Ÿ˜

ยฌ : ๐“ค ฬ‡ โ†’ ๐“ค ฬ‡
ยฌ X = X โ†’ ๐Ÿ˜

data โ„• : ๐“คโ‚€ ฬ‡  where
 zero : โ„•
 succ : โ„• โ†’ โ„•

{-# BUILTIN NATURAL โ„• #-}

โ„•-induction : (A : โ„• โ†’ ๐“ค ฬ‡ )
            โ†’ A 0
            โ†’ ((n : โ„•) โ†’ A n โ†’ A (succ n))
            โ†’ (n : โ„•) โ†’ A n

โ„•-induction A aโ‚€ f = h
 where
  h : (n : โ„•) โ†’ A n
  h 0        = aโ‚€
  h (succ n) = f n (h n)

โ„•-recursion : (X : ๐“ค ฬ‡ )
            โ†’ X
            โ†’ (โ„• โ†’ X โ†’ X)
            โ†’ โ„• โ†’ X

โ„•-recursion X = โ„•-induction (ฮป _ โ†’ X)

โ„•-iteration : (X : ๐“ค ฬ‡ )
            โ†’ X
            โ†’ (X โ†’ X)
            โ†’ โ„• โ†’ X

โ„•-iteration X x f = โ„•-recursion X x (ฮป _ x โ†’ f x)

module Arithmetic where

  _+_  _ร—_ : โ„• โ†’ โ„• โ†’ โ„•

  x + 0      = x
  x + succ y = succ (x + y)

  x ร— 0      = 0
  x ร— succ y = x + x ร— y

  infixl 20 _+_
  infixl 21 _ร—_

module Arithmetic' where

  _+_  _ร—_ : โ„• โ†’ โ„• โ†’ โ„•

  x + y = h y
   where
    h : โ„• โ†’ โ„•
    h = โ„•-iteration โ„• x succ

  x ร— y = h y
   where
    h : โ„• โ†’ โ„•
    h = โ„•-iteration โ„• 0 (x +_)

  infixl 20 _+_
  infixl 21 _ร—_

module โ„•-order where

  _โ‰ค_ _โ‰ฅ_ : โ„• โ†’ โ„• โ†’ ๐“คโ‚€ ฬ‡
  0      โ‰ค y      = ๐Ÿ™
  succ x โ‰ค 0      = ๐Ÿ˜
  succ x โ‰ค succ y = x โ‰ค y

  x โ‰ฅ y = y โ‰ค x

  infix 10 _โ‰ค_
  infix 10 _โ‰ฅ_

data _+_ {๐“ค ๐“ฅ} (X : ๐“ค ฬ‡ ) (Y : ๐“ฅ ฬ‡ ) : ๐“ค โŠ” ๐“ฅ ฬ‡  where
 inl : X โ†’ X + Y
 inr : Y โ†’ X + Y

+-induction : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (A : X + Y โ†’ ๐“ฆ ฬ‡ )
            โ†’ ((x : X) โ†’ A (inl x))
            โ†’ ((y : Y) โ†’ A (inr y))
            โ†’ (z : X + Y) โ†’ A z

+-induction A f g (inl x) = f x
+-induction A f g (inr y) = g y

+-recursion : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {A : ๐“ฆ ฬ‡ } โ†’ (X โ†’ A) โ†’ (Y โ†’ A) โ†’ X + Y โ†’ A
+-recursion {๐“ค} {๐“ฅ} {๐“ฆ} {X} {Y} {A} = +-induction (ฮป _ โ†’ A)

๐Ÿš : ๐“คโ‚€ ฬ‡
๐Ÿš = ๐Ÿ™ + ๐Ÿ™

pattern โ‚€ = inl โ‹†
pattern โ‚ = inr โ‹†

๐Ÿš-induction : (A : ๐Ÿš โ†’ ๐“ค ฬ‡ ) โ†’ A โ‚€ โ†’ A โ‚ โ†’ (n : ๐Ÿš) โ†’ A n
๐Ÿš-induction A aโ‚€ aโ‚ โ‚€ = aโ‚€
๐Ÿš-induction A aโ‚€ aโ‚ โ‚ = aโ‚

๐Ÿš-induction' : (A : ๐Ÿš โ†’ ๐“ค ฬ‡ ) โ†’ A โ‚€ โ†’ A โ‚ โ†’ (n : ๐Ÿš) โ†’ A n
๐Ÿš-induction' A aโ‚€ aโ‚ = +-induction A
                         (๐Ÿ™-induction (ฮป (x : ๐Ÿ™) โ†’ A (inl x)) aโ‚€)
                         (๐Ÿ™-induction (ฮป (y : ๐Ÿ™) โ†’ A (inr y)) aโ‚)

record ฮฃ {๐“ค ๐“ฅ} {X : ๐“ค ฬ‡ } (Y : X โ†’ ๐“ฅ ฬ‡ ) : ๐“ค โŠ” ๐“ฅ ฬ‡  where
  constructor
   _,_
  field
   x : X
   y : Y x

prโ‚ : {X : ๐“ค ฬ‡ } {Y : X โ†’ ๐“ฅ ฬ‡ } โ†’ ฮฃ Y โ†’ X
prโ‚ (x , y) = x

prโ‚‚ : {X : ๐“ค ฬ‡ } {Y : X โ†’ ๐“ฅ ฬ‡ } โ†’ (z : ฮฃ Y) โ†’ Y (prโ‚ z)
prโ‚‚ (x , y) = y

-ฮฃ : {๐“ค ๐“ฅ : Universe} (X : ๐“ค ฬ‡ ) (Y : X โ†’ ๐“ฅ ฬ‡ ) โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
-ฮฃ X Y = ฮฃ Y

syntax -ฮฃ X (ฮป x โ†’ y) = ฮฃ x ๊ž‰ X , y

ฮฃ-induction : {X : ๐“ค ฬ‡ } {Y : X โ†’ ๐“ฅ ฬ‡ } {A : ฮฃ Y โ†’ ๐“ฆ ฬ‡ }
            โ†’ ((x : X) (y : Y x) โ†’ A (x , y))
            โ†’ ((x , y) : ฮฃ Y) โ†’ A (x , y)

ฮฃ-induction g (x , y) = g x y

curry : {X : ๐“ค ฬ‡ } {Y : X โ†’ ๐“ฅ ฬ‡ } {A : ฮฃ Y โ†’ ๐“ฆ ฬ‡ }
      โ†’ (((x , y) : ฮฃ Y) โ†’ A (x , y))
      โ†’ ((x : X) (y : Y x) โ†’ A (x , y))

curry f x y = f (x , y)

_ร—_ : ๐“ค ฬ‡ โ†’ ๐“ฅ ฬ‡ โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
X ร— Y = ฮฃ x ๊ž‰ X , Y

ฮ  : {X : ๐“ค ฬ‡ } (A : X โ†’ ๐“ฅ ฬ‡ ) โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
ฮ  {๐“ค} {๐“ฅ} {X} A = (x : X) โ†’ A x

-ฮ  : {๐“ค ๐“ฅ : Universe} (X : ๐“ค ฬ‡ ) (Y : X โ†’ ๐“ฅ ฬ‡ ) โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
-ฮ  X Y = ฮ  Y

syntax -ฮ  A (ฮป x โ†’ b) = ฮ  x ๊ž‰ A , b

id : {X : ๐“ค ฬ‡ } โ†’ X โ†’ X
id x = x

๐‘–๐‘‘ : (X : ๐“ค ฬ‡ ) โ†’ X โ†’ X
๐‘–๐‘‘ X = id

_โˆ˜_ : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {Z : Y โ†’ ๐“ฆ ฬ‡ }
    โ†’ ((y : Y) โ†’ Z y)
    โ†’ (f : X โ†’ Y)
    โ†’ (x : X) โ†’ Z (f x)

g โˆ˜ f = ฮป x โ†’ g (f x)

domain : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ (X โ†’ Y) โ†’ ๐“ค ฬ‡
domain {๐“ค} {๐“ฅ} {X} {Y} f = X

codomain : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ (X โ†’ Y) โ†’ ๐“ฅ ฬ‡
codomain {๐“ค} {๐“ฅ} {X} {Y} f = Y

type-of : {X : ๐“ค ฬ‡ } โ†’ X โ†’ ๐“ค ฬ‡
type-of {๐“ค} {X} x = X

data Id {๐“ค} (X : ๐“ค ฬ‡ ) : X โ†’ X โ†’ ๐“ค ฬ‡  where
 refl : (x : X) โ†’ Id X x x

_โ‰ก_ : {X : ๐“ค ฬ‡ } โ†’ X โ†’ X โ†’ ๐“ค ฬ‡
x โ‰ก y = Id _ x y

๐• : (X : ๐“ค ฬ‡ ) (A : (x y : X) โ†’ x โ‰ก y โ†’ ๐“ฅ ฬ‡ )
  โ†’ ((x : X) โ†’ A x x (refl x))
  โ†’ (x y : X) (p : x โ‰ก y) โ†’ A x y p

๐• X A f x x (refl x) = f x

โ„ : {X : ๐“ค ฬ‡ } (x : X) (B : (y : X) โ†’ x โ‰ก y โ†’ ๐“ฅ ฬ‡ )
  โ†’ B x (refl x)
  โ†’ (y : X) (p : x โ‰ก y) โ†’ B y p

โ„ x B b x (refl x) = b

๐•' : (X : ๐“ค ฬ‡ ) (A : (x y : X) โ†’ x โ‰ก y โ†’ ๐“ฅ ฬ‡ )
   โ†’ ((x : X) โ†’ A x x (refl x))
   โ†’ (x y : X) (p : x โ‰ก y) โ†’ A x y p

๐•' X A f x = โ„ x (A x) (f x)

๐•s-agreement : (X : ๐“ค ฬ‡ ) (A : (x y : X) โ†’ x โ‰ก y โ†’ ๐“ฅ ฬ‡ )
               (f : (x : X) โ†’ A x x (refl x)) (x y : X) (p : x โ‰ก y)
             โ†’ ๐• X A f x y p โ‰ก ๐•' X A f x y p

๐•s-agreement X A f x x (refl x) = refl (f x)

transport : {X : ๐“ค ฬ‡ } (A : X โ†’ ๐“ฅ ฬ‡ ) {x y : X}
          โ†’ x โ‰ก y โ†’ A x โ†’ A y

transport A (refl x) = ๐‘–๐‘‘ (A x)

transport๐• : {X : ๐“ค ฬ‡ } (A : X โ†’ ๐“ฅ ฬ‡ ) {x y : X}
           โ†’ x โ‰ก y โ†’ A x โ†’ A y

transport๐• {๐“ค} {๐“ฅ} {X} A {x} {y} = ๐• X (ฮป x y _ โ†’ A x โ†’ A y) (ฮป x โ†’ ๐‘–๐‘‘ (A x)) x y

nondep-โ„ : {X : ๐“ค ฬ‡ } (x : X) (A : X โ†’ ๐“ฅ ฬ‡ )
         โ†’ A x โ†’ (y : X) โ†’ x โ‰ก y โ†’ A y
nondep-โ„ x A = โ„ x (ฮป y _ โ†’ A y)

transportโ„ : {X : ๐“ค ฬ‡ } (A : X โ†’ ๐“ฅ ฬ‡ ) {x y : X}
           โ†’ x โ‰ก y โ†’ A x โ†’ A y
transportโ„ A {x} {y} p a = nondep-โ„ x A a y p

transports-agreement : {X : ๐“ค ฬ‡ } (A : X โ†’ ๐“ฅ ฬ‡ ) {x y : X} (p : x โ‰ก y)
                     โ†’ (transportโ„ A p โ‰ก transport A p)
                     ร— (transport๐• A p โ‰ก transport A p)

transports-agreement A (refl x) = refl (transport A (refl x)) ,
                                  refl (transport A (refl x))

lhs : {X : ๐“ค ฬ‡ } {x y : X} โ†’ x โ‰ก y โ†’ X
lhs {๐“ค} {X} {x} {y} p = x

rhs : {X : ๐“ค ฬ‡ } {x y : X} โ†’ x โ‰ก y โ†’ X
rhs {๐“ค} {X} {x} {y} p = y

_โˆ™_ : {X : ๐“ค ฬ‡ } {x y z : X} โ†’ x โ‰ก y โ†’ y โ‰ก z โ†’ x โ‰ก z
p โˆ™ q = transport (lhs p โ‰ก_) q p

_โ‰กโŸจ_โŸฉ_ : {X : ๐“ค ฬ‡ } (x : X) {y z : X} โ†’ x โ‰ก y โ†’ y โ‰ก z โ†’ x โ‰ก z
x โ‰กโŸจ p โŸฉ q = p โˆ™ q

_โˆŽ : {X : ๐“ค ฬ‡ } (x : X) โ†’ x โ‰ก x
x โˆŽ = refl x

_โปยน : {X : ๐“ค ฬ‡ } โ†’ {x y : X} โ†’ x โ‰ก y โ†’ y โ‰ก x
p โปยน = transport (_โ‰ก lhs p) p (refl (lhs p))

_โˆ™'_ : {X : ๐“ค ฬ‡ } {x y z : X} โ†’ x โ‰ก y โ†’ y โ‰ก z โ†’ x โ‰ก z
p โˆ™' q = transport (_โ‰ก rhs q) (p โปยน) q

โˆ™agreement : {X : ๐“ค ฬ‡ } {x y z : X} (p : x โ‰ก y) (q : y โ‰ก z)
           โ†’ p โˆ™' q โ‰ก p โˆ™ q

โˆ™agreement (refl x) (refl x) = refl (refl x)

rdnel : {X : ๐“ค ฬ‡ } {x y : X} (p : x โ‰ก y)
      โ†’ p โˆ™ refl y โ‰ก p

rdnel p = refl p

rdner : {X : ๐“ค ฬ‡ } {y z : X} (q : y โ‰ก z)
      โ†’ refl y  โˆ™' q โ‰ก q

rdner q = refl q

ap : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y) {x x' : X} โ†’ x โ‰ก x' โ†’ f x โ‰ก f x'
ap f {x} {x'} p = transport (ฮป - โ†’ f x โ‰ก f -) p (refl (f x))

_โˆผ_ : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ } โ†’ ฮ  A โ†’ ฮ  A โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
f โˆผ g = โˆ€ x โ†’ f x โ‰ก g x

ยฌยฌ ยฌยฌยฌ : ๐“ค ฬ‡ โ†’ ๐“ค ฬ‡
ยฌยฌ  A = ยฌ(ยฌ A)
ยฌยฌยฌ A = ยฌ(ยฌยฌ A)

dni : (A : ๐“ค ฬ‡ ) โ†’ A โ†’ ยฌยฌ A
dni A a u = u a

contrapositive : {A : ๐“ค ฬ‡ } {B : ๐“ฅ ฬ‡ } โ†’ (A โ†’ B) โ†’ (ยฌ B โ†’ ยฌ A)
contrapositive f v a = v (f a)

tno : (A : ๐“ค ฬ‡ ) โ†’ ยฌยฌยฌ A โ†’ ยฌ A
tno A = contrapositive (dni A)

_โ‡”_ : ๐“ค ฬ‡ โ†’ ๐“ฅ ฬ‡ โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
X โ‡” Y = (X โ†’ Y) ร— (Y โ†’ X)

lr-implication : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ (X โ‡” Y) โ†’ (X โ†’ Y)
lr-implication = prโ‚

rl-implication : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ (X โ‡” Y) โ†’ (Y โ†’ X)
rl-implication = prโ‚‚

absurdityยณ-is-absurdity : {A : ๐“ค ฬ‡ } โ†’ ยฌยฌยฌ A โ‡” ยฌ A
absurdityยณ-is-absurdity {๐“ค} {A} = firstly , secondly
 where
  firstly : ยฌยฌยฌ A โ†’ ยฌ A
  firstly = contrapositive (dni A)

  secondly : ยฌ A โ†’ ยฌยฌยฌ A
  secondly = dni (ยฌ A)

_โ‰ข_ : {X : ๐“ค ฬ‡ } โ†’ X โ†’ X โ†’ ๐“ค ฬ‡
x โ‰ข y = ยฌ(x โ‰ก y)

โ‰ข-sym : {X : ๐“ค ฬ‡ } {x y : X} โ†’ x โ‰ข y โ†’ y โ‰ข x
โ‰ข-sym {๐“ค} {X} {x} {y} u = ฮป (p : y โ‰ก x) โ†’ u (p โปยน)

Idโ†’Fun : {X Y : ๐“ค ฬ‡ } โ†’ X โ‰ก Y โ†’ X โ†’ Y
Idโ†’Fun {๐“ค} = transport (๐‘–๐‘‘ (๐“ค ฬ‡ ))

Idโ†’Fun' : {X Y : ๐“ค ฬ‡ } โ†’ X โ‰ก Y โ†’ X โ†’ Y
Idโ†’Fun' (refl X) = ๐‘–๐‘‘ X

Idโ†’Funs-agree : {X Y : ๐“ค ฬ‡ } (p : X โ‰ก Y)
              โ†’ Idโ†’Fun p โ‰ก Idโ†’Fun' p

Idโ†’Funs-agree (refl X) = refl (๐‘–๐‘‘ X)

๐Ÿ™-is-not-๐Ÿ˜ : ๐Ÿ™ โ‰ข ๐Ÿ˜
๐Ÿ™-is-not-๐Ÿ˜ p = Idโ†’Fun p โ‹†

โ‚-is-not-โ‚€ : โ‚ โ‰ข โ‚€
โ‚-is-not-โ‚€ p = ๐Ÿ™-is-not-๐Ÿ˜ q
 where
  f : ๐Ÿš โ†’ ๐“คโ‚€ ฬ‡
  f โ‚€ = ๐Ÿ˜
  f โ‚ = ๐Ÿ™

  q : ๐Ÿ™ โ‰ก ๐Ÿ˜
  q = ap f p

โ‚-is-not-โ‚€[not-an-MLTT-proof] : ยฌ(โ‚ โ‰ก โ‚€)
โ‚-is-not-โ‚€[not-an-MLTT-proof] ()

decidable : ๐“ค ฬ‡ โ†’ ๐“ค ฬ‡
decidable A = A + ยฌ A

has-decidable-equality : ๐“ค ฬ‡ โ†’ ๐“ค ฬ‡
has-decidable-equality X = (x y : X) โ†’ decidable (x โ‰ก y)

๐Ÿš-has-decidable-equality : has-decidable-equality ๐Ÿš
๐Ÿš-has-decidable-equality โ‚€ โ‚€ = inl (refl โ‚€)
๐Ÿš-has-decidable-equality โ‚€ โ‚ = inr (โ‰ข-sym โ‚-is-not-โ‚€)
๐Ÿš-has-decidable-equality โ‚ โ‚€ = inr โ‚-is-not-โ‚€
๐Ÿš-has-decidable-equality โ‚ โ‚ = inl (refl โ‚)

not-zero-is-one : (n : ๐Ÿš) โ†’ n โ‰ข โ‚€ โ†’ n โ‰ก โ‚
not-zero-is-one โ‚€ f = !๐Ÿ˜ (โ‚€ โ‰ก โ‚) (f (refl โ‚€))
not-zero-is-one โ‚ f = refl โ‚

inl-inr-disjoint-images : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {x : X} {y : Y} โ†’ inl x โ‰ข inr y
inl-inr-disjoint-images {๐“ค} {๐“ฅ} {X} {Y} p = ๐Ÿ™-is-not-๐Ÿ˜ q
 where
  f : X + Y โ†’ ๐“คโ‚€ ฬ‡
  f (inl x) = ๐Ÿ™
  f (inr y) = ๐Ÿ˜

  q : ๐Ÿ™ โ‰ก ๐Ÿ˜
  q = ap f p

right-fails-gives-left-holds : {P : ๐“ค ฬ‡ } {Q : ๐“ฅ ฬ‡ } โ†’ P + Q โ†’ ยฌ Q โ†’ P
right-fails-gives-left-holds (inl p) u = p
right-fails-gives-left-holds (inr q) u = !๐Ÿ˜ _ (u q)

module twin-primes where

 open Arithmetic renaming (_ร—_ to _*_ ; _+_ to _โˆ”_)
 open โ„•-order

 is-prime : โ„• โ†’ ๐“คโ‚€ ฬ‡
 is-prime n = (n โ‰ฅ 2) ร— ((x y : โ„•) โ†’ x * y โ‰ก n โ†’ (x โ‰ก 1) + (x โ‰ก n))

 twin-prime-conjecture : ๐“คโ‚€ ฬ‡
 twin-prime-conjecture = (n : โ„•) โ†’ ฮฃ p ๊ž‰ โ„• , (p โ‰ฅ n)
                                           ร— is-prime p
                                           ร— is-prime (p โˆ” 2)

positive-not-zero : (x : โ„•) โ†’ succ x โ‰ข 0
positive-not-zero x p = ๐Ÿ™-is-not-๐Ÿ˜ (g p)
 where
  f : โ„• โ†’ ๐“คโ‚€ ฬ‡
  f 0        = ๐Ÿ˜
  f (succ x) = ๐Ÿ™

  g : succ x โ‰ก 0 โ†’ ๐Ÿ™ โ‰ก ๐Ÿ˜
  g = ap f

pred : โ„• โ†’ โ„•
pred 0        = 0
pred (succ n) = n

succ-lc : {x y : โ„•} โ†’ succ x โ‰ก succ y โ†’ x โ‰ก y
succ-lc = ap pred

โ„•-has-decidable-equality : has-decidable-equality โ„•
โ„•-has-decidable-equality 0 0               = inl (refl 0)
โ„•-has-decidable-equality 0 (succ y)        = inr (โ‰ข-sym (positive-not-zero y))
โ„•-has-decidable-equality (succ x) 0        = inr (positive-not-zero x)
โ„•-has-decidable-equality (succ x) (succ y) = f (โ„•-has-decidable-equality x y)
 where
  f : decidable (x โ‰ก y) โ†’ decidable (succ x โ‰ก succ y)
  f (inl p) = inl (ap succ p)
  f (inr k) = inr (ฮป (s : succ x โ‰ก succ y) โ†’ k (succ-lc s))

module basic-arithmetic-and-order where

  open โ„•-order public
  open Arithmetic renaming (_+_ to _โˆ”_) hiding (_ร—_)

  +-assoc : (x y z : โ„•) โ†’ (x โˆ” y) โˆ” z โ‰ก x โˆ” (y โˆ” z)

  +-assoc x y 0        = (x โˆ” y) โˆ” 0 โ‰กโŸจ refl _ โŸฉ
                         x โˆ” (y โˆ” 0) โˆŽ

  +-assoc x y (succ z) = (x โˆ” y) โˆ” succ z   โ‰กโŸจ refl _     โŸฉ
                         succ ((x โˆ” y) โˆ” z) โ‰กโŸจ ap succ IH โŸฉ
                         succ (x โˆ” (y โˆ” z)) โ‰กโŸจ refl _     โŸฉ
                         x โˆ” (y โˆ” succ z)   โˆŽ
   where
    IH : (x โˆ” y) โˆ” z โ‰ก x โˆ” (y โˆ” z)
    IH = +-assoc x y z

  +-assoc' : (x y z : โ„•) โ†’ (x โˆ” y) โˆ” z โ‰ก x โˆ” (y โˆ” z)
  +-assoc' x y zero     = refl _
  +-assoc' x y (succ z) = ap succ (+-assoc' x y z)

  +-base-on-first : (x : โ„•) โ†’ 0 โˆ” x โ‰ก x

  +-base-on-first 0        = refl 0

  +-base-on-first (succ x) = 0 โˆ” succ x   โ‰กโŸจ refl _     โŸฉ
                             succ (0 โˆ” x) โ‰กโŸจ ap succ IH โŸฉ
                             succ x       โˆŽ
   where
    IH : 0 โˆ” x โ‰ก x
    IH = +-base-on-first x

  +-step-on-first : (x y : โ„•) โ†’ succ x โˆ” y โ‰ก succ (x โˆ” y)

  +-step-on-first x zero     = refl (succ x)

  +-step-on-first x (succ y) = succ x โˆ” succ y   โ‰กโŸจ refl _     โŸฉ
                               succ (succ x โˆ” y) โ‰กโŸจ ap succ IH โŸฉ
                               succ (x โˆ” succ y) โˆŽ
   where
    IH : succ x โˆ” y โ‰ก succ (x โˆ” y)
    IH = +-step-on-first x y

  +-comm : (x y : โ„•) โ†’ x โˆ” y โ‰ก y โˆ” x

  +-comm 0 y = 0 โˆ” y โ‰กโŸจ +-base-on-first y โŸฉ
               y     โ‰กโŸจ refl _ โŸฉ
               y โˆ” 0 โˆŽ

  +-comm (succ x) y = succ x โˆ” y  โ‰กโŸจ +-step-on-first x y โŸฉ
                      succ(x โˆ” y) โ‰กโŸจ ap succ IH          โŸฉ
                      succ(y โˆ” x) โ‰กโŸจ refl _              โŸฉ
                      y โˆ” succ x  โˆŽ
    where
     IH : x โˆ” y โ‰ก y โˆ” x
     IH = +-comm x y

  +-lc : (x y z : โ„•) โ†’ x โˆ” y โ‰ก x โˆ” z โ†’ y โ‰ก z

  +-lc 0        y z p = y     โ‰กโŸจ (+-base-on-first y)โปยน โŸฉ
                        0 โˆ” y โ‰กโŸจ p                     โŸฉ
                        0 โˆ” z โ‰กโŸจ +-base-on-first z     โŸฉ
                        z     โˆŽ

  +-lc (succ x) y z p = IH
   where
    q = succ (x โˆ” y) โ‰กโŸจ (+-step-on-first x y)โปยน โŸฉ
        succ x โˆ” y   โ‰กโŸจ p                       โŸฉ
        succ x โˆ” z   โ‰กโŸจ +-step-on-first x z     โŸฉ
        succ (x โˆ” z) โˆŽ

    IH : y โ‰ก z
    IH = +-lc x y z (succ-lc q)

  _โ‰ผ_ : โ„• โ†’ โ„• โ†’ ๐“คโ‚€ ฬ‡
  x โ‰ผ y = ฮฃ z ๊ž‰ โ„• , x โˆ” z โ‰ก y

  โ‰ค-gives-โ‰ผ : (x y : โ„•) โ†’ x โ‰ค y โ†’ x โ‰ผ y
  โ‰ค-gives-โ‰ผ 0 0               l = 0 , refl 0
  โ‰ค-gives-โ‰ผ 0 (succ y)        l = succ y , +-base-on-first (succ y)
  โ‰ค-gives-โ‰ผ (succ x) 0        l = !๐Ÿ˜ (succ x โ‰ผ zero) l
  โ‰ค-gives-โ‰ผ (succ x) (succ y) l = ฮณ
   where
    IH : x โ‰ผ y
    IH = โ‰ค-gives-โ‰ผ x y l

    z : โ„•
    z = prโ‚ IH

    p : x โˆ” z โ‰ก y
    p = prโ‚‚ IH

    ฮณ : succ x โ‰ผ succ y
    ฮณ = z , (succ x โˆ” z   โ‰กโŸจ +-step-on-first x z โŸฉ
             succ (x โˆ” z) โ‰กโŸจ ap succ p           โŸฉ
             succ y       โˆŽ)

  โ‰ผ-gives-โ‰ค : (x y : โ„•) โ†’ x โ‰ผ y โ†’ x โ‰ค y

  โ‰ผ-gives-โ‰ค 0 0               (z , p) = โ‹†

  โ‰ผ-gives-โ‰ค 0 (succ y)        (z , p) = โ‹†

  โ‰ผ-gives-โ‰ค (succ x) 0        (z , p) = positive-not-zero (x โˆ” z) q
   where
    q = succ (x โˆ” z) โ‰กโŸจ (+-step-on-first x z)โปยน โŸฉ
        succ x โˆ” z   โ‰กโŸจ p                       โŸฉ
        zero         โˆŽ

  โ‰ผ-gives-โ‰ค (succ x) (succ y) (z , p) = IH
   where
    q = succ (x โˆ” z) โ‰กโŸจ (+-step-on-first x z)โปยน โŸฉ
        succ x โˆ” z   โ‰กโŸจ p                       โŸฉ
        succ y       โˆŽ

    IH : x โ‰ค y
    IH = โ‰ผ-gives-โ‰ค x y (z , succ-lc q)

  โ‰ค-refl : (n : โ„•) โ†’ n โ‰ค n
  โ‰ค-refl zero     = โ‹†
  โ‰ค-refl (succ n) = โ‰ค-refl n

  โ‰ค-trans : (l m n : โ„•) โ†’ l โ‰ค m โ†’ m โ‰ค n โ†’ l โ‰ค n
  โ‰ค-trans zero     m        n        p q = โ‹†
  โ‰ค-trans (succ l) zero     n        p q = !๐Ÿ˜ (succ l โ‰ค n) p
  โ‰ค-trans (succ l) (succ m) zero     p q = q
  โ‰ค-trans (succ l) (succ m) (succ n) p q = โ‰ค-trans l m n p q

  โ‰ค-anti : (m n : โ„•) โ†’ m โ‰ค n โ†’ n โ‰ค m โ†’ m โ‰ก n
  โ‰ค-anti zero     zero     p q = refl zero
  โ‰ค-anti zero     (succ n) p q = !๐Ÿ˜ (zero โ‰ก succ n) q
  โ‰ค-anti (succ m) zero     p q = !๐Ÿ˜ (succ m โ‰ก zero) p
  โ‰ค-anti (succ m) (succ n) p q = ap succ (โ‰ค-anti m n p q)

  โ‰ค-succ : (n : โ„•) โ†’ n โ‰ค succ n
  โ‰ค-succ zero     = โ‹†
  โ‰ค-succ (succ n) = โ‰ค-succ n

  zero-minimal : (n : โ„•) โ†’ zero โ‰ค n
  zero-minimal n = โ‹†

  unique-minimal : (n : โ„•) โ†’ n โ‰ค zero โ†’ n โ‰ก zero
  unique-minimal zero     p = refl zero
  unique-minimal (succ n) p = !๐Ÿ˜ (succ n โ‰ก zero) p

  โ‰ค-split : (m n : โ„•) โ†’ m โ‰ค succ n โ†’ (m โ‰ค n) + (m โ‰ก succ n)
  โ‰ค-split zero     n        l = inl l
  โ‰ค-split (succ m) zero     l = inr (ap succ (unique-minimal m l))
  โ‰ค-split (succ m) (succ n) l = +-recursion inl (inr โˆ˜ ap succ) (โ‰ค-split m n l)

  _<_ : โ„• โ†’ โ„• โ†’ ๐“คโ‚€ ฬ‡
  x < y = succ x โ‰ค y

  infix 10 _<_

  not-<-gives-โ‰ฅ : (m n : โ„•) โ†’ ยฌ(n < m) โ†’ m โ‰ค n
  not-<-gives-โ‰ฅ zero     n        u = zero-minimal n
  not-<-gives-โ‰ฅ (succ m) zero     u = dni (zero < succ m) (zero-minimal m) u
  not-<-gives-โ‰ฅ (succ m) (succ n) u = not-<-gives-โ‰ฅ m n u

  bounded-โˆ€-next : (A : โ„• โ†’ ๐“ค ฬ‡ ) (k : โ„•)
                 โ†’ A k
                 โ†’ ((n : โ„•) โ†’ n < k โ†’ A n)
                 โ†’ (n : โ„•) โ†’ n < succ k โ†’ A n
  bounded-โˆ€-next A k a ฯ† n l = +-recursion f g s
   where
    s : (n < k) + (succ n โ‰ก succ k)
    s = โ‰ค-split (succ n) k l

    f : n < k โ†’ A n
    f = ฯ† n

    g : succ n โ‰ก succ k โ†’ A n
    g p = transport A ((succ-lc p)โปยน) a

  root : (โ„• โ†’ โ„•) โ†’ ๐“คโ‚€ ฬ‡
  root f = ฮฃ n ๊ž‰ โ„• , f n โ‰ก 0

  _has-no-root<_ : (โ„• โ†’ โ„•) โ†’ โ„• โ†’ ๐“คโ‚€ ฬ‡
  f has-no-root< k = (n : โ„•) โ†’ n < k โ†’ f n โ‰ข 0

  is-minimal-root : (โ„• โ†’ โ„•) โ†’ โ„• โ†’ ๐“คโ‚€ ฬ‡
  is-minimal-root f m = (f m โ‰ก 0) ร— (f has-no-root< m)

  at-most-one-minimal-root : (f : โ„• โ†’ โ„•) (m n : โ„•)
                           โ†’ is-minimal-root f m โ†’ is-minimal-root f n โ†’ m โ‰ก n

  at-most-one-minimal-root f m n (p , ฯ†) (q , ฯˆ) = c m n a b
   where
    a : ยฌ(m < n)
    a u = ฯˆ m u p

    b : ยฌ(n < m)
    b v = ฯ† n v q

    c : (m n : โ„•) โ†’ ยฌ(m < n) โ†’ ยฌ(n < m) โ†’ m โ‰ก n
    c m n u v = โ‰ค-anti m n (not-<-gives-โ‰ฅ m n v) (not-<-gives-โ‰ฅ n m u)

  minimal-root : (โ„• โ†’ โ„•) โ†’ ๐“คโ‚€ ฬ‡
  minimal-root f = ฮฃ m ๊ž‰ โ„• , is-minimal-root f m

  minimal-root-is-root : โˆ€ f โ†’ minimal-root f โ†’ root f
  minimal-root-is-root f (m , p , _) = m , p

  bounded-โ„•-search : โˆ€ k f โ†’ (minimal-root f) + (f has-no-root< k)
  bounded-โ„•-search zero f = inr (ฮป n โ†’ !๐Ÿ˜ (f n โ‰ข 0))
  bounded-โ„•-search (succ k) f = +-recursion ฯ† ฮณ (bounded-โ„•-search k f)
   where
    A : โ„• โ†’ (โ„• โ†’ โ„•) โ†’ ๐“คโ‚€ ฬ‡
    A k f = (minimal-root f) + (f has-no-root< k)

    ฯ† : minimal-root f โ†’ A (succ k) f
    ฯ† = inl

    ฮณ : f has-no-root< k โ†’ A (succ k) f
    ฮณ u = +-recursion ฮณโ‚€ ฮณโ‚ (โ„•-has-decidable-equality (f k) 0)
     where
      ฮณโ‚€ : f k โ‰ก 0 โ†’ A (succ k) f
      ฮณโ‚€ p = inl (k , p , u)

      ฮณโ‚ : f k โ‰ข 0 โ†’ A (succ k) f
      ฮณโ‚ v = inr (bounded-โˆ€-next (ฮป n โ†’ f n โ‰ข 0) k v u)

  root-gives-minimal-root : โˆ€ f โ†’ root f โ†’ minimal-root f
  root-gives-minimal-root f (n , p) = ฮณ
   where
    g : ยฌ(f has-no-root< (succ n))
    g ฯ† = ฯ† n (โ‰ค-refl n) p

    ฮณ : minimal-root f
    ฮณ = right-fails-gives-left-holds (bounded-โ„•-search (succ n) f) g

is-singleton : ๐“ค ฬ‡ โ†’ ๐“ค ฬ‡
is-singleton X = ฮฃ c ๊ž‰ X , ((x : X) โ†’ c โ‰ก x)

is-center : (X : ๐“ค ฬ‡ ) โ†’ X โ†’ ๐“ค ฬ‡
is-center X c = (x : X) โ†’ c โ‰ก x

๐Ÿ™-is-singleton : is-singleton ๐Ÿ™
๐Ÿ™-is-singleton = โ‹† , ๐Ÿ™-induction (ฮป x โ†’ โ‹† โ‰ก x) (refl โ‹†)

center : (X : ๐“ค ฬ‡ ) โ†’ is-singleton X โ†’ X
center X (c , ฯ†) = c

centrality : (X : ๐“ค ฬ‡ ) (i : is-singleton X) (x : X) โ†’ center X i โ‰ก x
centrality X (c , ฯ†) = ฯ†

is-subsingleton : ๐“ค ฬ‡ โ†’ ๐“ค ฬ‡
is-subsingleton X = (x y : X) โ†’ x โ‰ก y

๐Ÿ˜-is-subsingleton : is-subsingleton ๐Ÿ˜
๐Ÿ˜-is-subsingleton x y = !๐Ÿ˜ (x โ‰ก y) x

singletons-are-subsingletons : (X : ๐“ค ฬ‡ ) โ†’ is-singleton X โ†’ is-subsingleton X
singletons-are-subsingletons X (c , ฯ†) x y = x โ‰กโŸจ (ฯ† x)โปยน โŸฉ
                                             c โ‰กโŸจ ฯ† y     โŸฉ
                                             y โˆŽ

๐Ÿ™-is-subsingleton : is-subsingleton ๐Ÿ™
๐Ÿ™-is-subsingleton = singletons-are-subsingletons ๐Ÿ™ ๐Ÿ™-is-singleton

pointed-subsingletons-are-singletons : (X : ๐“ค ฬ‡ )
                                     โ†’ X โ†’ is-subsingleton X โ†’ is-singleton X

pointed-subsingletons-are-singletons X x s = (x , s x)

singleton-iff-pointed-and-subsingleton : {X : ๐“ค ฬ‡ }
                                       โ†’ is-singleton X โ‡” (X ร— is-subsingleton X)

singleton-iff-pointed-and-subsingleton {๐“ค} {X} = (a , b)
 where
  a : is-singleton X โ†’ X ร— is-subsingleton X
  a s = center X s , singletons-are-subsingletons X s

  b : X ร— is-subsingleton X โ†’ is-singleton X
  b (x , t) = pointed-subsingletons-are-singletons X x t

is-prop is-truth-value : ๐“ค ฬ‡ โ†’ ๐“ค ฬ‡
is-prop        = is-subsingleton
is-truth-value = is-subsingleton

is-set : ๐“ค ฬ‡ โ†’ ๐“ค ฬ‡
is-set X = (x y : X) โ†’ is-subsingleton (x โ‰ก y)

EM EM' : โˆ€ ๐“ค โ†’ ๐“ค โบ ฬ‡
EM  ๐“ค = (X : ๐“ค ฬ‡ ) โ†’ is-subsingleton X โ†’ X + ยฌ X
EM' ๐“ค = (X : ๐“ค ฬ‡ ) โ†’ is-subsingleton X โ†’ is-singleton X + is-empty X

EM-gives-EM' : EM ๐“ค โ†’ EM' ๐“ค
EM-gives-EM' em X s = ฮณ (em X s)
 where
  ฮณ : X + ยฌ X โ†’ is-singleton X + is-empty X
  ฮณ (inl x) = inl (pointed-subsingletons-are-singletons X x s)
  ฮณ (inr x) = inr x

EM'-gives-EM : EM' ๐“ค โ†’ EM ๐“ค
EM'-gives-EM em' X s = ฮณ (em' X s)
 where
  ฮณ : is-singleton X + is-empty X โ†’ X + ยฌ X
  ฮณ (inl i) = inl (center X i)
  ฮณ (inr x) = inr x

no-unicorns : ยฌ(ฮฃ X ๊ž‰ ๐“ค ฬ‡ , is-subsingleton X ร— ยฌ(is-singleton X) ร— ยฌ(is-empty X))
no-unicorns (X , i , f , g) = c
 where
  e : is-empty X
  e x = f (pointed-subsingletons-are-singletons X x i)

  c : ๐Ÿ˜
  c = g e

module magmas where

 Magma : (๐“ค : Universe) โ†’ ๐“ค โบ ฬ‡
 Magma ๐“ค = ฮฃ X ๊ž‰ ๐“ค ฬ‡ , is-set X ร— (X โ†’ X โ†’ X)

 โŸจ_โŸฉ : Magma ๐“ค โ†’ ๐“ค ฬ‡
 โŸจ X , i , _ยท_ โŸฉ = X

 magma-is-set : (M : Magma ๐“ค) โ†’ is-set โŸจ M โŸฉ
 magma-is-set (X , i , _ยท_) = i

 magma-operation : (M : Magma ๐“ค) โ†’ โŸจ M โŸฉ โ†’ โŸจ M โŸฉ โ†’ โŸจ M โŸฉ
 magma-operation (X , i , _ยท_) = _ยท_

 syntax magma-operation M x y = x ยทโŸจ M โŸฉ y

 is-magma-hom : (M N : Magma ๐“ค) โ†’ (โŸจ M โŸฉ โ†’ โŸจ N โŸฉ) โ†’ ๐“ค ฬ‡
 is-magma-hom M N f = (x y : โŸจ M โŸฉ) โ†’ f (x ยทโŸจ M โŸฉ y) โ‰ก f x ยทโŸจ N โŸฉ f y

 id-is-magma-hom : (M : Magma ๐“ค) โ†’ is-magma-hom M M (๐‘–๐‘‘ โŸจ M โŸฉ)
 id-is-magma-hom M = ฮป (x y : โŸจ M โŸฉ) โ†’ refl (x ยทโŸจ M โŸฉ y)

 is-magma-iso : (M N : Magma ๐“ค) โ†’ (โŸจ M โŸฉ โ†’ โŸจ N โŸฉ) โ†’ ๐“ค ฬ‡
 is-magma-iso M N f = is-magma-hom M N f
                    ร— (ฮฃ g ๊ž‰ (โŸจ N โŸฉ โ†’ โŸจ M โŸฉ), is-magma-hom N M g
                                            ร— (g โˆ˜ f โˆผ ๐‘–๐‘‘ โŸจ M โŸฉ)
                                            ร— (f โˆ˜ g โˆผ ๐‘–๐‘‘ โŸจ N โŸฉ))

 id-is-magma-iso : (M : Magma ๐“ค) โ†’ is-magma-iso M M (๐‘–๐‘‘ โŸจ M โŸฉ)
 id-is-magma-iso M = id-is-magma-hom M ,
                     ๐‘–๐‘‘ โŸจ M โŸฉ ,
                     id-is-magma-hom M ,
                     refl ,
                     refl

 Idโ†’iso : {M N : Magma ๐“ค} โ†’ M โ‰ก N โ†’ โŸจ M โŸฉ โ†’ โŸจ N โŸฉ
 Idโ†’iso p = transport โŸจ_โŸฉ p

 Idโ†’iso-is-iso : {M N : Magma ๐“ค} (p : M โ‰ก N) โ†’ is-magma-iso M N (Idโ†’iso p)
 Idโ†’iso-is-iso (refl M) = id-is-magma-iso M

 _โ‰…โ‚˜_ : Magma ๐“ค โ†’ Magma ๐“ค โ†’ ๐“ค ฬ‡
 M โ‰…โ‚˜ N = ฮฃ f ๊ž‰ (โŸจ M โŸฉ โ†’ โŸจ N โŸฉ), is-magma-iso M N f

 magma-Idโ†’iso : {M N : Magma ๐“ค} โ†’ M โ‰ก N โ†’ M โ‰…โ‚˜ N
 magma-Idโ†’iso p = (Idโ†’iso p , Idโ†’iso-is-iso p)

 โˆž-Magma : (๐“ค : Universe) โ†’ ๐“ค โบ ฬ‡
 โˆž-Magma ๐“ค = ฮฃ X ๊ž‰ ๐“ค ฬ‡ , (X โ†’ X โ†’ X)

module monoids where

 left-neutral : {X : ๐“ค ฬ‡ } โ†’ X โ†’ (X โ†’ X โ†’ X) โ†’ ๐“ค ฬ‡
 left-neutral e _ยท_ = โˆ€ x โ†’ e ยท x โ‰ก x

 right-neutral : {X : ๐“ค ฬ‡ } โ†’ X โ†’ (X โ†’ X โ†’ X) โ†’ ๐“ค ฬ‡
 right-neutral e _ยท_ = โˆ€ x โ†’ x ยท e โ‰ก x

 associative : {X : ๐“ค ฬ‡ } โ†’ (X โ†’ X โ†’ X) โ†’ ๐“ค ฬ‡
 associative _ยท_ = โˆ€ x y z โ†’ (x ยท y) ยท z โ‰ก x ยท (y ยท z)

 Monoid : (๐“ค : Universe) โ†’ ๐“ค โบ ฬ‡
 Monoid ๐“ค = ฮฃ X ๊ž‰ ๐“ค  ฬ‡ , is-set X
                      ร— (ฮฃ ยท ๊ž‰ (X โ†’ X โ†’ X) , (ฮฃ e ๊ž‰ X , (left-neutral e ยท)
                                                      ร— (right-neutral e ยท)
                                                      ร— (associative ยท)))

refl-left : {X : ๐“ค ฬ‡ } {x y : X} {p : x โ‰ก y} โ†’ refl x โˆ™ p โ‰ก p
refl-left {๐“ค} {X} {x} {x} {refl x} = refl (refl x)

refl-right : {X : ๐“ค ฬ‡ } {x y : X} {p : x โ‰ก y} โ†’ p โˆ™ refl y โ‰ก p
refl-right {๐“ค} {X} {x} {y} {p} = refl p

โˆ™assoc : {X : ๐“ค ฬ‡ } {x y z t : X} (p : x โ‰ก y) (q : y โ‰ก z) (r : z โ‰ก t)
       โ†’ (p โˆ™ q) โˆ™ r โ‰ก p โˆ™ (q โˆ™ r)

โˆ™assoc p q (refl z) = refl (p โˆ™ q)

โปยน-leftโˆ™ : {X : ๐“ค ฬ‡ } {x y : X} (p : x โ‰ก y)
         โ†’ p โปยน โˆ™ p โ‰ก refl y

โปยน-leftโˆ™ (refl x) = refl (refl x)

โปยน-rightโˆ™ : {X : ๐“ค ฬ‡ } {x y : X} (p : x โ‰ก y)
          โ†’ p โˆ™ p โปยน โ‰ก refl x

โปยน-rightโˆ™ (refl x) = refl (refl x)

โปยน-involutive : {X : ๐“ค ฬ‡ } {x y : X} (p : x โ‰ก y)
              โ†’ (p โปยน)โปยน โ‰ก p

โปยน-involutive (refl x) = refl (refl x)

ap-refl : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y) (x : X)
        โ†’ ap f (refl x) โ‰ก refl (f x)

ap-refl f x = refl (refl (f x))

ap-โˆ™ : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y) {x y z : X} (p : x โ‰ก y) (q : y โ‰ก z)
     โ†’ ap f (p โˆ™ q) โ‰ก ap f p โˆ™ ap f q

ap-โˆ™ f p (refl y) = refl (ap f p)

apโปยน : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y) {x y : X} (p : x โ‰ก y)
     โ†’ (ap f p)โปยน โ‰ก ap f (p โปยน)

apโปยน f (refl x) = refl (refl (f x))

ap-id : {X : ๐“ค ฬ‡ } {x y : X} (p : x โ‰ก y)
      โ†’ ap id p โ‰ก p

ap-id (refl x) = refl (refl x)

ap-โˆ˜ : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {Z : ๐“ฆ ฬ‡ }
       (f : X โ†’ Y) (g : Y โ†’ Z) {x y : X} (p : x โ‰ก y)
     โ†’ ap (g โˆ˜ f) p โ‰ก (ap g โˆ˜ ap f) p

ap-โˆ˜ f g (refl x) = refl (refl (g (f x)))

transportโˆ™ : {X : ๐“ค ฬ‡ } (A : X โ†’ ๐“ฅ ฬ‡ ) {x y z : X} (p : x โ‰ก y) (q : y โ‰ก z)
           โ†’ transport A (p โˆ™ q) โ‰ก transport A q โˆ˜ transport A p

transportโˆ™ A p (refl y) = refl (transport A p)

Nat : {X : ๐“ค ฬ‡ } โ†’ (X โ†’ ๐“ฅ ฬ‡ ) โ†’ (X โ†’ ๐“ฆ ฬ‡ ) โ†’ ๐“ค โŠ” ๐“ฅ โŠ” ๐“ฆ ฬ‡
Nat A B = (x : domain A) โ†’ A x โ†’ B x

Nats-are-natural : {X : ๐“ค ฬ‡ } (A : X โ†’ ๐“ฅ ฬ‡ ) (B : X โ†’ ๐“ฆ ฬ‡ ) (ฯ„ : Nat A B)
                 โ†’ {x y : X} (p : x โ‰ก y)
                 โ†’ ฯ„ y โˆ˜ transport A p โ‰ก transport B p โˆ˜ ฯ„ x

Nats-are-natural A B ฯ„ (refl x) = refl (ฯ„ x)

Natฮฃ : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ } {B : X โ†’ ๐“ฆ ฬ‡ } โ†’ Nat A B โ†’ ฮฃ A โ†’ ฮฃ B
Natฮฃ ฯ„ (x , a) = (x , ฯ„ x a)

transport-ap : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (A : Y โ†’ ๐“ฆ ฬ‡ )
               (f : X โ†’ Y) {x x' : X} (p : x โ‰ก x') (a : A (f x))
             โ†’ transport (A โˆ˜ f) p a โ‰ก transport A (ap f p) a

transport-ap A f (refl x) a = refl a

data Color : ๐“คโ‚€ ฬ‡  where
 Black White : Color

apd : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ } (f : (x : X) โ†’ A x) {x y : X}
      (p : x โ‰ก y) โ†’ transport A p (f x) โ‰ก f y

apd f (refl x) = refl (f x)

to-ฮฃ-โ‰ก : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ } {ฯƒ ฯ„ : ฮฃ A}
       โ†’ (ฮฃ p ๊ž‰ prโ‚ ฯƒ โ‰ก prโ‚ ฯ„ , transport A p (prโ‚‚ ฯƒ) โ‰ก prโ‚‚ ฯ„)
       โ†’ ฯƒ โ‰ก ฯ„

to-ฮฃ-โ‰ก (refl x , refl a) = refl (x , a)

from-ฮฃ-โ‰ก : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ } {ฯƒ ฯ„ : ฮฃ A}
         โ†’ ฯƒ โ‰ก ฯ„
         โ†’ ฮฃ p ๊ž‰ prโ‚ ฯƒ โ‰ก prโ‚ ฯ„ , transport A p (prโ‚‚ ฯƒ) โ‰ก prโ‚‚ ฯ„

from-ฮฃ-โ‰ก (refl (x , a)) = (refl x , refl a)

to-ฮฃ-โ‰ก-again : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ } {(x , a) (y , b) : ฮฃ A}
             โ†’ ฮฃ p ๊ž‰ x โ‰ก y , transport A p a โ‰ก b
             โ†’ (x , a) โ‰ก (y , b)

to-ฮฃ-โ‰ก-again (refl x , refl a) = refl (x , a)

from-ฮฃ-โ‰ก-again : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ } {(x , a) (y , b) : ฮฃ A}
               โ†’ (x , a) โ‰ก (y , b)
               โ†’ ฮฃ p ๊ž‰ x โ‰ก y , transport A p a โ‰ก b

from-ฮฃ-โ‰ก-again (refl (x , a)) = (refl x , refl a)

to-ฮฃ-โ‰ก' : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ } {x : X} {a a' : A x}
        โ†’ a โ‰ก a' โ†’ Id (ฮฃ A) (x , a) (x , a')

to-ฮฃ-โ‰ก' {๐“ค} {๐“ฅ} {X} {A} {x} = ap (ฮป - โ†’ (x , -))

transport-ร— : {X : ๐“ค ฬ‡ } (A : X โ†’ ๐“ฅ ฬ‡ ) (B : X โ†’ ๐“ฆ ฬ‡ )
              {x y : X} (p : x โ‰ก y) {(a , b) : A x ร— B x}

            โ†’ transport (ฮป x โ†’ A x ร— B x) p (a , b)
            โ‰ก (transport A p a , transport B p b)

transport-ร— A B (refl _) = refl _

transportd : {X : ๐“ค ฬ‡ } (A : X โ†’ ๐“ฅ ฬ‡ ) (B : (x : X) โ†’ A x โ†’ ๐“ฆ ฬ‡ )
             {x : X} ((a , b) : ฮฃ a ๊ž‰ A x , B x a) {y : X} (p : x โ‰ก y)
           โ†’ B x a โ†’ B y (transport A p a)

transportd A B (a , b) (refl x) = id

transport-ฮฃ : {X : ๐“ค ฬ‡ } (A : X โ†’ ๐“ฅ ฬ‡ ) (B : (x : X) โ†’ A x โ†’ ๐“ฆ ฬ‡ )
              {x : X} {y : X} (p : x โ‰ก y) {(a , b) : ฮฃ a ๊ž‰ A x , B x a}

            โ†’ transport (ฮป - โ†’ ฮฃ (B -)) p (a , b)
            โ‰ก transport A p a , transportd A B (a , b) p b

transport-ฮฃ A B (refl x) {a , b} = refl (a , b)

_is-of-hlevel_ : ๐“ค ฬ‡ โ†’ โ„• โ†’ ๐“ค ฬ‡
X is-of-hlevel 0        = is-singleton X
X is-of-hlevel (succ n) = (x x' : X) โ†’ ((x โ‰ก x') is-of-hlevel n)

wconstant : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ (X โ†’ Y) โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
wconstant f = (x x' : domain f) โ†’ f x โ‰ก f x'

wconstant-endomap : ๐“ค ฬ‡ โ†’ ๐“ค ฬ‡
wconstant-endomap X = ฮฃ f ๊ž‰ (X โ†’ X), wconstant f

wcmap : (X : ๐“ค ฬ‡ ) โ†’ wconstant-endomap X โ†’ (X โ†’ X)
wcmap X (f , w) = f

wcmap-constancy : (X : ๐“ค ฬ‡ ) (c : wconstant-endomap X)
                โ†’ wconstant (wcmap X c)
wcmap-constancy X (f , w) = w

Hedberg : {X : ๐“ค ฬ‡ } (x : X)
        โ†’ ((y : X) โ†’ wconstant-endomap (x โ‰ก y))
        โ†’ (y : X) โ†’ is-subsingleton (x โ‰ก y)

Hedberg {๐“ค} {X} x c y p q =

 p                         โ‰กโŸจ a y p                                     โŸฉ
 (f x (refl x))โปยน โˆ™ f y p  โ‰กโŸจ ap (ฮป - โ†’ (f x (refl x))โปยน โˆ™ -) (ฮบ y p q) โŸฉ
 (f x (refl x))โปยน โˆ™ f y q  โ‰กโŸจ (a y q)โปยน                                 โŸฉ
 q                         โˆŽ

 where
  f : (y : X) โ†’ x โ‰ก y โ†’ x โ‰ก y
  f y = wcmap (x โ‰ก y) (c y)

  ฮบ : (y : X) (p q : x โ‰ก y) โ†’ f y p โ‰ก f y q
  ฮบ y = wcmap-constancy (x โ‰ก y) (c y)

  a : (y : X) (p : x โ‰ก y) โ†’ p โ‰ก (f x (refl x))โปยน โˆ™ f y p
  a x (refl x) = (โปยน-leftโˆ™ (f x (refl x)))โปยน

wconstant-โ‰ก-endomaps : ๐“ค ฬ‡ โ†’ ๐“ค ฬ‡
wconstant-โ‰ก-endomaps X = (x y : X) โ†’ wconstant-endomap (x โ‰ก y)

sets-have-wconstant-โ‰ก-endomaps : (X : ๐“ค ฬ‡ ) โ†’ is-set X โ†’ wconstant-โ‰ก-endomaps X
sets-have-wconstant-โ‰ก-endomaps X s x y = (f , ฮบ)
 where
  f : x โ‰ก y โ†’ x โ‰ก y
  f p = p

  ฮบ : (p q : x โ‰ก y) โ†’ f p โ‰ก f q
  ฮบ p q = s x y p q

types-with-wconstant-โ‰ก-endomaps-are-sets : (X : ๐“ค ฬ‡ )
                                         โ†’ wconstant-โ‰ก-endomaps X โ†’ is-set X

types-with-wconstant-โ‰ก-endomaps-are-sets X c x = Hedberg x
                                                  (ฮป y โ†’ wcmap (x โ‰ก y) (c x y) ,
                                                   wcmap-constancy (x โ‰ก y) (c x y))

subsingletons-have-wconstant-โ‰ก-endomaps : (X : ๐“ค ฬ‡ )
                                        โ†’ is-subsingleton X
                                        โ†’ wconstant-โ‰ก-endomaps X

subsingletons-have-wconstant-โ‰ก-endomaps X s x y = (f , ฮบ)
 where
  f : x โ‰ก y โ†’ x โ‰ก y
  f p = s x y

  ฮบ : (p q : x โ‰ก y) โ†’ f p โ‰ก f q
  ฮบ p q = refl (s x y)

subsingletons-are-sets : (X : ๐“ค ฬ‡ ) โ†’ is-subsingleton X โ†’ is-set X
subsingletons-are-sets X s = types-with-wconstant-โ‰ก-endomaps-are-sets X
                               (subsingletons-have-wconstant-โ‰ก-endomaps X s)

singletons-are-sets : (X : ๐“ค ฬ‡ ) โ†’ is-singleton X โ†’ is-set X
singletons-are-sets X = subsingletons-are-sets X โˆ˜ singletons-are-subsingletons X

๐Ÿ˜-is-set : is-set ๐Ÿ˜
๐Ÿ˜-is-set = subsingletons-are-sets ๐Ÿ˜ ๐Ÿ˜-is-subsingleton

๐Ÿ™-is-set : is-set ๐Ÿ™
๐Ÿ™-is-set = subsingletons-are-sets ๐Ÿ™ ๐Ÿ™-is-subsingleton

subsingletons-are-of-hlevel-1 : (X : ๐“ค ฬ‡ )
                              โ†’ is-subsingleton X
                              โ†’ X is-of-hlevel 1

subsingletons-are-of-hlevel-1 X = g
 where
  g : ((x y : X) โ†’ x โ‰ก y) โ†’ (x y : X) โ†’ is-singleton (x โ‰ก y)
  g t x y = t x y , subsingletons-are-sets X t x y (t x y)

types-of-hlevel-1-are-subsingletons : (X : ๐“ค ฬ‡ )
                                    โ†’ X is-of-hlevel 1
                                    โ†’ is-subsingleton X

types-of-hlevel-1-are-subsingletons X = f
 where
  f : ((x y : X) โ†’ is-singleton (x โ‰ก y)) โ†’ (x y : X) โ†’ x โ‰ก y
  f s x y = center (x โ‰ก y) (s x y)

sets-are-of-hlevel-2 : (X : ๐“ค ฬ‡ ) โ†’ is-set X โ†’ X is-of-hlevel 2
sets-are-of-hlevel-2 X = g
 where
  g : ((x y : X) โ†’ is-subsingleton (x โ‰ก y)) โ†’ (x y : X) โ†’ (x โ‰ก y) is-of-hlevel 1
  g t x y = subsingletons-are-of-hlevel-1 (x โ‰ก y) (t x y)

types-of-hlevel-2-are-sets : (X : ๐“ค ฬ‡ ) โ†’ X is-of-hlevel 2 โ†’ is-set X
types-of-hlevel-2-are-sets X = f
 where
  f : ((x y : X) โ†’ (x โ‰ก y) is-of-hlevel 1) โ†’ (x y : X) โ†’ is-subsingleton (x โ‰ก y)
  f s x y = types-of-hlevel-1-are-subsingletons (x โ‰ก y) (s x y)

hlevel-upper : (X : ๐“ค ฬ‡ ) (n : โ„•) โ†’ X is-of-hlevel n โ†’ X is-of-hlevel (succ n)
hlevel-upper X zero = ฮณ
 where
  ฮณ : is-singleton X โ†’ (x y : X) โ†’ is-singleton (x โ‰ก y)
  ฮณ h x y = p , subsingletons-are-sets X k x y p
   where
    k : is-subsingleton X
    k = singletons-are-subsingletons X h

    p : x โ‰ก y
    p = k x y

hlevel-upper X (succ n) = ฮป h x y โ†’ hlevel-upper (x โ‰ก y) n (h x y)

_has-minimal-hlevel_ : ๐“ค ฬ‡ โ†’ โ„• โ†’ ๐“ค ฬ‡
X has-minimal-hlevel 0        = X is-of-hlevel 0
X has-minimal-hlevel (succ n) = (X is-of-hlevel (succ n)) ร— ยฌ(X is-of-hlevel n)

_has-minimal-hlevel-โˆž : ๐“ค ฬ‡ โ†’ ๐“ค ฬ‡
X has-minimal-hlevel-โˆž = (n : โ„•) โ†’ ยฌ(X is-of-hlevel n)

pointed-types-have-wconstant-endomap : {X : ๐“ค ฬ‡ } โ†’ X โ†’ wconstant-endomap X
pointed-types-have-wconstant-endomap x = ((ฮป y โ†’ x) , (ฮป y y' โ†’ refl x))

empty-types-have-wconstant-endomap : {X : ๐“ค ฬ‡ } โ†’ is-empty X โ†’ wconstant-endomap X
empty-types-have-wconstant-endomap e = (id , (ฮป x x' โ†’ !๐Ÿ˜ (x โ‰ก x') (e x)))

decidable-has-wconstant-endomap : {X : ๐“ค ฬ‡ } โ†’ decidable X โ†’ wconstant-endomap X
decidable-has-wconstant-endomap (inl x) = pointed-types-have-wconstant-endomap x
decidable-has-wconstant-endomap (inr e) = empty-types-have-wconstant-endomap e

hedberg-lemma : {X : ๐“ค ฬ‡ } โ†’ has-decidable-equality X โ†’ wconstant-โ‰ก-endomaps X
hedberg-lemma {๐“ค} {X} d x y = decidable-has-wconstant-endomap (d x y)

hedberg : {X : ๐“ค ฬ‡ } โ†’ has-decidable-equality X โ†’ is-set X
hedberg {๐“ค} {X} d = types-with-wconstant-โ‰ก-endomaps-are-sets X (hedberg-lemma d)

โ„•-is-set : is-set โ„•
โ„•-is-set = hedberg โ„•-has-decidable-equality

๐Ÿš-is-set : is-set ๐Ÿš
๐Ÿš-is-set = hedberg ๐Ÿš-has-decidable-equality

has-section : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ (X โ†’ Y) โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
has-section r = ฮฃ s ๊ž‰ (codomain r โ†’ domain r), r โˆ˜ s โˆผ id

_โ—_ : ๐“ค ฬ‡ โ†’ ๐“ฅ ฬ‡ โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
X โ— Y = ฮฃ r ๊ž‰ (Y โ†’ X), has-section r

retraction : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ X โ— Y โ†’ Y โ†’ X
retraction (r , s , ฮท) = r

section : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ X โ— Y โ†’ X โ†’ Y
section (r , s , ฮท) = s

retract-equation : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (ฯ : X โ— Y)
                 โ†’ retraction ฯ โˆ˜ section ฯ โˆผ ๐‘–๐‘‘ X

retract-equation (r , s , ฮท) = ฮท

retraction-has-section : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (ฯ : X โ— Y)
                       โ†’ has-section (retraction ฯ)

retraction-has-section (r , h) = h

id-โ— : (X : ๐“ค ฬ‡ ) โ†’ X โ— X
id-โ— X = ๐‘–๐‘‘ X , ๐‘–๐‘‘ X , refl

_โ—โˆ˜_ : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {Z : ๐“ฆ ฬ‡ } โ†’ X โ— Y โ†’ Y โ— Z โ†’ X โ— Z

(r , s , ฮท) โ—โˆ˜ (r' , s' , ฮท') = (r โˆ˜ r' , s' โˆ˜ s , ฮท'')
 where
  ฮท'' = ฮป x โ†’ r (r' (s' (s x))) โ‰กโŸจ ap r (ฮท' (s x)) โŸฉ
              r (s x)           โ‰กโŸจ ฮท x             โŸฉ
              x                 โˆŽ

_โ—โŸจ_โŸฉ_ : (X : ๐“ค ฬ‡ ) {Y : ๐“ฅ ฬ‡ } {Z : ๐“ฆ ฬ‡ } โ†’ X โ— Y โ†’ Y โ— Z โ†’ X โ— Z
X โ—โŸจ ฯ โŸฉ ฯƒ = ฯ โ—โˆ˜ ฯƒ

_โ—€ : (X : ๐“ค ฬ‡ ) โ†’ X โ— X
X โ—€ = id-โ— X

ฮฃ-retract : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ } {B : X โ†’ ๐“ฆ ฬ‡ }
          โ†’ ((x : X) โ†’ A x โ—  B x) โ†’ ฮฃ A โ— ฮฃ B

ฮฃ-retract {๐“ค} {๐“ฅ} {๐“ฆ} {X} {A} {B} ฯ = Natฮฃ r , Natฮฃ s , ฮท'
 where
  r : (x : X) โ†’ B x โ†’ A x
  r x = retraction (ฯ x)

  s : (x : X) โ†’ A x โ†’ B x
  s x = section (ฯ x)

  ฮท : (x : X) (a : A x) โ†’ r x (s x a) โ‰ก a
  ฮท x = retract-equation (ฯ x)

  ฮท' : (ฯƒ : ฮฃ A) โ†’ Natฮฃ r (Natฮฃ s ฯƒ) โ‰ก ฯƒ
  ฮท' (x , a) = x , r x (s x a) โ‰กโŸจ to-ฮฃ-โ‰ก' (ฮท x a) โŸฉ
               x , a           โˆŽ

transport-is-retraction : {X : ๐“ค ฬ‡ } (A : X โ†’ ๐“ฅ ฬ‡ ) {x y : X} (p : x โ‰ก y)
                        โ†’ transport A p โˆ˜ transport A (p โปยน) โˆผ ๐‘–๐‘‘ (A y)

transport-is-retraction A (refl x) = refl

transport-is-section : {X : ๐“ค ฬ‡ } (A : X โ†’ ๐“ฅ ฬ‡ ) {x y : X} (p : x โ‰ก y)
                     โ†’ transport A (p โปยน) โˆ˜ transport A p โˆผ ๐‘–๐‘‘ (A x)

transport-is-section A (refl x) = refl

ฮฃ-reindexing-retract : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {A : X โ†’ ๐“ฆ ฬ‡ } (r : Y โ†’ X)
                     โ†’ has-section r
                     โ†’ (ฮฃ x ๊ž‰ X , A x) โ— (ฮฃ y ๊ž‰ Y , A (r y))

ฮฃ-reindexing-retract {๐“ค} {๐“ฅ} {๐“ฆ} {X} {Y} {A} r (s , ฮท) = ฮณ , ฯ† , ฮณฯ†
 where
  ฮณ : ฮฃ (A โˆ˜ r) โ†’ ฮฃ A
  ฮณ (y , a) = (r y , a)

  ฯ† : ฮฃ A โ†’ ฮฃ (A โˆ˜ r)
  ฯ† (x , a) = (s x , transport A ((ฮท x)โปยน) a)

  ฮณฯ† : (ฯƒ : ฮฃ A) โ†’ ฮณ (ฯ† ฯƒ) โ‰ก ฯƒ
  ฮณฯ† (x , a) = p
   where
    p : (r (s x) , transport A ((ฮท x)โปยน) a) โ‰ก (x , a)
    p = to-ฮฃ-โ‰ก (ฮท x , transport-is-retraction A (ฮท x) a)

singleton-type : {X : ๐“ค ฬ‡ } โ†’ X โ†’ ๐“ค ฬ‡
singleton-type {๐“ค} {X} x = ฮฃ y ๊ž‰ X , y โ‰ก x

singleton-type-center : {X : ๐“ค ฬ‡ } (x : X) โ†’ singleton-type x
singleton-type-center x = (x , refl x)

singleton-type-centered : {X : ๐“ค ฬ‡ } (x : X) (ฯƒ : singleton-type x)
                        โ†’ singleton-type-center x โ‰ก ฯƒ

singleton-type-centered x (x , refl x) = refl (x , refl x)

singleton-types-are-singletons : (X : ๐“ค ฬ‡ ) (x : X)
                               โ†’ is-singleton (singleton-type x)

singleton-types-are-singletons X x = singleton-type-center x ,
                                     singleton-type-centered x

retract-of-singleton : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
                     โ†’ Y โ— X โ†’ is-singleton X โ†’ is-singleton Y

retract-of-singleton (r , s , ฮท) (c , ฯ†) = r c , ฮณ
 where
  ฮณ = ฮป y โ†’ r c     โ‰กโŸจ ap r (ฯ† (s y)) โŸฉ
            r (s y) โ‰กโŸจ ฮท y            โŸฉ
            y       โˆŽ

singleton-type' : {X : ๐“ค ฬ‡ } โ†’ X โ†’ ๐“ค ฬ‡
singleton-type' {๐“ค} {X} x = ฮฃ y ๊ž‰ X , x โ‰ก y

singleton-type'-center : {X : ๐“ค ฬ‡ } (x : X) โ†’ singleton-type' x
singleton-type'-center x = (x , refl x)

singleton-type'-centered : {X : ๐“ค ฬ‡ } (x : X) (ฯƒ : singleton-type' x)
                         โ†’ singleton-type'-center x โ‰ก ฯƒ

singleton-type'-centered x (x , refl x) = refl (x , refl x)

singleton-types'-are-singletons : (X : ๐“ค ฬ‡ ) (x : X)
                                โ†’ is-singleton (singleton-type' x)

singleton-types'-are-singletons X x = singleton-type'-center x ,
                                      singleton-type'-centered x

invertible : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ (X โ†’ Y) โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
invertible f = ฮฃ g ๊ž‰ (codomain f โ†’ domain f) , (g โˆ˜ f โˆผ id) ร— (f โˆ˜ g โˆผ id)

fiber : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y) โ†’ Y โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
fiber f y = ฮฃ x ๊ž‰ domain f , f x โ‰ก y

fiber-point : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {f : X โ†’ Y} {y : Y}
            โ†’ fiber f y โ†’ X

fiber-point (x , p) = x

fiber-identification : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {f : X โ†’ Y} {y : Y}
                     โ†’ (w : fiber f y) โ†’ f (fiber-point w) โ‰ก y

fiber-identification (x , p) = p

is-equiv : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ (X โ†’ Y) โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
is-equiv f = (y : codomain f) โ†’ is-singleton (fiber f y)

inverse : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y) โ†’ is-equiv f โ†’ (Y โ†’ X)
inverse f e y = fiber-point (center (fiber f y) (e y))

inverses-are-sections : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y) (e : is-equiv f)
                      โ†’ f โˆ˜ inverse f e โˆผ id

inverses-are-sections f e y = fiber-identification (center (fiber f y) (e y))

inverse-centrality : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
                     (f : X โ†’ Y) (e : is-equiv f) (y : Y) (t : fiber f y)
                   โ†’ (inverse f e y , inverses-are-sections f e y) โ‰ก t

inverse-centrality f e y = centrality (fiber f y) (e y)

inverses-are-retractions : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y) (e : is-equiv f)
                         โ†’ inverse f e โˆ˜ f โˆผ id

inverses-are-retractions f e x = ap fiber-point p
 where
  p : inverse f e (f x) , inverses-are-sections f e (f x) โ‰ก x , refl (f x)
  p = inverse-centrality f e (f x) (x , (refl (f x)))

equivs-are-invertible : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
                      โ†’ is-equiv f โ†’ invertible f

equivs-are-invertible f e = inverse f e ,
                            inverses-are-retractions f e ,
                            inverses-are-sections f e

invertibles-are-equivs : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
                       โ†’ invertible f โ†’ is-equiv f

invertibles-are-equivs {๐“ค} {๐“ฅ} {X} {Y} f (g , ฮท , ฮต) yโ‚€ = iii
 where
  i : (y : Y) โ†’ (f (g y) โ‰ก yโ‚€) โ— (y โ‰ก yโ‚€)
  i y =  r , s , transport-is-section (_โ‰ก yโ‚€) (ฮต y)
   where
    s : f (g y) โ‰ก yโ‚€ โ†’ y โ‰ก yโ‚€
    s = transport (_โ‰ก yโ‚€) (ฮต y)

    r : y โ‰ก yโ‚€ โ†’ f (g y) โ‰ก yโ‚€
    r = transport (_โ‰ก yโ‚€) ((ฮต y)โปยน)

  ii : fiber f yโ‚€ โ— singleton-type yโ‚€
  ii = (ฮฃ x ๊ž‰ X , f x โ‰ก yโ‚€)     โ—โŸจ ฮฃ-reindexing-retract g (f , ฮท) โŸฉ
       (ฮฃ y ๊ž‰ Y , f (g y) โ‰ก yโ‚€) โ—โŸจ ฮฃ-retract i                    โŸฉ
       (ฮฃ y ๊ž‰ Y , y โ‰ก yโ‚€)       โ—€

  iii : is-singleton (fiber f yโ‚€)
  iii = retract-of-singleton ii (singleton-types-are-singletons Y yโ‚€)

inverses-are-equivs : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y) (e : is-equiv f)
                    โ†’ is-equiv (inverse f e)

inverses-are-equivs f e = invertibles-are-equivs
                           (inverse f e)
                           (f , inverses-are-sections f e , inverses-are-retractions f e)

inversion-involutive : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y) (e : is-equiv f)
                     โ†’ inverse (inverse f e) (inverses-are-equivs f e) โ‰ก f

inversion-involutive f e = refl f

id-invertible : (X : ๐“ค ฬ‡ ) โ†’ invertible (๐‘–๐‘‘ X)
id-invertible X = ๐‘–๐‘‘ X , refl , refl

โˆ˜-invertible : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {Z : ๐“ฆ ฬ‡ } {f : X โ†’ Y} {f' : Y โ†’ Z}
             โ†’ invertible f' โ†’ invertible f โ†’ invertible (f' โˆ˜ f)

โˆ˜-invertible {๐“ค} {๐“ฅ} {๐“ฆ} {X} {Y} {Z} {f} {f'} (g' , gf' , fg') (g , gf , fg) =
  g โˆ˜ g' , ฮท , ฮต
 where
  ฮท = ฮป x โ†’ g (g' (f' (f x))) โ‰กโŸจ ap g (gf' (f x)) โŸฉ
            g (f x)           โ‰กโŸจ gf x             โŸฉ
            x                 โˆŽ

  ฮต = ฮป z โ†’ f' (f (g (g' z))) โ‰กโŸจ ap f' (fg (g' z)) โŸฉ
            f' (g' z)         โ‰กโŸจ fg' z             โŸฉ
            z                 โˆŽ

id-is-equiv : (X : ๐“ค ฬ‡ ) โ†’ is-equiv (๐‘–๐‘‘ X)
id-is-equiv = singleton-types-are-singletons

โˆ˜-is-equiv : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {Z : ๐“ฆ ฬ‡ } {f : X โ†’ Y} {g : Y โ†’ Z}
           โ†’ is-equiv g โ†’ is-equiv f โ†’ is-equiv (g โˆ˜ f)

โˆ˜-is-equiv {๐“ค} {๐“ฅ} {๐“ฆ} {X} {Y} {Z} {f} {g} i j = ฮณ
 where
  abstract
   ฮณ : is-equiv (g โˆ˜ f)
   ฮณ = invertibles-are-equivs (g โˆ˜ f)
         (โˆ˜-invertible (equivs-are-invertible g i)
                       (equivs-are-invertible f j))

inverse-of-โˆ˜ : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {Z : ๐“ฆ ฬ‡ }
               (f : X โ†’ Y) (g : Y โ†’ Z)
               (i : is-equiv f) (j : is-equiv g)
             โ†’ inverse f i โˆ˜ inverse g j โˆผ inverse (g โˆ˜ f) (โˆ˜-is-equiv j i)

inverse-of-โˆ˜ f g i j z =

  f' (g' z)             โ‰กโŸจ (ap (f' โˆ˜ g') (s z))โปยน                         โŸฉ
  f' (g' (g (f (h z)))) โ‰กโŸจ ap f' (inverses-are-retractions g j (f (h z))) โŸฉ
  f' (f (h z))          โ‰กโŸจ inverses-are-retractions f i (h z)             โŸฉ
  h z                   โˆŽ

 where
  f' = inverse f i
  g' = inverse g j
  h  = inverse (g โˆ˜ f) (โˆ˜-is-equiv j i)

  s : g โˆ˜ f โˆ˜ h โˆผ id
  s = inverses-are-sections (g โˆ˜ f) (โˆ˜-is-equiv j i)

_โ‰ƒ_ : ๐“ค ฬ‡ โ†’ ๐“ฅ ฬ‡ โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
X โ‰ƒ Y = ฮฃ f ๊ž‰ (X โ†’ Y), is-equiv f

Eqโ†’fun โŒœ_โŒ : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ X โ‰ƒ Y โ†’ X โ†’ Y
Eqโ†’fun (f , i) = f
โŒœ_โŒ            = Eqโ†’fun

Eqโ†’fun-is-equiv โŒœโŒ-is-equiv : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (e : X โ‰ƒ Y) โ†’ is-equiv (โŒœ e โŒ)
Eqโ†’fun-is-equiv (f , i) = i
โŒœโŒ-is-equiv             = Eqโ†’fun-is-equiv

invertibility-gives-โ‰ƒ : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
                      โ†’ invertible f โ†’ X โ‰ƒ Y

invertibility-gives-โ‰ƒ f i = f , invertibles-are-equivs f i

ฮฃ-induction-โ‰ƒ : {X : ๐“ค ฬ‡ } {Y : X โ†’ ๐“ฅ ฬ‡ } {A : ฮฃ Y โ†’ ๐“ฆ ฬ‡ }
              โ†’ ((x : X) (y : Y x) โ†’ A (x , y)) โ‰ƒ ((z : ฮฃ Y) โ†’ A z)

ฮฃ-induction-โ‰ƒ = invertibility-gives-โ‰ƒ ฮฃ-induction (curry , refl , refl)

ฮฃ-flip : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {A : X โ†’ Y โ†’ ๐“ฆ ฬ‡ }
       โ†’ (ฮฃ x ๊ž‰ X , ฮฃ y ๊ž‰ Y , A x y) โ‰ƒ (ฮฃ y ๊ž‰ Y , ฮฃ x ๊ž‰ X , A x y)

ฮฃ-flip = invertibility-gives-โ‰ƒ
          (ฮป (x , y , p) โ†’ (y , x , p))
          ((ฮป (y , x , p) โ†’ (x , y , p)) , refl , refl)

ร—-comm : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
       โ†’ (X ร— Y) โ‰ƒ (Y ร— X)

ร—-comm = invertibility-gives-โ‰ƒ
          (ฮป (x , y) โ†’ (y , x))
          ((ฮป (y , x) โ†’ (x , y)) , refl , refl)

id-โ‰ƒ : (X : ๐“ค ฬ‡ ) โ†’ X โ‰ƒ X
id-โ‰ƒ X = ๐‘–๐‘‘ X , id-is-equiv X

_โ—_ : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {Z : ๐“ฆ ฬ‡ } โ†’ X โ‰ƒ Y โ†’ Y โ‰ƒ Z โ†’ X โ‰ƒ Z
(f , d) โ— (f' , e) = f' โˆ˜ f , โˆ˜-is-equiv e d

โ‰ƒ-sym : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ X โ‰ƒ Y โ†’ Y โ‰ƒ X
โ‰ƒ-sym (f , e) = inverse f e , inverses-are-equivs f e

_โ‰ƒโŸจ_โŸฉ_ : (X : ๐“ค ฬ‡ ) {Y : ๐“ฅ ฬ‡ } {Z : ๐“ฆ ฬ‡ } โ†’ X โ‰ƒ Y โ†’ Y โ‰ƒ Z โ†’ X โ‰ƒ Z
_ โ‰ƒโŸจ d โŸฉ e = d โ— e

_โ–  : (X : ๐“ค ฬ‡ ) โ†’ X โ‰ƒ X
_โ–  = id-โ‰ƒ

transport-is-equiv : {X : ๐“ค ฬ‡ } (A : X โ†’ ๐“ฅ ฬ‡ ) {x y : X} (p : x โ‰ก y)
                   โ†’ is-equiv (transport A p)

transport-is-equiv A (refl x) = id-is-equiv (A x)

ฮฃ-โ‰ก-โ‰ƒ : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ } (ฯƒ ฯ„ : ฮฃ A)
      โ†’ (ฯƒ โ‰ก ฯ„) โ‰ƒ (ฮฃ p ๊ž‰ prโ‚ ฯƒ โ‰ก prโ‚ ฯ„ , transport A p (prโ‚‚ ฯƒ) โ‰ก prโ‚‚ ฯ„)

ฮฃ-โ‰ก-โ‰ƒ {๐“ค} {๐“ฅ} {X} {A}  ฯƒ ฯ„ = invertibility-gives-โ‰ƒ from-ฮฃ-โ‰ก (to-ฮฃ-โ‰ก , ฮท , ฮต)
 where
  ฮท : (q : ฯƒ โ‰ก ฯ„) โ†’ to-ฮฃ-โ‰ก (from-ฮฃ-โ‰ก q) โ‰ก q
  ฮท (refl ฯƒ) = refl (refl ฯƒ)

  ฮต : (w : ฮฃ p ๊ž‰ prโ‚ ฯƒ โ‰ก prโ‚ ฯ„ , transport A p (prโ‚‚ ฯƒ) โ‰ก prโ‚‚ ฯ„)
    โ†’ from-ฮฃ-โ‰ก (to-ฮฃ-โ‰ก w) โ‰ก w

  ฮต (refl p , refl q) = refl (refl p , refl q)

to-ร—-โ‰ก : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {z t : X ร— Y}
       โ†’ (prโ‚ z โ‰ก prโ‚ t) ร— (prโ‚‚ z โ‰ก prโ‚‚ t) โ†’ z โ‰ก t

to-ร—-โ‰ก (refl x , refl y) = refl (x , y)

from-ร—-โ‰ก : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {z t : X ร— Y}
         โ†’ z โ‰ก t โ†’ (prโ‚ z โ‰ก prโ‚ t) ร— (prโ‚‚ z โ‰ก prโ‚‚ t)

from-ร—-โ‰ก {๐“ค} {๐“ฅ} {X} {Y} (refl (x , y)) = (refl x , refl y)

ร—-โ‰ก-โ‰ƒ : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (z t : X ร— Y)
      โ†’ (z โ‰ก t) โ‰ƒ (prโ‚ z โ‰ก prโ‚ t) ร— (prโ‚‚ z โ‰ก prโ‚‚ t)

ร—-โ‰ก-โ‰ƒ {๐“ค} {๐“ฅ} {X} {Y} z t = invertibility-gives-โ‰ƒ from-ร—-โ‰ก (to-ร—-โ‰ก , ฮท , ฮต)
 where
  ฮท : (p : z โ‰ก t) โ†’ to-ร—-โ‰ก (from-ร—-โ‰ก p) โ‰ก p
  ฮท (refl z) = refl (refl z)

  ฮต : (q : (prโ‚ z โ‰ก prโ‚ t) ร— (prโ‚‚ z โ‰ก prโ‚‚ t)) โ†’ from-ร—-โ‰ก (to-ร—-โ‰ก q) โ‰ก q
  ฮต (refl x , refl y) = refl (refl x , refl y)

ap-prโ‚-to-ร—-โ‰ก : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {z t : X ร— Y}
              โ†’ (pโ‚ : prโ‚ z โ‰ก prโ‚ t)
              โ†’ (pโ‚‚ : prโ‚‚ z โ‰ก prโ‚‚ t)
              โ†’ ap prโ‚ (to-ร—-โ‰ก (pโ‚ , pโ‚‚)) โ‰ก pโ‚

ap-prโ‚-to-ร—-โ‰ก (refl x) (refl y) = refl (refl x)

ap-prโ‚‚-to-ร—-โ‰ก : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {z t : X ร— Y}
              โ†’ (pโ‚ : prโ‚ z โ‰ก prโ‚ t)
              โ†’ (pโ‚‚ : prโ‚‚ z โ‰ก prโ‚‚ t)
              โ†’ ap prโ‚‚ (to-ร—-โ‰ก (pโ‚ , pโ‚‚)) โ‰ก pโ‚‚

ap-prโ‚‚-to-ร—-โ‰ก (refl x) (refl y) = refl (refl y)

ฮฃ-cong : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ } {B : X โ†’ ๐“ฆ ฬ‡ }
       โ†’ ((x : X) โ†’ A x โ‰ƒ B x) โ†’ ฮฃ A โ‰ƒ ฮฃ B

ฮฃ-cong {๐“ค} {๐“ฅ} {๐“ฆ} {X} {A} {B} ฯ† =
  invertibility-gives-โ‰ƒ (Natฮฃ f) (Natฮฃ g , Natฮฃ-ฮท , Natฮฃ-ฮต)
 where
  f : (x : X) โ†’ A x โ†’ B x
  f x = โŒœ ฯ† x โŒ

  g : (x : X) โ†’ B x โ†’ A x
  g x = inverse (f x) (โŒœโŒ-is-equiv (ฯ† x))

  ฮท : (x : X) (a : A x) โ†’ g x (f x a) โ‰ก a
  ฮท x = inverses-are-retractions (f x) (โŒœโŒ-is-equiv (ฯ† x))

  ฮต : (x : X) (b : B x) โ†’ f x (g x b) โ‰ก b
  ฮต x = inverses-are-sections (f x) (โŒœโŒ-is-equiv (ฯ† x))

  Natฮฃ-ฮท : (w : ฮฃ A) โ†’ Natฮฃ g (Natฮฃ f w) โ‰ก w
  Natฮฃ-ฮท (x , a) = x , g x (f x a) โ‰กโŸจ to-ฮฃ-โ‰ก' (ฮท x a) โŸฉ
                   x , a           โˆŽ

  Natฮฃ-ฮต : (t : ฮฃ B) โ†’ Natฮฃ f (Natฮฃ g t) โ‰ก t
  Natฮฃ-ฮต (x , b) = x , f x (g x b) โ‰กโŸจ to-ฮฃ-โ‰ก' (ฮต x b) โŸฉ
                   x , b           โˆŽ

โ‰ƒ-gives-โ— : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ X โ‰ƒ Y โ†’ X โ— Y
โ‰ƒ-gives-โ— (f , e) = (inverse f e , f , inverses-are-retractions f e)

โ‰ƒ-gives-โ–ท : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ X โ‰ƒ Y โ†’ Y โ— X
โ‰ƒ-gives-โ–ท (f , e) = (f , inverse f e , inverses-are-sections f e)

equiv-to-singleton : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
                   โ†’ X โ‰ƒ Y โ†’ is-singleton Y โ†’ is-singleton X

equiv-to-singleton e = retract-of-singleton (โ‰ƒ-gives-โ— e)

Idโ†’Eq : (X Y : ๐“ค ฬ‡ ) โ†’ X โ‰ก Y โ†’ X โ‰ƒ Y
Idโ†’Eq X X (refl X) = id-โ‰ƒ X

is-univalent : (๐“ค : Universe) โ†’ ๐“ค โบ ฬ‡
is-univalent ๐“ค = (X Y : ๐“ค ฬ‡ ) โ†’ is-equiv (Idโ†’Eq X Y)

univalence-โ‰ƒ : is-univalent ๐“ค โ†’ (X Y : ๐“ค ฬ‡ ) โ†’ (X โ‰ก Y) โ‰ƒ (X โ‰ƒ Y)
univalence-โ‰ƒ ua X Y = Idโ†’Eq X Y , ua X Y

Eqโ†’Id : is-univalent ๐“ค โ†’ (X Y : ๐“ค ฬ‡ ) โ†’ X โ‰ƒ Y โ†’ X โ‰ก Y
Eqโ†’Id ua X Y = inverse (Idโ†’Eq X Y) (ua X Y)

Idโ†’fun : {X Y : ๐“ค ฬ‡ } โ†’ X โ‰ก Y โ†’ X โ†’ Y
Idโ†’fun {๐“ค} {X} {Y} p = โŒœ Idโ†’Eq X Y p โŒ

Idโ†’funs-agree : {X Y : ๐“ค ฬ‡ } (p : X โ‰ก Y)
              โ†’ Idโ†’fun p โ‰ก Idโ†’Fun p
Idโ†’funs-agree (refl X) = refl (๐‘–๐‘‘ X)

swapโ‚‚ : ๐Ÿš โ†’ ๐Ÿš
swapโ‚‚ โ‚€ = โ‚
swapโ‚‚ โ‚ = โ‚€

swapโ‚‚-involutive : (n : ๐Ÿš) โ†’ swapโ‚‚ (swapโ‚‚ n) โ‰ก n
swapโ‚‚-involutive โ‚€ = refl โ‚€
swapโ‚‚-involutive โ‚ = refl โ‚

swapโ‚‚-is-equiv : is-equiv swapโ‚‚
swapโ‚‚-is-equiv = invertibles-are-equivs
                  swapโ‚‚
                  (swapโ‚‚ , swapโ‚‚-involutive , swapโ‚‚-involutive)

module example-of-a-nonset (ua : is-univalent ๐“คโ‚€) where

 eโ‚€ eโ‚ : ๐Ÿš โ‰ƒ ๐Ÿš
 eโ‚€ = id-โ‰ƒ ๐Ÿš
 eโ‚ = swapโ‚‚ , swapโ‚‚-is-equiv

 eโ‚€-is-not-eโ‚ : eโ‚€ โ‰ข eโ‚
 eโ‚€-is-not-eโ‚ p = โ‚-is-not-โ‚€ r
  where
   q : id โ‰ก swapโ‚‚
   q = ap โŒœ_โŒ p

   r : โ‚ โ‰ก โ‚€
   r = ap (ฮป - โ†’ - โ‚) q

 pโ‚€ pโ‚ : ๐Ÿš โ‰ก ๐Ÿš
 pโ‚€ = Eqโ†’Id ua ๐Ÿš ๐Ÿš eโ‚€
 pโ‚ = Eqโ†’Id ua ๐Ÿš ๐Ÿš eโ‚

 pโ‚€-is-not-pโ‚ : pโ‚€ โ‰ข pโ‚
 pโ‚€-is-not-pโ‚ q = eโ‚€-is-not-eโ‚ r
  where
   r = eโ‚€            โ‰กโŸจ (inverses-are-sections (Idโ†’Eq ๐Ÿš ๐Ÿš) (ua ๐Ÿš ๐Ÿš) eโ‚€)โปยน โŸฉ
       Idโ†’Eq ๐Ÿš ๐Ÿš pโ‚€  โ‰กโŸจ ap (Idโ†’Eq ๐Ÿš ๐Ÿš) q                                  โŸฉ
       Idโ†’Eq ๐Ÿš ๐Ÿš pโ‚  โ‰กโŸจ inverses-are-sections (Idโ†’Eq ๐Ÿš ๐Ÿš) (ua ๐Ÿš ๐Ÿš) eโ‚     โŸฉ
       eโ‚            โˆŽ

 ๐“คโ‚€-is-not-a-set : ยฌ(is-set (๐“คโ‚€ ฬ‡ ))
 ๐“คโ‚€-is-not-a-set s = pโ‚€-is-not-pโ‚ q
  where
   q : pโ‚€ โ‰ก pโ‚
   q = s ๐Ÿš ๐Ÿš pโ‚€ pโ‚

subsingleton-criterion : {X : ๐“ค ฬ‡ }
                       โ†’ (X โ†’ is-singleton X)
                       โ†’ is-subsingleton X

subsingleton-criterion' : {X : ๐“ค ฬ‡ }
                        โ†’ (X โ†’ is-subsingleton X)
                        โ†’ is-subsingleton X

retract-of-subsingleton : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
                        โ†’ Y โ— X โ†’ is-subsingleton X โ†’ is-subsingleton Y

left-cancellable : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ (X โ†’ Y) โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
left-cancellable f = {x x' : domain f} โ†’ f x โ‰ก f x' โ†’ x โ‰ก x'

lc-maps-reflect-subsingletons : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
                              โ†’ left-cancellable f
                              โ†’ is-subsingleton Y
                              โ†’ is-subsingleton X

has-retraction : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ (X โ†’ Y) โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
has-retraction s = ฮฃ r ๊ž‰ (codomain s โ†’ domain s), r โˆ˜ s โˆผ id

sections-are-lc : {X : ๐“ค ฬ‡ } {A : ๐“ฅ ฬ‡ } (s : X โ†’ A)
                โ†’ has-retraction s โ†’ left-cancellable s

equivs-have-retractions : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
                        โ†’ is-equiv f โ†’ has-retraction f

equivs-have-sections : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
                     โ†’ is-equiv f โ†’ has-section f

equivs-are-lc : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
              โ†’ is-equiv f โ†’ left-cancellable f

equiv-to-subsingleton : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
                      โ†’ X โ‰ƒ Y
                      โ†’ is-subsingleton Y
                      โ†’ is-subsingleton X

comp-inverses : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {Z : ๐“ฆ ฬ‡ }
                (f : X โ†’ Y) (g : Y โ†’ Z)
                (i : is-equiv f) (j : is-equiv g)
                (f' : Y โ†’ X) (g' : Z โ†’ Y)
              โ†’ f' โˆผ inverse f i
              โ†’ g' โˆผ inverse g j
              โ†’ f' โˆ˜ g' โˆผ inverse (g โˆ˜ f) (โˆ˜-is-equiv j i)

equiv-to-set : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
             โ†’ X โ‰ƒ Y
             โ†’ is-set Y
             โ†’ is-set X

sections-closed-under-โˆผ : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f g : X โ†’ Y)
                        โ†’ has-retraction f
                        โ†’ g โˆผ f
                        โ†’ has-retraction g

retractions-closed-under-โˆผ : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f g : X โ†’ Y)
                           โ†’ has-section f
                           โ†’ g โˆผ f
                           โ†’ has-section g

is-joyal-equiv : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ (X โ†’ Y) โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
is-joyal-equiv f = has-section f ร— has-retraction f

one-inverse : (X : ๐“ค ฬ‡ ) (Y : ๐“ฅ ฬ‡ )
              (f : X โ†’ Y) (r s : Y โ†’ X)
            โ†’ (r โˆ˜ f โˆผ id)
            โ†’ (f โˆ˜ s โˆผ id)
            โ†’ r โˆผ s

joyal-equivs-are-invertible : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
                            โ†’ is-joyal-equiv f โ†’ invertible f

joyal-equivs-are-equivs : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
                        โ†’ is-joyal-equiv f โ†’ is-equiv f

invertibles-are-joyal-equivs : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
                             โ†’ invertible f โ†’ is-joyal-equiv f

equivs-are-joyal-equivs : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
                        โ†’ is-equiv f โ†’ is-joyal-equiv f

equivs-closed-under-โˆผ : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {f g : X โ†’ Y}
                      โ†’ is-equiv f
                      โ†’ g โˆผ f
                      โ†’ is-equiv g

equiv-to-singleton' : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
                    โ†’ X โ‰ƒ Y โ†’ is-singleton X โ†’ is-singleton Y

subtypes-of-sets-are-sets : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (m : X โ†’ Y)
                          โ†’ left-cancellable m โ†’ is-set Y โ†’ is-set X

prโ‚-lc : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ }
       โ†’ ((x : X) โ†’ is-subsingleton (A x))
       โ†’ left-cancellable (ฮป (t : ฮฃ A) โ†’ prโ‚ t)

subsets-of-sets-are-sets : (X : ๐“ค ฬ‡ ) (A : X โ†’ ๐“ฅ ฬ‡ )
                         โ†’ is-set X
                         โ†’ ((x : X) โ†’ is-subsingleton (A x))
                         โ†’ is-set (ฮฃ x ๊ž‰ X , A x)

to-subtype-โ‰ก : {X : ๐“ฆ ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ }
               {x y : X} {a : A x} {b : A y}
             โ†’ ((x : X) โ†’ is-subsingleton (A x))
             โ†’ x โ‰ก y
             โ†’ (x , a) โ‰ก (y , b)

prโ‚-is-equiv : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ }
             โ†’ ((x : X) โ†’ is-singleton (A x))
             โ†’ is-equiv (ฮป (t : ฮฃ A) โ†’ prโ‚ t)

prโ‚-โ‰ƒ : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ }
      โ†’ ((x : X) โ†’ is-singleton (A x))
      โ†’ ฮฃ A โ‰ƒ X

prโ‚-โ‰ƒ i = prโ‚ , prโ‚-is-equiv i

ฮ ฮฃ-distr-โ‰ƒ : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ } {P : (x : X) โ†’ A x โ†’ ๐“ฆ ฬ‡ }
           โ†’ (ฮ  x ๊ž‰ X , ฮฃ a ๊ž‰ A x , P x a)
           โ‰ƒ (ฮฃ f ๊ž‰ ฮ  A , ฮ  x ๊ž‰ X , P x (f x))

ฮฃ-assoc : {X : ๐“ค ฬ‡ } {Y : X โ†’ ๐“ฅ ฬ‡ } {Z : ฮฃ Y โ†’ ๐“ฆ ฬ‡ }
        โ†’ ฮฃ Z โ‰ƒ (ฮฃ x ๊ž‰ X , ฮฃ y ๊ž‰ Y x , Z (x , y))

โปยน-โ‰ƒ : {X : ๐“ค ฬ‡ } (x y : X) โ†’ (x โ‰ก y) โ‰ƒ (y โ‰ก x)

singleton-types-โ‰ƒ : {X : ๐“ค ฬ‡ } (x : X) โ†’ singleton-type' x โ‰ƒ singleton-type x

singletons-โ‰ƒ : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
             โ†’ is-singleton X โ†’ is-singleton Y โ†’ X โ‰ƒ Y

maps-of-singletons-are-equivs : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
                              โ†’ is-singleton X โ†’ is-singleton Y โ†’ is-equiv f

logically-equivalent-subsingletons-are-equivalent : (X : ๐“ค ฬ‡ ) (Y : ๐“ฅ ฬ‡ )
                                                  โ†’ is-subsingleton X
                                                  โ†’ is-subsingleton Y
                                                  โ†’ X โ‡” Y
                                                  โ†’ X โ‰ƒ Y

singletons-are-equivalent : (X : ๐“ค ฬ‡ ) (Y : ๐“ฅ ฬ‡ )
                          โ†’ is-singleton X
                          โ†’ is-singleton Y
                          โ†’ X โ‰ƒ Y

Natฮฃ-fiber-equiv : {X : ๐“ค ฬ‡ } (A : X โ†’ ๐“ฅ ฬ‡ ) (B : X โ†’ ๐“ฆ ฬ‡ ) (ฯ† : Nat A B)
                   (x : X) (b : B x)
                 โ†’ fiber (ฯ† x) b โ‰ƒ fiber (Natฮฃ ฯ†) (x , b)

Natฮฃ-equiv-gives-fiberwise-equiv : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ } {B : X โ†’ ๐“ฆ ฬ‡ }
                                   (ฯ† : Nat A B)
                                 โ†’ is-equiv (Natฮฃ ฯ†)
                                 โ†’ ((x : X) โ†’ is-equiv (ฯ† x))

ฮฃ-is-subsingleton : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ }
                  โ†’ is-subsingleton X
                  โ†’ ((x : X) โ†’ is-subsingleton (A x))
                  โ†’ is-subsingleton (ฮฃ A)

ร—-is-singleton : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
                  โ†’ is-singleton X
                  โ†’ is-singleton Y
                  โ†’ is-singleton (X ร— Y)

ร—-is-subsingleton : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
                  โ†’ is-subsingleton X
                  โ†’ is-subsingleton Y
                  โ†’ is-subsingleton (X ร— Y)

ร—-is-subsingleton' : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
                   โ†’ ((Y โ†’ is-subsingleton X) ร— (X โ†’ is-subsingleton Y))
                   โ†’ is-subsingleton (X ร— Y)

ร—-is-subsingleton'-back : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
                        โ†’ is-subsingleton (X ร— Y)
                        โ†’ (Y โ†’ is-subsingleton X) ร— (X โ†’ is-subsingleton Y)

apโ‚‚ : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {Z : ๐“ฆ ฬ‡ } (f : X โ†’ Y โ†’ Z) {x x' : X} {y y' : Y}
    โ†’ x โ‰ก x' โ†’ y โ‰ก y' โ†’ f x y โ‰ก f x' y'

subsingleton-criterion = sol
 where
  sol : {X : ๐“ค ฬ‡ } โ†’ (X โ†’ is-singleton X) โ†’ is-subsingleton X
  sol f x = singletons-are-subsingletons (domain f) (f x) x

subsingleton-criterion' = sol
 where
  sol : {X : ๐“ค ฬ‡ } โ†’ (X โ†’ is-subsingleton X) โ†’ is-subsingleton X
  sol f x y = f x x y

retract-of-subsingleton = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
      โ†’ Y โ— X โ†’ is-subsingleton X โ†’ is-subsingleton Y
  sol (r , s , ฮท) i =  subsingleton-criterion
                        (ฮป x โ†’ retract-of-singleton (r , s , ฮท)
                                (pointed-subsingletons-are-singletons
                                  (codomain s) (s x) i))

lc-maps-reflect-subsingletons = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
      โ†’ left-cancellable f โ†’ is-subsingleton Y โ†’ is-subsingleton X
  sol f l s x x' = l (s (f x) (f x'))

sections-are-lc = sol
 where
  sol : {X : ๐“ค ฬ‡ } {A : ๐“ฅ ฬ‡ } (s : X โ†’ A)
      โ†’ has-retraction s โ†’ left-cancellable s
  sol s (r , ฮต) {x} {y} p = x       โ‰กโŸจ (ฮต x)โปยน โŸฉ
                            r (s x) โ‰กโŸจ ap r p  โŸฉ
                            r (s y) โ‰กโŸจ ฮต y     โŸฉ
                            y       โˆŽ

equivs-have-retractions = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y) โ†’ is-equiv f โ†’ has-retraction f
  sol f e = (inverse f e , inverses-are-retractions f e)

equivs-have-sections = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y) โ†’ is-equiv f โ†’ has-section f
  sol f e = (inverse f e , inverses-are-sections f e)

equivs-are-lc = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y) โ†’ is-equiv f โ†’ left-cancellable f
  sol f e = sections-are-lc f (equivs-have-retractions f e)

equiv-to-subsingleton = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ X โ‰ƒ Y โ†’ is-subsingleton Y โ†’ is-subsingleton X
  sol (f , i) = lc-maps-reflect-subsingletons f (equivs-are-lc f i)

comp-inverses = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {Z : ๐“ฆ ฬ‡ }
        (f : X โ†’ Y) (g : Y โ†’ Z)
        (i : is-equiv f) (j : is-equiv g)
        (f' : Y โ†’ X) (g' : Z โ†’ Y)
      โ†’ f' โˆผ inverse f i
      โ†’ g' โˆผ inverse g j
      โ†’ f' โˆ˜ g' โˆผ inverse (g โˆ˜ f) (โˆ˜-is-equiv j i)
  sol f g i j f' g' h k z =
   f' (g' z)                          โ‰กโŸจ h (g' z)               โŸฉ
   inverse f i (g' z)                 โ‰กโŸจ ap (inverse f i) (k z) โŸฉ
   inverse f i (inverse g j z)        โ‰กโŸจ inverse-of-โˆ˜ f g i j z โŸฉ
   inverse (g โˆ˜ f) (โˆ˜-is-equiv j i) z โˆŽ

equiv-to-set = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ X โ‰ƒ Y โ†’ is-set Y โ†’ is-set X
  sol e = subtypes-of-sets-are-sets โŒœ e โŒ (equivs-are-lc โŒœ e โŒ (โŒœโŒ-is-equiv e))

sections-closed-under-โˆผ = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f g : X โ†’ Y)
      โ†’ has-retraction f โ†’ g โˆผ f โ†’ has-retraction g
  sol f g (r , rf) h = (r ,
                        ฮป x โ†’ r (g x) โ‰กโŸจ ap r (h x) โŸฉ
                              r (f x) โ‰กโŸจ rf x       โŸฉ
                              x       โˆŽ)

retractions-closed-under-โˆผ = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f g : X โ†’ Y)
      โ†’ has-section f โ†’ g โˆผ f โ†’ has-section g
  sol f g (s , fs) h = (s ,
                        ฮป y โ†’ g (s y) โ‰กโŸจ h (s y) โŸฉ
                              f (s y) โ‰กโŸจ fs y    โŸฉ
                              y โˆŽ)

one-inverse = sol
 where
  sol : (X : ๐“ค ฬ‡ ) (Y : ๐“ฅ ฬ‡ )
        (f : X โ†’ Y) (r s : Y โ†’ X)
      โ†’ (r โˆ˜ f โˆผ id)
      โ†’ (f โˆ˜ s โˆผ id)
      โ†’ r โˆผ s
  sol X Y f r s h k y = r y         โ‰กโŸจ ap r ((k y)โปยน) โŸฉ
                        r (f (s y)) โ‰กโŸจ h (s y)        โŸฉ
                        s y         โˆŽ

joyal-equivs-are-invertible = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
      โ†’ is-joyal-equiv f โ†’ invertible f
  sol f ((s , ฮต) , (r , ฮท)) = (s , sf , ฮต)
   where
    sf = ฮป (x : domain f) โ†’ s(f x)       โ‰กโŸจ (ฮท (s (f x)))โปยน โŸฉ
                            r(f(s(f x))) โ‰กโŸจ ap r (ฮต (f x))  โŸฉ
                            r(f x)       โ‰กโŸจ ฮท x             โŸฉ
                            x            โˆŽ

joyal-equivs-are-equivs = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
      โ†’ is-joyal-equiv f โ†’ is-equiv f
  sol f j = invertibles-are-equivs f (joyal-equivs-are-invertible f j)

invertibles-are-joyal-equivs = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
      โ†’ invertible f โ†’ is-joyal-equiv f
  sol f (g , ฮท , ฮต) = ((g , ฮต) , (g , ฮท))

equivs-are-joyal-equivs = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
      โ†’ is-equiv f โ†’ is-joyal-equiv f
  sol f e = invertibles-are-joyal-equivs f (equivs-are-invertible f e)

equivs-closed-under-โˆผ = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {f g : X โ†’ Y}
      โ†’ is-equiv f โ†’ g โˆผ f โ†’ is-equiv g
  sol {๐“ค} {๐“ฅ} {X} {Y} {f} {g} e h = joyal-equivs-are-equivs g
                                      (retractions-closed-under-โˆผ f g
                                       (equivs-have-sections f e) h ,
                                      sections-closed-under-โˆผ f g
                                       (equivs-have-retractions f e) h)

equiv-to-singleton' = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
      โ†’ X โ‰ƒ Y โ†’ is-singleton X โ†’ is-singleton Y
  sol e = retract-of-singleton (โ‰ƒ-gives-โ–ท e)

subtypes-of-sets-are-sets = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (m : X โ†’ Y)
      โ†’ left-cancellable m โ†’ is-set Y โ†’ is-set X
  sol {๐“ค} {๐“ฅ} {X} m i h = types-with-wconstant-โ‰ก-endomaps-are-sets X c
   where
    f : (x x' : X) โ†’ x โ‰ก x' โ†’ x โ‰ก x'
    f x x' r = i (ap m r)

    ฮบ : (x x' : X) (r s : x โ‰ก x') โ†’ f x x' r โ‰ก f x x' s
    ฮบ x x' r s = ap i (h (m x) (m x') (ap m r) (ap m s))

    c : wconstant-โ‰ก-endomaps X
    c x x' = f x x' , ฮบ x x'

prโ‚-lc = sol
 where
  sol : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ }
      โ†’ ((x : X) โ†’ is-subsingleton (A x))
      โ†’ left-cancellable  (ฮป (t : ฮฃ A) โ†’ prโ‚ t)
  sol i p = to-ฮฃ-โ‰ก (p , i _ _ _)

subsets-of-sets-are-sets = sol
 where
  sol : (X : ๐“ค ฬ‡ ) (A : X โ†’ ๐“ฅ ฬ‡ )
     โ†’ is-set X
     โ†’ ((x : X) โ†’ is-subsingleton (A x))
     โ†’ is-set (ฮฃ x ๊ž‰ X , A x)
  sol X A h p = subtypes-of-sets-are-sets prโ‚ (prโ‚-lc p) h

to-subtype-โ‰ก = sol
 where
  sol : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ }
        {x y : X} {a : A x} {b : A y}
      โ†’ ((x : X) โ†’ is-subsingleton (A x))
      โ†’ x โ‰ก y
      โ†’ (x , a) โ‰ก (y , b)
  sol {๐“ค} {๐“ฅ} {X} {A} {x} {y} {a} {b} s p = to-ฮฃ-โ‰ก (p , s y (transport A p a) b)

prโ‚-is-equiv = sol
 where
  sol : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ }
      โ†’ ((x : X) โ†’ is-singleton (A x))
      โ†’ is-equiv (ฮป (t : ฮฃ A) โ†’ prโ‚ t)
  sol {๐“ค} {๐“ฅ} {X} {A} s = invertibles-are-equivs prโ‚ (g , ฮท , ฮต)
   where
    g : X โ†’ ฮฃ A
    g x = x , prโ‚(s x)

    ฮต : (x : X) โ†’ prโ‚ (g x) โ‰ก x
    ฮต x = refl (prโ‚ (g x))

    ฮท : (ฯƒ : ฮฃ A) โ†’ g (prโ‚ ฯƒ) โ‰ก ฯƒ
    ฮท (x , a) = to-subtype-โ‰ก (ฮป x โ†’ singletons-are-subsingletons (A x) (s x)) (ฮต x)

ฮ ฮฃ-distr-โ‰ƒ = sol
 where
  sol : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ } {P : (x : X) โ†’ A x โ†’ ๐“ฆ ฬ‡ }
      โ†’ (ฮ  x ๊ž‰ X , ฮฃ a ๊ž‰ A x , P x a)
      โ‰ƒ (ฮฃ f ๊ž‰ ฮ  A , ฮ  x ๊ž‰ X , P x (f x))
  sol {๐“ค} {๐“ฅ} {๐“ฆ} {X} {A} {P} = invertibility-gives-โ‰ƒ ฯ† (ฮณ , ฮท , ฮต)
   where
    ฯ† : (ฮ  x ๊ž‰ X , ฮฃ a ๊ž‰ A x , P x a)
      โ†’ ฮฃ f ๊ž‰ ฮ  A , ฮ  x ๊ž‰ X , P x (f x)
    ฯ† g = ((ฮป x โ†’ prโ‚ (g x)) , ฮป x โ†’ prโ‚‚ (g x))

    ฮณ : (ฮฃ f ๊ž‰ ฮ  A , ฮ  x ๊ž‰ X , P x (f x))
      โ†’ ฮ  x ๊ž‰ X , ฮฃ a ๊ž‰ A x , P x a
    ฮณ (f , ฯ†) x = f x , ฯ† x

    ฮท : ฮณ โˆ˜ ฯ† โˆผ id
    ฮท = refl

    ฮต : ฯ† โˆ˜ ฮณ โˆผ id
    ฮต = refl

ฮฃ-assoc = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : X โ†’ ๐“ฅ ฬ‡ } {Z : ฮฃ Y โ†’ ๐“ฆ ฬ‡ }
      โ†’ ฮฃ Z โ‰ƒ (ฮฃ x ๊ž‰ X , ฮฃ y ๊ž‰ Y x , Z (x , y))
  sol {๐“ค} {๐“ฅ} {๐“ฆ} {X} {Y} {Z} = invertibility-gives-โ‰ƒ f (g , refl , refl)
   where
    f : ฮฃ Z โ†’ ฮฃ x ๊ž‰ X , ฮฃ y ๊ž‰ Y x , Z (x , y)
    f ((x , y) , z) = (x , (y , z))

    g : (ฮฃ x ๊ž‰ X , ฮฃ y ๊ž‰ Y x , Z (x , y)) โ†’ ฮฃ Z
    g (x , (y , z)) = ((x , y) , z)

โปยน-is-equiv : {X : ๐“ค ฬ‡ } (x y : X)
            โ†’ is-equiv (ฮป (p : x โ‰ก y) โ†’ p โปยน)
โปยน-is-equiv x y = invertibles-are-equivs _โปยน
                   (_โปยน , โปยน-involutive , โปยน-involutive)

โปยน-โ‰ƒ = sol
 where
  sol : {X : ๐“ค ฬ‡ } (x y : X) โ†’ (x โ‰ก y) โ‰ƒ (y โ‰ก x)
  sol x y = (_โปยน , โปยน-is-equiv x y)

singleton-types-โ‰ƒ = sol
 where
  sol : {X : ๐“ค ฬ‡ } (x : X) โ†’ singleton-type' x โ‰ƒ singleton-type x
  sol x = ฮฃ-cong (ฮป y โ†’ โปยน-โ‰ƒ x y)

singletons-โ‰ƒ = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
      โ†’ is-singleton X โ†’ is-singleton Y โ†’ X โ‰ƒ Y
  sol {๐“ค} {๐“ฅ} {X} {Y} i j = invertibility-gives-โ‰ƒ f (g , ฮท , ฮต)
   where
    f : X โ†’ Y
    f x = center Y j

    g : Y โ†’ X
    g y = center X i

    ฮท : (x : X) โ†’ g (f x) โ‰ก x
    ฮท = centrality X i

    ฮต : (y : Y) โ†’ f (g y) โ‰ก y
    ฮต = centrality Y j

maps-of-singletons-are-equivs = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
      โ†’ is-singleton X โ†’ is-singleton Y โ†’ is-equiv f

  sol {๐“ค} {๐“ฅ} {X} {Y} f i j = invertibles-are-equivs f (g , ฮท , ฮต)
   where
    g : Y โ†’ X
    g y = center X i

    ฮท : (x : X) โ†’ g (f x) โ‰ก x
    ฮท = centrality X i

    ฮต : (y : Y) โ†’ f (g y) โ‰ก y
    ฮต y = singletons-are-subsingletons Y j (f (g y)) y

logically-equivalent-subsingletons-are-equivalent = sol
 where
  sol : (X : ๐“ค ฬ‡ ) (Y : ๐“ฅ ฬ‡ )
      โ†’ is-subsingleton X โ†’ is-subsingleton Y โ†’ X โ‡” Y โ†’ X โ‰ƒ Y
  sol  X Y i j (f , g) = invertibility-gives-โ‰ƒ f
                          (g ,
                           (ฮป x โ†’ i (g (f x)) x) ,
                           (ฮป y โ†’ j (f (g y)) y))

singletons-are-equivalent = sol
 where
  sol : (X : ๐“ค ฬ‡ ) (Y : ๐“ฅ ฬ‡ )
      โ†’ is-singleton X โ†’ is-singleton Y โ†’ X โ‰ƒ Y
  sol  X Y i j = invertibility-gives-โ‰ƒ (ฮป _ โ†’ center Y j)
                  ((ฮป _ โ†’ center X i) ,
                   centrality X i ,
                   centrality Y j)

Natฮฃ-fiber-equiv = sol
 where
  sol : {X : ๐“ค ฬ‡ } (A : X โ†’ ๐“ฅ ฬ‡ ) (B : X โ†’ ๐“ฆ ฬ‡ ) (ฯ† : Nat A B)
        (x : X) (b : B x)
      โ†’ fiber (ฯ† x) b โ‰ƒ fiber (Natฮฃ ฯ†) (x , b)
  sol A B ฯ† x b = invertibility-gives-โ‰ƒ f (g , ฮต , ฮท)
   where
    f : fiber (ฯ† x) b โ†’ fiber (Natฮฃ ฯ†) (x , b)
    f (a , refl _) = ((x , a) , refl (x , ฯ† x a))

    g : fiber (Natฮฃ ฯ†) (x , b) โ†’ fiber (ฯ† x) b
    g ((x , a) , refl _) = (a , refl (ฯ† x a))

    ฮต : (w : fiber (ฯ† x) b) โ†’ g (f w) โ‰ก w
    ฮต (a , refl _) = refl (a , refl (ฯ† x a))

    ฮท : (t : fiber (Natฮฃ ฯ†) (x , b)) โ†’ f (g t) โ‰ก t
    ฮท ((x , a) , refl _) = refl ((x , a) , refl (Natฮฃ ฯ† (x , a)))

Natฮฃ-equiv-gives-fiberwise-equiv = sol
 where
  sol : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ } {B : X โ†’ ๐“ฆ ฬ‡ } (ฯ† : Nat A B)
      โ†’ is-equiv (Natฮฃ ฯ†) โ†’ ((x : X) โ†’ is-equiv (ฯ† x))
  sol {๐“ค} {๐“ฅ} {๐“ฆ} {X} {A} {B} ฯ† e x b = ฮณ
   where
    d : fiber (ฯ† x) b โ‰ƒ fiber (Natฮฃ ฯ†) (x , b)
    d = Natฮฃ-fiber-equiv A B ฯ† x b

    s : is-singleton (fiber (Natฮฃ ฯ†) (x , b))
    s = e (x , b)

    ฮณ : is-singleton (fiber (ฯ† x) b)
    ฮณ = equiv-to-singleton d s

ฮฃ-is-subsingleton = sol
 where
  sol : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ }
      โ†’ is-subsingleton X
      โ†’ ((x : X) โ†’ is-subsingleton (A x))
      โ†’ is-subsingleton (ฮฃ A)
  sol i j (x , _) (y , _) = to-subtype-โ‰ก j (i x y)

ร—-is-singleton = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
      โ†’ is-singleton X
      โ†’ is-singleton Y
      โ†’ is-singleton (X ร— Y)
  sol (x , ฯ†) (y , ฮณ) = (x , y) , ฮด
   where
    ฮด : โˆ€ z โ†’ (x , y) โ‰ก z
    ฮด (x' , y' ) = to-ร—-โ‰ก (ฯ† x' , ฮณ y')

ร—-is-subsingleton = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
      โ†’ is-subsingleton X โ†’ is-subsingleton Y โ†’ is-subsingleton (X ร— Y)
  sol i j = ฮฃ-is-subsingleton i (ฮป _ โ†’ j)

ร—-is-subsingleton' = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
      โ†’ ((Y โ†’ is-subsingleton X) ร— (X โ†’ is-subsingleton Y))
      โ†’ is-subsingleton (X ร— Y)
  sol {๐“ค} {๐“ฅ} {X} {Y} (i , j) = k
   where
    k : is-subsingleton (X ร— Y)
    k (x , y) (x' , y') = to-ร—-โ‰ก (i y x x' , j x y y')

ร—-is-subsingleton'-back = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
      โ†’ is-subsingleton (X ร— Y)
      โ†’ (Y โ†’ is-subsingleton X) ร— (X โ†’ is-subsingleton Y)
  sol {๐“ค} {๐“ฅ} {X} {Y} k = i , j
   where
    i : Y โ†’ is-subsingleton X
    i y x x' = ap prโ‚ (k (x , y) (x' , y))

    j : X โ†’ is-subsingleton Y
    j x y y' = ap prโ‚‚ (k (x , y) (x , y'))

apโ‚‚ = sol
 where
  sol : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {Z : ๐“ฆ ฬ‡ } (f : X โ†’ Y โ†’ Z) {x x' : X} {y y' : Y}
      โ†’ x โ‰ก x' โ†’ y โ‰ก y' โ†’ f x y โ‰ก f x' y'
  sol f (refl x) (refl y) = refl (f x y)

equiv-singleton-lemma : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ } (x : X)
                        (f : (y : X) โ†’ x โ‰ก y โ†’ A y)
                      โ†’ ((y : X) โ†’ is-equiv (f y))
                      โ†’ is-singleton (ฮฃ A)

equiv-singleton-lemma {๐“ค} {๐“ฅ} {X} {A} x f i = ฮณ
 where
  abstract
   e : (y : X) โ†’ (x โ‰ก y) โ‰ƒ A y
   e y = (f y , i y)

   d : singleton-type' x โ‰ƒ ฮฃ A
   d = ฮฃ-cong e

   ฮณ : is-singleton (ฮฃ A)
   ฮณ = equiv-to-singleton (โ‰ƒ-sym d) (singleton-types'-are-singletons X x)

singleton-equiv-lemma : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ } (x : X)
                        (f : (y : X) โ†’ x โ‰ก y โ†’ A y)
                      โ†’ is-singleton (ฮฃ A)
                      โ†’ (y : X) โ†’ is-equiv (f y)

singleton-equiv-lemma {๐“ค} {๐“ฅ} {X} {A} x f i = ฮณ
 where
  abstract
   g : singleton-type' x โ†’ ฮฃ A
   g = Natฮฃ f

   e : is-equiv g
   e = maps-of-singletons-are-equivs g (singleton-types'-are-singletons X x) i

   ฮณ : (y : X) โ†’ is-equiv (f y)
   ฮณ = Natฮฃ-equiv-gives-fiberwise-equiv f e

univalenceโ‡’ : is-univalent ๐“ค
            โ†’ (X : ๐“ค ฬ‡ ) โ†’ is-singleton (ฮฃ Y ๊ž‰ ๐“ค ฬ‡ , X โ‰ƒ Y)

univalenceโ‡’ ua X = equiv-singleton-lemma X (Idโ†’Eq X) (ua X)

โ‡’univalence : ((X : ๐“ค ฬ‡ ) โ†’ is-singleton (ฮฃ Y ๊ž‰ ๐“ค ฬ‡ , X โ‰ƒ Y))
            โ†’ is-univalent ๐“ค

โ‡’univalence i X = singleton-equiv-lemma X (Idโ†’Eq X) (i X)

univalenceโ†’ : is-univalent ๐“ค
            โ†’ (X : ๐“ค ฬ‡ ) โ†’ is-subsingleton (ฮฃ Y ๊ž‰ ๐“ค ฬ‡ , X โ‰ƒ Y)

univalenceโ†’ ua X = singletons-are-subsingletons
                    (ฮฃ (X โ‰ƒ_)) (univalenceโ‡’ ua X)

โ†’univalence : ((X : ๐“ค ฬ‡ ) โ†’ is-subsingleton (ฮฃ Y ๊ž‰ ๐“ค ฬ‡ , X โ‰ƒ Y))
            โ†’ is-univalent ๐“ค

โ†’univalence i = โ‡’univalence (ฮป X โ†’ pointed-subsingletons-are-singletons
                                    (ฮฃ (X โ‰ƒ_)) (X , id-โ‰ƒ X) (i X))

๐”พ-โ‰ƒ : is-univalent ๐“ค
    โ†’ (X : ๐“ค ฬ‡ ) (A : (ฮฃ Y ๊ž‰ ๐“ค ฬ‡ , X โ‰ƒ Y) โ†’ ๐“ฅ ฬ‡ )
    โ†’ A (X , id-โ‰ƒ X) โ†’ (Y : ๐“ค ฬ‡ ) (e : X โ‰ƒ Y) โ†’ A (Y , e)

๐”พ-โ‰ƒ {๐“ค} ua X A a Y e = transport A p a
 where
  t : ฮฃ Y ๊ž‰ ๐“ค ฬ‡ , X โ‰ƒ Y
  t = (X , id-โ‰ƒ X)

  p : t โ‰ก (Y , e)
  p = univalenceโ†’ {๐“ค} ua X t (Y , e)

๐”พ-โ‰ƒ-equation : (ua : is-univalent ๐“ค)
             โ†’ (X : ๐“ค ฬ‡ ) (A : (ฮฃ Y ๊ž‰ ๐“ค ฬ‡ , X โ‰ƒ Y) โ†’ ๐“ฅ ฬ‡ ) (a : A (X , id-โ‰ƒ X))
             โ†’ ๐”พ-โ‰ƒ ua X A a X (id-โ‰ƒ X) โ‰ก a

๐”พ-โ‰ƒ-equation {๐“ค} {๐“ฅ} ua X A a =

  ๐”พ-โ‰ƒ ua X A a X (id-โ‰ƒ X) โ‰กโŸจ refl _                       โŸฉ
  transport A p a         โ‰กโŸจ ap (ฮป - โ†’ transport A - a) q โŸฉ
  transport A (refl t) a  โ‰กโŸจ refl _                       โŸฉ
  a                       โˆŽ

 where
  t : ฮฃ Y ๊ž‰ ๐“ค ฬ‡ , X โ‰ƒ Y
  t = (X , id-โ‰ƒ X)

  p : t โ‰ก t
  p = univalenceโ†’ {๐“ค} ua X t t

  q : p โ‰ก refl t
  q = subsingletons-are-sets (ฮฃ Y ๊ž‰ ๐“ค ฬ‡ , X โ‰ƒ Y)
       (univalenceโ†’ {๐“ค} ua X) t t p (refl t)

โ„-โ‰ƒ : is-univalent ๐“ค
    โ†’ (X : ๐“ค ฬ‡ ) (A : (Y : ๐“ค ฬ‡ ) โ†’ X โ‰ƒ Y โ†’ ๐“ฅ ฬ‡ )
    โ†’ A X (id-โ‰ƒ X) โ†’ (Y : ๐“ค ฬ‡ ) (e : X โ‰ƒ Y) โ†’ A Y e

โ„-โ‰ƒ ua X A = ๐”พ-โ‰ƒ ua X (ฮฃ-induction A)

โ„-โ‰ƒ-equation : (ua : is-univalent ๐“ค)
             โ†’ (X : ๐“ค ฬ‡ ) (A : (Y : ๐“ค ฬ‡ ) โ†’ X โ‰ƒ Y โ†’ ๐“ฅ ฬ‡ ) (a : A X  (id-โ‰ƒ X))
             โ†’ โ„-โ‰ƒ ua X A a X (