{-# 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 (