text:
------------------------------------------------------------------------
-- Conatural numbers
------------------------------------------------------------------------

{-# OPTIONS --without-K --sized-types #-}

open import Equality

module Conat {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where

open Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude hiding (_+_; _∸_; _*_)
open import Prelude.Size

open import Function-universe eq hiding (_∘_)
open import Nat eq as Nat using (_≤_)

------------------------------------------------------------------------
-- The type

-- Conats.

mutual

  data Conat (i : Size) : Type where
    zero : Conat i
    suc  : Conat′ i → Conat i

  record Conat′ (i : Size) : Type where
    coinductive
    field
      force : {j : Size< i} → Conat j

open Conat′ public

------------------------------------------------------------------------
-- Bisimilarity

-- Bisimilarity is only defined for fully defined conatural numbers
-- (of size ∞).

mutual

  infix 4 [_]_∼_ [_]_∼′_

  data [_]_∼_ (i : Size) : Conat ∞ → Conat ∞ → Type where
    zero : [ i ] zero ∼ zero
    suc  : ∀ {m n} → [ i ] force m ∼′ force n → [ i ] suc m ∼ suc n

  record [_]_∼′_ (i : Size) (m n : Conat ∞) : Type where
    coinductive
    field
      force : {j : Size< i} → [ j ] m ∼ n

open [_]_∼′_ public

-- Bisimilarity is an equivalence relation.

reflexive-∼ : ∀ {i} n → [ i ] n ∼ n
reflexive-∼ zero    = zero
reflexive-∼ (suc n) = suc λ { .force → reflexive-∼ (force n) }

symmetric-∼ : ∀ {i m n} → [ i ] m ∼ n → [ i ] n ∼ m
symmetric-∼ zero    = zero
symmetric-∼ (suc p) = suc λ { .force → symmetric-∼ (force p) }

transitive-∼ : ∀ {i m n o} → [ i ] m ∼ n → [ i ] n ∼ o → [ i ] m ∼ o
transitive-∼ zero    zero    = zero
transitive-∼ (suc p) (suc q) =
  suc λ { .force → transitive-∼ (force p) (force q) }

-- Equational reasoning combinators.

infix  -1 finally-∼ _∎∼
infixr -2 step-∼ step-≡∼ _≡⟨⟩∼_

_∎∼ : ∀ {i} n → [ i ] n ∼ n
_∎∼ = reflexive-∼

-- For an explanation of why step-∼ is defined in this way, see
-- Equality.step-≡.

step-∼ : ∀ {i} m {n o} → [ i ] n ∼ o → [ i ] m ∼ n → [ i ] m ∼ o
step-∼ _ n∼o m∼n = transitive-∼ m∼n n∼o

syntax step-∼ m n∼o m∼n = m ∼⟨ m∼n ⟩ n∼o

step-≡∼ : ∀ {i} m {n o} → [ i ] n ∼ o → m ≡ n → [ i ] m ∼ o
step-≡∼ {i} _ n∼o m≡n = subst ([ i ]_∼ _) (sym m≡n) n∼o

syntax step-≡∼ m n∼o m≡n = m ≡⟨ m≡n ⟩∼ n∼o

_≡⟨⟩∼_ : ∀ {i} m {n} → [ i ] m ∼ n → [ i ] m ∼ n
_ ≡⟨⟩∼ m∼n = m∼n

finally-∼ : ∀ {i} m n → [ i ] m ∼ n → [ i ] m ∼ n
finally-∼ _ _ m∼n = m∼n

syntax finally-∼ m n m∼n = m ∼⟨ m∼n ⟩∎ n ∎∼

------------------------------------------------------------------------
-- Some operations

-- The largest conatural number.

infinity : ∀ {i} → Conat i
infinity = suc λ { .force → infinity }

mutual

  -- Turns natural numbers into conatural numbers.

  ⌜_⌝ : ∀ {i} → ℕ → Conat i
  ⌜ zero  ⌝ = zero
  ⌜ suc n ⌝ = suc ⌜ n ⌝′

  ⌜_⌝′ : ∀ {i} → ℕ → Conat′ i
  force ⌜ n ⌝′ = ⌜ n ⌝

-- ⌜_⌝ maps equal numbers to bisimilar numbers.

⌜⌝-cong : ∀ {i m n} → m ≡ n → [ i ] ⌜ m ⌝ ∼ ⌜ n ⌝
⌜⌝-cong {m = m} {n} m≡n =
  ⌜ m ⌝  ≡⟨ cong ⌜_⌝ m≡n ⟩∼
  ⌜ n ⌝  ∎∼

-- Truncated predecessor.

pred : ∀ {i} {j : Size< i} → Conat i → Conat j
pred zero    = zero
pred (suc n) = force n

-- The pred function preserves bisimilarity.

pred-cong :
  ∀ {n₁ n₂ i} {j : Size< i} →
  [ i ] n₁ ∼ n₂ → [ j ] pred n₁ ∼ pred n₂
pred-cong zero    = zero
pred-cong (suc p) = force p

-- ⌜_⌝ is homomorphic with respect to pred.

⌜⌝-pred : ∀ n {i} → [ i ] ⌜ Nat.pred n ⌝ ∼ pred ⌜ n ⌝
⌜⌝-pred zero    = zero   ∎∼
⌜⌝-pred (suc n) = ⌜ n ⌝  ∎∼

-- Addition.

infixl 6 _+_

_+_ : ∀ {i} → Conat i → Conat i → Conat i
zero  + n = n
suc m + n = suc λ { .force → force m + n }

-- Zero is a left and right identity of addition (up to bisimilarity).

+-left-identity : ∀ {i} n → [ i ] zero + n ∼ n
+-left-identity = reflexive-∼

+-right-identity : ∀ {i} n → [ i ] n + zero ∼ n
+-right-identity zero    = zero
+-right-identity (suc n) = suc λ { .force → +-right-identity (force n) }

-- Infinity is a left and right zero of addition (up to bisimilarity).

+-left-zero : ∀ {i n} → [ i ] infinity + n ∼ infinity
+-left-zero = suc λ { .force → +-left-zero }

+-right-zero : ∀ {i} n → [ i ] n + infinity ∼ infinity
+-right-zero zero    = reflexive-∼ _
+-right-zero (suc n) = suc λ { .force → +-right-zero (force n) }

-- Addition is associative.

+-assoc : ∀ m {n o i} → [ i ] m + (n + o) ∼ (m + n) + o
+-assoc zero    = reflexive-∼ _
+-assoc (suc m) = suc λ { .force → +-assoc (force m) }

mutual

  -- The successor constructor can be moved from one side of _+_ to the
  -- other.

  suc+∼+suc : ∀ {m n i} → [ i ] suc m + force n ∼ force m + suc n
  suc+∼+suc {m} {n} =
    suc m + force n            ∼⟨ (suc λ { .force → reflexive-∼ _ }) ⟩
    ⌜ 1 ⌝ + force m + force n  ∼⟨ 1++∼+suc _ ⟩∎
    force m + suc n            ∎∼

  1++∼+suc : ∀ m {n i} → [ i ] ⌜ 1 ⌝ + m + force n ∼ m + suc n
  1++∼+suc zero    = suc λ { .force → reflexive-∼ _ }
  1++∼+suc (suc _) = suc λ { .force → suc+∼+suc }

-- Addition is commutative.

+-comm : ∀ m {n i} → [ i ] m + n ∼ n + m
+-comm zero {n} =
  zero + n  ∼⟨ symmetric-∼ (+-right-identity _) ⟩∎
  n + zero  ∎∼
+-comm (suc m) {n} =
  suc m + n            ∼⟨ (suc λ { .force → +-comm (force m) }) ⟩
  ⌜ 1 ⌝ + n + force m  ∼⟨ 1++∼+suc _ ⟩∎
  n + suc m            ∎∼

-- Addition preserves bisimilarity.

infixl 6 _+-cong_

_+-cong_ :
  ∀ {i m₁ m₂ n₁ n₂} →
  [ i ] m₁ ∼ m₂ → [ i ] n₁ ∼ n₂ → [ i ] m₁ + n₁ ∼ m₂ + n₂
zero  +-cong q = q
suc p +-cong q = suc λ { .force → force p +-cong q }

-- ⌜_⌝ is homomorphic with respect to addition.

⌜⌝-+ : ∀ m {n i} → [ i ] ⌜ m Prelude.+ n ⌝ ∼ ⌜ m ⌝ + ⌜ n ⌝
⌜⌝-+ zero    = reflexive-∼ _
⌜⌝-+ (suc m) = suc λ { .force → ⌜⌝-+ m }

-- Truncated subtraction of a natural number.

infixl 6 _∸_

_∸_ : Conat ∞ → ℕ → Conat ∞
m     ∸ zero  = m
zero  ∸ suc n = zero
suc m ∸ suc n = force m ∸ n

-- Infinity is a left zero of _∸_ (up to bisimilarity).

∸-left-zero-infinity : ∀ {i} n → [ i ] infinity ∸ n ∼ infinity
∸-left-zero-infinity zero    = reflexive-∼ _
∸-left-zero-infinity (suc n) = ∸-left-zero-infinity n

-- Zero is a left zero of _∸_ (up to bisimilarity).

∸-left-zero-zero : ∀ {i} n → [ i ] zero ∸ n ∼ zero
∸-left-zero-zero zero    = reflexive-∼ _
∸-left-zero-zero (suc n) = reflexive-∼ _

-- Zero is a right identity of subtraction (up to bisimilarity).

∸-right-identity : ∀ {i} n → [ i ] n ∸ zero ∼ n
∸-right-identity = reflexive-∼

-- Subtraction preserves bisimilarity and equality.

infixl 6 _∸-cong_

_∸-cong_ :
  ∀ {i m₁ m₂ n₁ n₂} →
  [ ∞ ] m₁ ∼ m₂ → n₁ ≡ n₂ → [ i ] m₁ ∸ n₁ ∼ m₂ ∸ n₂
_∸-cong_ {m₁ = m₁} {m₂} {zero} {n₂} p eq =
  m₁         ∼⟨ p ⟩
  m₂         ≡⟨⟩∼
  m₂ ∸ zero  ≡⟨ cong (_ ∸_) eq ⟩∼
  m₂ ∸ n₂    ∎∼

_∸-cong_ {n₁ = suc n₁} {n₂} zero eq =
  zero           ≡⟨⟩∼
  zero ∸ suc n₁  ≡⟨ cong (_ ∸_) eq ⟩∼
  zero ∸ n₂      ∎∼

_∸-cong_ {n₁ = suc n₁} {n₂} (suc {m = m₁} {n = m₂} p) eq =
  force m₁ ∸ n₁    ∼⟨ force p ∸-cong refl n₁ ⟩
  force m₂ ∸ n₁    ≡⟨⟩∼
  suc m₂ ∸ suc n₁  ≡⟨ cong (_ ∸_) eq ⟩∼
  suc m₂ ∸ n₂      ∎∼

-- ⌜_⌝ is homomorphic with respect to subtraction.

⌜⌝-∸ : ∀ m n {i} → [ i ] ⌜ m Prelude.∸ n ⌝ ∼ ⌜ m ⌝ ∸ n
⌜⌝-∸ m       zero    = reflexive-∼ _
⌜⌝-∸ zero    (suc n) = reflexive-∼ _
⌜⌝-∸ (suc m) (suc n) = ⌜⌝-∸ m n

-- Multiplication.

infixl 7 _*_

_*_ : ∀ {i} → Conat i → Conat i → Conat i
zero  * n     = zero
m     * zero  = zero
suc m * suc n = suc λ { .force → n .force + m .force * suc n }

-- One is a left and right identity of multiplication (up to
-- bisimilarity).

*-left-identity : ∀ {i} n → [ i ] ⌜ 1 ⌝ * n ∼ n
*-left-identity zero    = reflexive-∼ _
*-left-identity (suc n) = suc λ { .force →
  n .force + zero  ∼⟨ +-right-identity _ ⟩
  n .force         ∎∼ }

*-right-identity : ∀ {i} n → [ i ] n * ⌜ 1 ⌝ ∼ n
*-right-identity zero    = reflexive-∼ _
*-right-identity (suc n) = suc λ { .force → *-right-identity _ }

-- Zero is a left and right zero of multiplication (up to
-- bisimilarity).

*-left-zero : ∀ {i n} → [ i ] zero * n ∼ zero
*-left-zero = reflexive-∼ _

*-right-zero : ∀ {i n} → [ i ] n * zero ∼ zero
*-right-zero {n = zero}  = reflexive-∼ _
*-right-zero {n = suc n} = reflexive-∼ _

-- An unfolding lemma for multiplication.

suc*∼+* : ∀ {m n i} → [ i ] suc m * n ∼ n + m .force * n
suc*∼+* {m} {zero}  =
  zero             ∼⟨ symmetric-∼ *-right-zero ⟩
  m .force * zero  ∎∼
suc*∼+* {m} {suc n} = suc λ { .force → reflexive-∼ _ }

-- Multiplication distributes over addition.

*-+-distribˡ : ∀ m {n o i} → [ i ] m * (n + o) ∼ m * n + m * o
*-+-distribˡ zero                = reflexive-∼ _
*-+-distribˡ (suc m) {zero}  {o} = reflexive-∼ _
*-+-distribˡ (suc m) {suc n} {o} = suc λ { .force →
  n .force + o + m .force * (suc n + o)               ∼⟨ (_ ∎∼) +-cong *-+-distribˡ (m .force) ⟩
  n .force + o + (m .force * suc n + m .force * o)    ∼⟨ symmetric-∼ (+-assoc (n .force)) ⟩
  n .force + (o + (m .force * suc n + m .force * o))  ∼⟨ (n .force ∎∼) +-cong +-assoc o ⟩
  n .force + ((o + m .force * suc n) + m .force * o)  ∼⟨ (n .force ∎∼) +-cong (+-comm o +-cong (_ ∎∼)) ⟩
  n .force + ((m .force * suc n + o) + m .force * o)  ∼⟨ (n .force ∎∼) +-cong symmetric-∼ (+-assoc (m .force * _)) ⟩
  n .force + (m .force * suc n + (o + m .force * o))  ∼⟨ +-assoc (n .force) ⟩
  n .force + m .force * suc n + (o + m .force * o)    ∼⟨ (n .force + _ ∎∼) +-cong symmetric-∼ suc*∼+* ⟩
  n .force + m .force * suc n + suc m * o             ∎∼ }

*-+-distribʳ : ∀ m {n o i} → [ i ] (m + n) * o ∼ m * o + n * o
*-+-distribʳ zero               = reflexive-∼ _
*-+-distribʳ (suc m) {n} {zero} =
  zero      ∼⟨ symmetric-∼ *-right-zero ⟩
  n * zero  ∎∼
*-+-distribʳ (suc m) {n} {suc o} = suc λ { .force →
  o .force + (m .force + n) * suc o          ∼⟨ (_ ∎∼) +-cong *-+-distribʳ (m .force) ⟩
  o .force + (m .force * suc o + n * suc o)  ∼⟨ +-assoc (o .force) ⟩
  o .force + m .force * suc o + n * suc o    ∎∼ }

-- Multiplication is associative.

*-assoc : ∀ m {n o i} → [ i ] m * (n * o) ∼ (m * n) * o
*-assoc zero                    = reflexive-∼ _
*-assoc (suc m) {zero}          = reflexive-∼ _
*-assoc (suc m) {suc n} {zero}  = reflexive-∼ _
*-assoc (suc m) {suc n} {suc o} = suc λ { .force →
  o .force + n .force * suc o + m .force * (suc n * suc o)    ∼⟨ symmetric-∼ (+-assoc (o .force)) ⟩
  o .force + (n .force * suc o + m .force * (suc n * suc o))  ∼⟨ (o .force ∎∼) +-cong ((_ ∎∼) +-cong *-assoc (m .force)) ⟩
  o .force + (n .force * suc o + (m .force * suc n) * suc o)  ∼⟨ (o .force ∎∼) +-cong symmetric-∼ (*-+-distribʳ (n .force)) ⟩
  o .force + (n .force + m .force * suc n) * suc o            ∎∼ }

-- Multiplication is commutative.

*-comm : ∀ m {n i} → [ i ] m * n ∼ n * m
*-comm zero {n} =
  zero      ∼⟨ symmetric-∼ *-right-zero ⟩
  n * zero  ∎∼
*-comm (suc m) {zero}  = reflexive-∼ _
*-comm (suc m) {suc n} = suc λ { .force →
  n .force + m .force * suc n                  ∼⟨ (_ ∎∼) +-cong *-comm (m .force) ⟩
  n .force + suc n * m .force                  ∼⟨ (n .force ∎∼) +-cong suc*∼+* ⟩
  n .force + (m .force + n .force * m .force)  ∼⟨ +-assoc (n .force) ⟩
  (n .force + m .force) + n .force * m .force  ∼⟨ +-comm (n .force) +-cong *-comm _ ⟩
  (m .force + n .force) + m .force * n .force  ∼⟨ symmetric-∼ (+-assoc (m .force)) ⟩
  m .force + (n .force + m .force * n .force)  ∼⟨ (m .force ∎∼) +-cong symmetric-∼ suc*∼+* ⟩
  m .force + suc m * n .force                  ∼⟨ (m .force ∎∼) +-cong *-comm (suc m) ⟩
  m .force + n .force * suc m                  ∎∼ }

-- An unfolding lemma for multiplication.

*suc∼+* : ∀ {m n i} → [ i ] m * suc n ∼ m + m * n .force
*suc∼+* {m} {n} =
  m * suc n         ∼⟨ *-comm _ ⟩
  suc n * m         ∼⟨ suc*∼+* ⟩
  m + n .force * m  ∼⟨ (_ ∎∼) +-cong *-comm (n .force) ⟩
  m + m * n .force  ∎∼

-- Multiplication preserves bisimilarity.

infixl 7 _*-cong_

_*-cong_ :
  ∀ {i m₁ m₂ n₁ n₂} →
  [ i ] m₁ ∼ m₂ → [ i ] n₁ ∼ n₂ → [ i ] m₁ * n₁ ∼ m₂ * n₂
zero  *-cong _     = zero
suc p *-cong zero  = zero
suc p *-cong suc q = suc λ { .force →
  q .force +-cong p .force *-cong suc q }

-- ⌜_⌝ is homomorphic with respect to multiplication.

⌜⌝-* : ∀ m {n i} → [ i ] ⌜ m Prelude.* n ⌝ ∼ ⌜ m ⌝ * ⌜ n ⌝
⌜⌝-* zero        = reflexive-∼ _
⌜⌝-* (suc m) {n} =
  ⌜ n Prelude.+ m Prelude.* n ⌝  ∼⟨ ⌜⌝-+ n ⟩
  ⌜ n ⌝ + ⌜ m Prelude.* n ⌝      ∼⟨ reflexive-∼ _ +-cong ⌜⌝-* m ⟩
  ⌜ n ⌝ + ⌜ m ⌝ * ⌜ n ⌝          ∼⟨ symmetric-∼ suc*∼+* ⟩
  ⌜ suc m ⌝ * ⌜ n ⌝              ∎∼

------------------------------------------------------------------------
-- Ordering

-- [ ∞ ] m ≤ n means that m is less than or equal to n.

mutual

  infix 4 [_]_≤_ [_]_≤′_

  data [_]_≤_ (i : Size) : Conat ∞ → Conat ∞ → Type where
    zero : ∀ {n} → [ i ] zero ≤ n
    suc  : ∀ {m n} → [ i ] force m ≤′ force n → [ i ] suc m ≤ suc n

  record [_]_≤′_ (i : Size) (m n : Conat ∞) : Type where
    coinductive
    field
      force : {j : Size< i} → [ j ] m ≤ n

open [_]_≤′_ public

-- [ ∞ ] m < n means that m is less than n (if n is finite).

infix 4 [_]_<_

[_]_<_ : Size → Conat′ ∞ → Conat ∞ → Type
[ i ] m < n = [ i ] suc m ≤ n

-- Every conatural number is less than or equal to infinity.

infix 4 _≤infinity

_≤infinity : ∀ {i} n → [ i ] n ≤ infinity
zero  ≤infinity = zero
suc n ≤infinity = suc λ { .force → force n ≤infinity }

-- No natural number is greater than or equal to infinity.

infinity≰⌜⌝ : ∀ n → ¬ [ ∞ ] infinity ≤ ⌜ n ⌝
infinity≰⌜⌝ zero    ()
infinity≰⌜⌝ (suc n) (suc p) = infinity≰⌜⌝ n (force p)

-- No number is less than zero.

≮0 : ∀ {n i} → ¬ [ i ] n < zero
≮0 ()

-- If a number is not bounded from above by any natural number, then
-- it is bisimilar to infinity.

¬≤⌜⌝→∼∞ : ∀ {i} m → (∀ n → ¬ [ ∞ ] m ≤ ⌜ n ⌝) → [ i ] m ∼ infinity
¬≤⌜⌝→∼∞ zero    zero≰ = ⊥-elim (zero≰ 0 zero)
¬≤⌜⌝→∼∞ (suc m) hyp   =
  suc λ { .force →
    ¬≤⌜⌝→∼∞ (force m) λ n →
      [ ∞ ] force m ≤ ⌜ n ⌝    ↝⟨ (λ p → suc λ { .force → p }) ⟩
      [ ∞ ] suc m ≤ ⌜ suc n ⌝  ↝⟨ hyp (suc n) ⟩□
      ⊥                        □ }

-- The ordering relation is a partial order (with respect to
-- bisimilarity).

reflexive-≤ : ∀ {i} n → [ i ] n ≤ n
reflexive-≤ zero    = zero
reflexive-≤ (suc n) = suc λ { .force → reflexive-≤ (force n) }

transitive-≤ : ∀ {i m n o} → [ i ] m ≤ n → [ i ] n ≤ o → [ i ] m ≤ o
transitive-≤ zero    _       = zero
transitive-≤ (suc p) (suc q) =
  suc λ { .force → transitive-≤ (force p) (force q) }

antisymmetric-≤ : ∀ {i m n} → [ i ] m ≤ n → [ i ] n ≤ m → [ i ] m ∼ n
antisymmetric-≤ zero    zero    = zero
antisymmetric-≤ (suc p) (suc q) =
  suc λ { .force → antisymmetric-≤ (force p) (force q) }

-- Bisimilarity is contained in the ordering relation.

∼→≤ : ∀ {i m n} → [ i ] m ∼ n → [ i ] m ≤ n
∼→≤ zero    = zero
∼→≤ (suc p) = suc λ { .force → ∼→≤ (force p) }

-- "Equational" reasoning combinators.

infix  -1 finally-≤ _∎≤
infixr -2 step-≤ step-∼≤ _≡⟨⟩≤_

_∎≤ : ∀ {i} n → [ i ] n ≤ n
_∎≤ = reflexive-≤

step-≤ : ∀ {i} m {n o} → [ i ] n ≤ o → [ i ] m ≤ n → [ i ] m ≤ o
step-≤ _ n≤o m≤n = transitive-≤ m≤n n≤o

syntax step-≤ m n≤o m≤n = m ≤⟨ m≤n ⟩ n≤o

step-∼≤ : ∀ {i} m {n o} → [ i ] n ≤ o → [ i ] m ∼ n → [ i ] m ≤ o
step-∼≤ _ n≤o m∼n = step-≤ _ n≤o (∼→≤ m∼n)

syntax step-∼≤ m n≤o m∼n = m ∼⟨ m∼n ⟩≤ n≤o

_≡⟨⟩≤_ : ∀ {i} m {n} → [ i ] m ≤ n → [ i ] m ≤ n
_ ≡⟨⟩≤ m≤n = m≤n

finally-≤ : ∀ {i} m n → [ i ] m ≤ n → [ i ] m ≤ n
finally-≤ _ _ m≤n = m≤n

syntax finally-≤ m n m≤n = m ≤⟨ m≤n ⟩∎ n ∎≤

-- The ordering relation respects the ordering relation
-- (contravariantly in the first argument).

infix 4 _≤-cong-≤_

_≤-cong-≤_ :
  ∀ {m m′ n n′ i} →
  [ i ] m′ ≤ m → [ i ] n ≤ n′ → [ i ] m ≤ n → [ i ] m′ ≤ n′
_≤-cong-≤_ {m} {m′} {n} {n′} m≥m′ n≤n′ m≤n =
  m′  ≤⟨ m≥m′ ⟩
  m   ≤⟨ m≤n ⟩
  n   ≤⟨ n≤n′ ⟩
  n′  ∎≤

-- A kind of preservation result for bisimilarity, ordering and
-- logical equivalence.

infix 4 _≤-cong-∼_

_≤-cong-∼_ :
  ∀ {m m′ n n′ i} →
  [ i ] m ∼ m′ → [ i ] n ∼ n′ → [ i ] m ≤ n ⇔ [ i ] m′ ≤ n′
m∼m′ ≤-cong-∼ n∼n′ = record
  { to   = ∼→≤ (symmetric-∼ m∼m′) ≤-cong-≤ ∼→≤ n∼n′
  ; from = ∼→≤ m∼m′ ≤-cong-≤ ∼→≤ (symmetric-∼ n∼n′)
  }

-- Some inversion lemmas.

cancel-suc-≤ :
  ∀ {i m n} → [ i ] suc m ≤ suc n → [ i ] force m ≤′ force n
cancel-suc-≤ (suc p) = p

cancel-pred-≤ :
  ∀ {m n i} →
  [ i ] ⌜ 1 ⌝ ≤ n →
  [ i ] pred m ≤′ pred n →
  [ i ] m ≤ n
cancel-pred-≤ {zero}  (suc _) = λ _ → zero
cancel-pred-≤ {suc _} (suc _) = suc

cancel-∸-suc-≤ :
  ∀ {m n o i} →
  [ ∞ ] ⌜ o ⌝′ < n →
  [ i ] m ∸ suc o ≤′ n ∸ suc o →
  [ i ] m ∸ o ≤ n ∸ o
cancel-∸-suc-≤ {zero} {n} {o} _ _ =
  zero ∸ o  ∼⟨ ∸-left-zero-zero o ⟩≤
  zero      ≤⟨ zero ⟩∎
  n ∸ o     ∎≤
cancel-∸-suc-≤ {suc _} {_}     {zero}  (suc _)   = suc
cancel-∸-suc-≤ {suc m} {suc n} {suc o} (suc o<n) =
  cancel-∸-suc-≤ (force o<n)

-- The successor of a number is greater than or equal to the number.

≤suc : ∀ {i n} → [ i ] force n ≤ suc n
≤suc = helper _ (refl _)
  where
  helper : ∀ {i} m {n} → m ≡ force n → [ i ] m ≤ suc n
  helper zero    _    = zero
  helper (suc m) 1+m≡ = suc λ { .force {j = j} →
                          subst ([ j ] _ ≤_) 1+m≡ ≤suc }

-- If a number is less than or equal to another, then it is also less
-- than or equal to the other's successor.

≤-step : ∀ {m n i} → [ i ] m ≤′ force n → [ i ] m ≤ suc n
≤-step {zero}      _ = zero
≤-step {suc m} {n} p = suc λ { .force →
  force m  ≤⟨ ≤suc ⟩
  suc m    ≤⟨ force p ⟩∎
  force n  ∎≤ }

-- If m is less than n, then m is less than or equal to n.

<→≤ : ∀ {i m n} → [ i ] m < n → [ i ] force m ≤ n
<→≤ (suc p) = ≤-step p

-- If you add something to a number, then you get something that is
-- greater than or equal to what you started with.

m≤n+m : ∀ {i m n} → [ i ] m ≤ n + m
m≤n+m {n = zero}  = reflexive-≤ _
m≤n+m {n = suc n} = ≤-step λ { .force → m≤n+m }

m≤m+n : ∀ {m n i} → [ i ] m ≤ m + n
m≤m+n {m} {n} =
  m      ≤⟨ m≤n+m ⟩
  n + m  ≤⟨ ∼→≤ (+-comm n) ⟩∎
  m + n  ∎≤

-- A form of associativity for _∸_.

∸-∸-assoc : ∀ {m} n {k i} → [ i ] (m ∸ n) ∸ k ∼ m ∸ (n Prelude.+ k)
∸-∸-assoc         zero            = _ ∎∼
∸-∸-assoc {zero}  (suc _) {zero}  = _ ∎∼
∸-∸-assoc {zero}  (suc _) {suc _} = _ ∎∼
∸-∸-assoc {suc _} (suc n)         = ∸-∸-assoc n

-- A limited form of associativity for _+_ and _∸_.

+-∸-assoc : ∀ {m n k i} →
            [ ∞ ] ⌜ k ⌝ ≤ n → [ i ] (m + n) ∸ k ∼ m + (n ∸ k)
+-∸-assoc {m} {n} {zero} zero =
  m + n ∸ 0    ≡⟨⟩∼
  m + n        ≡⟨⟩∼
  m + (n ∸ 0)  ∎∼
+-∸-assoc {m} {suc n} {suc k} (suc k≤n) =
  m + suc n ∸ suc k            ∼⟨ symmetric-∼ (1++∼+suc m) ∸-cong refl (suc k) ⟩
  ⌜ 1 ⌝ + m + force n ∸ suc k  ≡⟨⟩∼
  m + force n ∸ k              ∼⟨ +-∸-assoc (force k≤n) ⟩
  m + (force n ∸ k)            ≡⟨⟩∼
  m + (suc n ∸ suc k)          ∎∼

-- If you subtract a number and then add it again, then you get back
-- what you started with if the number is less than or equal to the
-- number that you started with.

∸+≡ : ∀ {m n i} → [ i ] ⌜ n ⌝ ≤ m → [ i ] (m ∸ n) + ⌜ n ⌝ ∼ m
∸+≡ {m} {zero} zero =
  m + zero  ∼⟨ +-right-identity _ ⟩∎
  m         ∎∼
∸+≡ {.suc m} {suc n} (suc p) =
  force m ∸ n + ⌜ suc n ⌝        ∼⟨ symmetric-∼ (1++∼+suc _) ⟩
  ⌜ 1 ⌝ + (force m ∸ n) + ⌜ n ⌝  ∼⟨ symmetric-∼ (+-assoc ⌜ 1 ⌝) ⟩
  ⌜ 1 ⌝ + (force m ∸ n + ⌜ n ⌝)  ∼⟨ (suc λ { .force → ∸+≡ (force p) }) ⟩
  ⌜ 1 ⌝ + force m                ∼⟨ (suc λ { .force → _ ∎∼ }) ⟩∎
  suc m                          ∎∼

-- If you subtract a natural number and then add it again, then you
-- get something that is greater than or equal to what you started
-- with.

≤∸+ : ∀ m n {i} → [ i ] m ≤ (m ∸ n) + ⌜ n ⌝
≤∸+ m zero =
  m          ∼⟨ symmetric-∼ (+-right-identity _) ⟩≤
  m + ⌜ 0 ⌝  ∎≤
≤∸+ zero    (suc n) = zero
≤∸+ (suc m) (suc n) =
  suc m                          ≤⟨ (suc λ { .force → ≤∸+ (force m) n }) ⟩
  ⌜ 1 ⌝ + (force m ∸ n + ⌜ n ⌝)  ∼⟨ +-assoc ⌜ 1 ⌝ ⟩≤
  ⌜ 1 ⌝ + (force m ∸ n) + ⌜ n ⌝  ∼⟨ 1++∼+suc _ ⟩≤
  force m ∸ n + ⌜ suc n ⌝        ≡⟨⟩≤
  suc m ∸ suc n + ⌜ suc n ⌝      ∎≤

-- If you subtract something from a number you get a number that is
-- less than or equal to the one you started with.

∸≤ : ∀ {m} n {i} → [ i ] m ∸ n ≤ m
∸≤         zero    = _ ∎≤
∸≤ {zero}  (suc _) = _ ∎≤
∸≤ {suc m} (suc n) = ≤-step λ { .force → ∸≤ n }

-- Lemmas relating the ordering relation, subtraction and the
-- successor function.

∸suc≤→∸≤suc :
  ∀ {i} m n {o} →
  [ i ] m ∸ suc n ≤ force o → [ ssuc i ] m ∸ n ≤ suc o
∸suc≤→∸≤suc zero    zero    p = zero
∸suc≤→∸≤suc zero    (suc n) p = zero
∸suc≤→∸≤suc (suc m) zero    p = suc λ { .force → p }
∸suc≤→∸≤suc (suc m) (suc n) p = ∸suc≤→∸≤suc (force m) n p

∸≤suc→∸suc≤ :
  ∀ {i} {j : Size< i} m n {o} →
  [ i ] m ∸ n ≤ suc o → [ j ] m ∸ suc n ≤ force o
∸≤suc→∸suc≤ zero    zero    p       = zero
∸≤suc→∸suc≤ zero    (suc n) p       = zero
∸≤suc→∸suc≤ (suc m) zero    (suc p) = force p
∸≤suc→∸suc≤ (suc m) (suc n) p       = ∸≤suc→∸suc≤ (force m) n p

-- One can decide whether a natural number is greater than or equal
-- to, or less than, any number.

≤⌜⌝⊎>⌜⌝ : ∀ {i} m n → [ i ] m ≤ ⌜ n ⌝ ⊎ [ i ] ⌜ n ⌝′ < m
≤⌜⌝⊎>⌜⌝ zero    _       = inj₁ zero
≤⌜⌝⊎>⌜⌝ (suc m) zero    = inj₂ (suc λ { .force → zero })
≤⌜⌝⊎>⌜⌝ (suc m) (suc n) =
  ⊎-map (λ (p : [ _ ] _ ≤ _) → suc λ { .force → p })
        (λ (p : [ _ ] _ < _) → suc λ { .force → p })
        (≤⌜⌝⊎>⌜⌝ (force m) n)

-- One can decide whether a natural number is less than or equal to,
-- or greater than, any number.

⌜⌝≤⊎⌜⌝> : ∀ {i} m n → [ i ] ⌜ m ⌝ ≤ n ⊎ [ i ] ⌜ 1 ⌝ + n ≤ ⌜ m ⌝
⌜⌝≤⊎⌜⌝> zero    _       = inj₁ zero
⌜⌝≤⊎⌜⌝> (suc m) zero    = inj₂ (suc λ { .force → zero })
⌜⌝≤⊎⌜⌝> (suc m) (suc n) =
  ⊎-map (λ (p : [ _ ] _ ≤ _) → suc λ { .force → p })
        (λ p                 → suc λ { .force → suc n            ≤⟨ (suc λ { .force → _ ∎≤ }) ⟩
                                                ⌜ 1 ⌝ + force n  ≤⟨ p ⟩∎
                                                ⌜ m ⌝            ∎≤ })
        (⌜⌝≤⊎⌜⌝> m (force n))

-- ⌜_⌝ is monotone.

⌜⌝-mono : ∀ {m n i} → m ≤ n → [ i ] ⌜ m ⌝ ≤ ⌜ n ⌝
⌜⌝-mono {zero}          m≤n = zero
⌜⌝-mono {suc _} {zero}  m≤n = ⊥-elim (Nat.≮0 _ m≤n)
⌜⌝-mono {suc _} {suc _} m≤n =
  suc λ { .force → ⌜⌝-mono (Nat.suc≤suc⁻¹ m≤n) }

-- If two natural numbers are related by [ ∞ ]_≤_, then they are also
-- related by _≤_.

⌜⌝-mono⁻¹ : ∀ {m n} → [ ∞ ] ⌜ m ⌝ ≤ ⌜ n ⌝ → m ≤ n
⌜⌝-mono⁻¹ {zero}          zero      = Nat.zero≤ _
⌜⌝-mono⁻¹ {suc _} {zero}  ()
⌜⌝-mono⁻¹ {suc _} {suc _} (suc m≤n) =
  Nat.suc≤suc (⌜⌝-mono⁻¹ (force m≤n))

-- The pred function is monotone.

pred-mono : ∀ {m n} → [ ∞ ] m ≤ n → [ ∞ ] pred m ≤ pred n
pred-mono zero    = zero
pred-mono (suc p) = force p

-- Addition is monotone.

infixl 6 _+-mono_

_+-mono_ : ∀ {i m₁ m₂ n₁ n₂} →
           [ i ] m₁ ≤ m₂ → [ i ] n₁ ≤ n₂ → [ i ] m₁ + n₁ ≤ m₂ + n₂
_+-mono_ {m₁ = m₁} {m₂} {n₁} {n₂} zero q =
  zero + n₁  ≡⟨⟩≤
  n₁         ≤⟨ q ⟩
  n₂         ≤⟨ m≤n+m ⟩∎
  m₂ + n₂    ∎≤
suc p +-mono q = suc λ { .force → force p +-mono q }

-- Subtraction is monotone in its first argument and antitone in its
-- second argument.

infixl 6 _∸-mono_

_∸-mono_ : ∀ {m₁ m₂ n₁ n₂ i} →
           [ ∞ ] m₁ ≤ m₂ → n₂ ≤ n₁ → [ i ] m₁ ∸ n₁ ≤ m₂ ∸ n₂
_∸-mono_              {n₁ = zero}   {zero}  p  _ = p
_∸-mono_              {n₁ = zero}   {suc _} _  q = ⊥-elim (Nat.≮0 _ q)
_∸-mono_ {zero}       {n₁ = suc n₁}         _  _ = zero
_∸-mono_ {suc _}  {zero}   {suc _}          () _
_∸-mono_ {suc m₁} {suc m₂} {suc n₁} {zero}  p  _ = force m₁ ∸ n₁  ≤⟨ ∸≤ n₁ ⟩
                                                   force m₁       ≤⟨ ≤suc ⟩
                                                   suc m₁         ≤⟨ p ⟩∎
                                                   suc m₂         ∎≤
_∸-mono_ {suc _}  {suc _}  {suc _}  {suc _} p  q =
  force (cancel-suc-≤ p) ∸-mono Nat.suc≤suc⁻¹ q

-- Multiplication is monotone.

infixl 7 _*-mono_

_*-mono_ : ∀ {i m₁ m₂ n₁ n₂} →
           [ i ] m₁ ≤ m₂ → [ i ] n₁ ≤ n₂ → [ i ] m₁ * n₁ ≤ m₂ * n₂
zero  *-mono _     = zero
suc _ *-mono zero  = zero
suc p *-mono suc q = suc λ { .force →
  q .force +-mono p .force *-mono suc q  }

------------------------------------------------------------------------
-- Minimum and maximum

-- The smallest number.

min : ∀ {i} → Conat i → Conat i → Conat i
min zero    n       = zero
min m       zero    = zero
min (suc m) (suc n) = suc λ { .force → min (force m) (force n) }

-- The largest number.

max : ∀ {i} → Conat i → Conat i → Conat i
max zero    n = n
max (suc m) n = suc λ { .force → max (force m) (pred n) }

-- The minimum of two numbers is less than or equal to both of them.

min≤ˡ : ∀ {i} m n → [ i ] min m n ≤ m
min≤ˡ zero    _       = zero
min≤ˡ (suc _) zero    = zero
min≤ˡ (suc m) (suc n) = suc λ { .force → min≤ˡ (force m) (force n) }

min≤ʳ : ∀ {i} m n → [ i ] min m n ≤ n
min≤ʳ zero    _       = zero
min≤ʳ (suc _) zero    = zero
min≤ʳ (suc m) (suc n) = suc λ { .force → min≤ʳ (force m) (force n) }

-- The maximum of two numbers is greater than or equal to both of
-- them.

ˡ≤max : ∀ {i} m n → [ i ] m ≤ max m n
ˡ≤max zero    _ = zero
ˡ≤max (suc m) n = suc λ { .force → ˡ≤max (force m) (pred n) }

ʳ≤max : ∀ {i} m n → [ i ] n ≤ max m n
ʳ≤max zero    _       = reflexive-≤ _
ʳ≤max (suc _) zero    = zero
ʳ≤max (suc m) (suc n) = suc λ { .force → ʳ≤max (force m) (force n) }

-- The min and max functions preserve bisimilarity.

min-cong :
  ∀ {i m₁ m₂ n₁ n₂} →
  [ i ] m₁ ∼ m₂ → [ i ] n₁ ∼ n₂ → [ i ] min m₁ n₁ ∼ min m₂ n₂
min-cong zero    q       = zero
min-cong (suc p) zero    = zero
min-cong (suc p) (suc q) =
  suc λ { .force → min-cong (force p) (force q) }

max-cong :
  ∀ {i m₁ m₂ n₁ n₂} →
  [ i ] m₁ ∼ m₂ → [ i ] n₁ ∼ n₂ → [ i ] max m₁ n₁ ∼ max m₂ n₂
max-cong zero    q = q
max-cong (suc p) q =
  suc λ { .force → max-cong (force p) (pred-cong q) }

------------------------------------------------------------------------
-- Finite and infinite numbers

-- A number is finite if it is bisimilar to a natural number.

Finite : Conat ∞ → Type
Finite m = ∃ λ n → [ ∞ ] m ∼ ⌜ n ⌝

-- Numbers that are not finite are infinite.

Infinite : Conat ∞ → Type
Infinite n = ¬ Finite n

-- The value infinity is infinite.

Infinite-infinity : Infinite infinity
Infinite-infinity = uncurry λ n →
  [ ∞ ] infinity ∼ ⌜ n ⌝  ↝⟨ ∼→≤ ⟩
  [ ∞ ] infinity ≤ ⌜ n ⌝  ↝⟨ infinity≰⌜⌝ _ ⟩
  ⊥                       □

-- Infinite numbers are bisimilar to infinity.

Infinite→∼infinity : ∀ {n i} → Infinite n → [ i ] n ∼ infinity
Infinite→∼infinity {zero}  inf = ⊥-elim (inf (_ , zero))
Infinite→∼infinity {suc n} inf =
  suc λ { .force → Infinite→∼infinity (inf ∘ Σ-map suc suc′) }
  where
  suc′ : ∀ {m} → [ ∞ ] force n ∼ ⌜ m ⌝ → [ ∞ ] suc n ∼ ⌜ suc m ⌝
  suc′ p = suc λ { .force → p }

-- If m is bounded from above by some natural number, then m is
-- finite.

≤⌜⌝→Finite : ∀ {m n} → [ ∞ ] m ≤ ⌜ n ⌝ → Finite m
≤⌜⌝→Finite {.zero}  {zero}  zero      = zero , zero
≤⌜⌝→Finite {.zero}  {suc n} zero      = zero , zero
≤⌜⌝→Finite {.suc m} {suc n} (suc m≤n) =
  Σ-map suc (λ (hyp : [ _ ] _ ∼ _) → suc λ { .force → hyp })
    (≤⌜⌝→Finite (force m≤n))

------------------------------------------------------------------------
-- Functions and proofs related to addition of strictly positive
-- numbers

-- The function _⁺+_ adds two numbers, given that the first one is
-- positive. This fact allows the second number to have type Conat′ i,
-- rather than Conat i. This can be convenient in corecursive
-- definitions.

infixl 6 _⁺+_

_⁺+_ : ∀ {m i} → [ i ] ⌜ 1 ⌝ ≤ m → Conat′ i → Conat i
_⁺+_ {zero}  () _
_⁺+_ {suc m} _  n = suc λ { .force → force m + force n }

-- The definition of _⁺+_ is correct.

⁺+∼+ : ∀ {m i} (1≤m : [ ∞ ] ⌜ 1 ⌝ ≤ m) n →
       [ i ] 1≤m ⁺+ n ∼ m + force n
⁺+∼+ {zero}  () _
⁺+∼+ {suc _} _  _ = suc λ { .force → _ ∎∼ }

-- _⁺+_ preserves bisimilarity.

⁺+-cong :
  ∀ {m₁ m₂ n₁ n₂ i}
  (1≤m₁ : [ ∞ ] ⌜ 1 ⌝ ≤ m₁)
  (1≤m₂ : [ ∞ ] ⌜ 1 ⌝ ≤ m₂) →
  [ i ] m₁ ∼ m₂ →
  [ i ] force n₁ ∼′ force n₂ →
  [ i ] 1≤m₁ ⁺+ n₁ ∼ 1≤m₂ ⁺+ n₂
⁺+-cong {zero}          () _  _           _
⁺+-cong {suc _} {zero}  _  () _           _
⁺+-cong {suc _} {suc _} _  _  (suc m₁∼m₂) n₁∼n₂ =
  suc λ { .force → force m₁∼m₂ +-cong force n₁∼n₂ }

-- _⁺+_ is monotone.

⁺+-mono :
  ∀ {m₁ m₂ n₁ n₂ i}
  (1≤m₁ : [ ∞ ] ⌜ 1 ⌝ ≤ m₁)
  (1≤m₂ : [ ∞ ] ⌜ 1 ⌝ ≤ m₂) →
  [ i ] m₁ ≤ m₂ →
  [ i ] force n₁ ≤′ force n₂ →
  [ i ] 1≤m₁ ⁺+ n₁ ≤ 1≤m₂ ⁺+ n₂
⁺+-mono {zero}          () _  _           _
⁺+-mono {suc _} {zero}  _  () _           _
⁺+-mono {suc _} {suc _} _  _  (suc m₁∼m₂) n₁∼n₂ =
  suc λ { .force → force m₁∼m₂ +-mono force n₁∼n₂ }

-- Variants of _+-cong_ that can be used when one or more of the
-- numbers are known to be positive. With this information at hand it
-- suffices for some of the proofs to be "primed".

1≤+-cong :
  ∀ {m₁ m₂ n₁ n₂ i} →
  [ i ] ⌜ 1 ⌝ ≤ m₁ →
  [ i ] m₁ ∼ m₂ →
  [ i ] n₁ ∼′ n₂ →
  [ i ] m₁ + n₁ ∼ m₂ + n₂
1≤+-cong {zero}          () _           _
1≤+-cong {suc _} {zero}  _  ()          _
1≤+-cong {suc _} {suc _} _  (suc m₁∼m₂) n₁∼n₂ =
  suc λ { .force → force m₁∼m₂ +-cong force n₁∼n₂ }

+1≤-cong :
  ∀ {m₁ m₂ n₁ n₂ i} →
  [ i ] ⌜ 1 ⌝ ≤ n₁ →
  [ i ] m₁ ∼′ m₂ →
  [ i ] n₁ ∼ n₂ →
  [ i ] m₁ + n₁ ∼ m₂ + n₂
+1≤-cong {m₁} {m₂} {n₁} {n₂} 1≤n₁ m₁∼m₂ n₁∼n₂ =
  m₁ + n₁  ∼⟨ +-comm m₁ ⟩
  n₁ + m₁  ∼⟨ 1≤+-cong 1≤n₁ n₁∼n₂ m₁∼m₂ ⟩
  n₂ + m₂  ∼⟨ +-comm n₂ ⟩∎
  m₂ + n₂  ∎∼

1≤+1≤-cong :
  ∀ {m₁ m₂ n₁ n₂ i} →
  [ i ] ⌜ 1 ⌝ ≤ m₁ →
  [ i ] ⌜ 1 ⌝ ≤ n₂ →
  [ i ] m₁ ∼′ m₂ →
  [ i ] n₁ ∼′ n₂ →
  [ i ] m₁ + n₁ ∼ m₂ + n₂
1≤+1≤-cong {m₁} {m₂} {n₁} {n₂} 1≤m₁ 1≤n₂ m₁∼m₂ n₁∼n₂ =
  m₁ + n₁  ∼⟨ 1≤+-cong 1≤m₁ (_ ∎∼) n₁∼n₂ ⟩
  m₁ + n₂  ∼⟨ +1≤-cong 1≤n₂ m₁∼m₂ (_ ∎∼) ⟩∎
  m₂ + n₂  ∎∼

-- Variants of _+-mono_ that can be used when one or more of the
-- numbers are known to be positive. With this information at hand it
-- suffices for some of the proofs to be "primed".

1≤+-mono :
  ∀ {m₁ m₂ n₁ n₂ i} →
  [ i ] ⌜ 1 ⌝ ≤ m₁ →
  [ i ] m₁ ≤ m₂ →
  [ i ] n₁ ≤′ n₂ →
  [ i ] m₁ + n₁ ≤ m₂ + n₂
1≤+-mono {zero}          () _           _
1≤+-mono {suc _} {zero}  _  ()          _
1≤+-mono {suc _} {suc _} _  (suc m₁≤m₂) n₁≤n₂ =
  suc λ { .force → force m₁≤m₂ +-mono force n₁≤n₂ }

+1≤-mono :
  ∀ {m₁ m₂ n₁ n₂ i} →
  [ i ] ⌜ 1 ⌝ ≤ n₁ →
  [ i ] m₁ ≤′ m₂ →
  [ i ] n₁ ≤ n₂ →
  [ i ] m₁ + n₁ ≤ m₂ + n₂
+1≤-mono {m₁} {m₂} {n₁} {n₂} 1≤n₁ m₁≤m₂ n₁≤n₂ =
  m₁ + n₁  ∼⟨ +-comm m₁ ⟩≤
  n₁ + m₁  ≤⟨ 1≤+-mono 1≤n₁ n₁≤n₂ m₁≤m₂ ⟩
  n₂ + m₂  ∼⟨ +-comm n₂ ⟩≤
  m₂ + n₂  ∎≤

1≤+1≤-mono :
  ∀ {m₁ m₂ n₁ n₂ i} →
  [ i ] ⌜ 1 ⌝ ≤ m₁ →
  [ i ] ⌜ 1 ⌝ ≤ n₂ →
  [ i ] m₁ ≤′ m₂ →
  [ i ] n₁ ≤′ n₂ →
  [ i ] m₁ + n₁ ≤ m₂ + n₂
1≤+1≤-mono {m₁} {m₂} {n₁} {n₂} 1≤m₁ 1≤n₂ m₁≤m₂ n₁≤n₂ =
  m₁ + n₁  ≤⟨ 1≤+-mono 1≤m₁ (_ ∎≤) n₁≤n₂ ⟩
  m₁ + n₂  ≤⟨ +1≤-mono 1≤n₂ m₁≤m₂ (_ ∎≤) ⟩∎
  m₂ + n₂  ∎≤

------------------------------------------------------------------------
-- Some negative results

-- It is impossible to define a strengthening function that, for any
-- size i, takes strong bisimilarity of size i between 2 and 1 into
-- ordering of size ssuc i between 2 and 1.

no-strengthening-21 :
  ¬ (∀ {i} → [ i ] ⌜ 2 ⌝ ∼ ⌜ 1 ⌝ → [ ssuc i ] ⌜ 2 ⌝ ≤ ⌜ 1 ⌝)
no-strengthening-21 strengthen = contradiction ∞
  where
  2≁1 : ∀ i → ¬ [ i ] ⌜ 2 ⌝ ∼ ⌜ 1 ⌝
  2≁1 i =
    [ i      ] ⌜ 2 ⌝ ∼ ⌜ 1 ⌝  ↝⟨ strengthen ⟩
    [ ssuc i ] ⌜ 2 ⌝ ≤ ⌜ 1 ⌝  ↝⟨ (λ hyp → cancel-suc-≤ hyp .force) ⟩
    [ i      ] ⌜ 1 ⌝ ≤ ⌜ 0 ⌝  ↝⟨ ≮0 ⟩□
    ⊥                         □

  mutual

    2∼1 : ∀ i → [ i ] ⌜ 2 ⌝ ∼ ⌜ 1 ⌝
    2∼1 i = suc λ { .force {j} → ⊥-elim (contradiction j) }

    contradiction : Size → ⊥
    contradiction i = 2≁1 i (2∼1 i)

-- It is impossible to define a strengthening function that, for any
-- size i, takes strong bisimilarity of size i between 2 and 1 into
-- strong bisimilarity of size ssuc i between 2 and 1.

no-strengthening-∼-21 :
  ¬ (∀ {i} → [ i ] ⌜ 2 ⌝ ∼ ⌜ 1 ⌝ → [ ssuc i ] ⌜ 2 ⌝ ∼ ⌜ 1 ⌝)
no-strengthening-∼-21 =
  (∀ {i} → [ i ] ⌜ 2 ⌝ ∼ ⌜ 1 ⌝ → [ ssuc i ] ⌜ 2 ⌝ ∼ ⌜ 1 ⌝)  ↝⟨ ∼→≤ ∘_ ⟩
  (∀ {i} → [ i ] ⌜ 2 ⌝ ∼ ⌜ 1 ⌝ → [ ssuc i ] ⌜ 2 ⌝ ≤ ⌜ 1 ⌝)  ↝⟨ no-strengthening-21 ⟩□
  ⊥                                                         □

-- It is impossible to define a strengthening function that, for any
-- size i, takes ordering of size i between 2 and 1 into ordering of
-- size ssuc i between 2 and 1.

no-strengthening-≤-21 :
  ¬ (∀ {i} → [ i ] ⌜ 2 ⌝ ≤ ⌜ 1 ⌝ → [ ssuc i ] ⌜ 2 ⌝ ≤ ⌜ 1 ⌝)
no-strengthening-≤-21 =
  (∀ {i} → [ i ] ⌜ 2 ⌝ ≤ ⌜ 1 ⌝ → [ ssuc i ] ⌜ 2 ⌝ ≤ ⌜ 1 ⌝)  ↝⟨ _∘ ∼→≤ ⟩
  (∀ {i} → [ i ] ⌜ 2 ⌝ ∼ ⌜ 1 ⌝ → [ ssuc i ] ⌜ 2 ⌝ ≤ ⌜ 1 ⌝)  ↝⟨ no-strengthening-21 ⟩□
  ⊥                                                         □

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
open import Data.Product using ( ∃ ; _×_ ; _,_ ; proj₁ ; proj₂ )
open import Relation.Unary using ( _∈_ )
open import Web.Semantic.DL.ABox using ( ABox )
open import Web.Semantic.DL.ABox.Model using ( _⊨a_ ; _⊨b_ ; ⊨a-resp-≲ ; ⊨b-resp-≲ )
open import Web.Semantic.DL.ABox.Interp using ( Interp ; ⌊_⌋ ; _*_ )
open import Web.Semantic.DL.ABox.Interp.Morphism using ( _≲_ ; ≲-refl )
open import Web.Semantic.DL.KB using ( _,_ )
open import Web.Semantic.DL.KB.Model using ( _⊨_ )
open import Web.Semantic.DL.Integrity using ( Initial ; _⊕_⊨_ ; extension ; ext-init ; ext-⊨ ; ext✓ ; init-≲ ; init-⊨ ; init-med ; med-≲ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox ; _,_ )
open import Web.Semantic.DL.TBox.Model using ( _⊨t_ )
open import Web.Semantic.DL.Category.Object using ( Object ; _,_ ; IN ; iface )
open import Web.Semantic.Util using ( _⊕_⊕_ ; inode ; enode )

module Web.Semantic.DL.Category.Morphism {Σ : Signature} {S T : TBox Σ} where

infixr 4 _,_

-- A morphism A ⇒ B is an abox F such that for every I ⊨ S , T , A
-- there is a J which is the initial extension of I satisfying (S , F),
-- and moreover J satisfies (T , B).

data _⇒_w/_ (A B : Object S T) (V : Set) : Set₁ where
  _,_ : (F : ABox Σ (IN A ⊕ V ⊕ IN B)) →
    (∀ I → (I ⊨ (S , T) , iface A) → (I ⊕ (S , F) ⊨ (T , iface B))) →
      (A ⇒ B w/ V)

data _⇒_ (A B : Object S T) : Set₁ where
  _,_ : ∀ V → (A ⇒ B w/ V) → (A ⇒ B)

BN : ∀ {A B} → (F : A ⇒ B) → Set
BN (V , F,F✓) = V

impl : ∀ {A B} → (F : A ⇒ B) → ABox Σ (IN A ⊕ BN F ⊕ IN B)
impl (V , F , F✓) = F

impl✓ : ∀ {A B} → (F : A ⇒ B) → ∀ I → (I ⊨ (S , T) , iface A) → (I ⊕ (S , impl F) ⊨ (T , iface B))
impl✓ (V , F , F✓) = F✓

apply : ∀ {A B} (F : A ⇒ B) I → (I ⊨ (S , T) , iface A) →
  Interp Σ (IN A ⊕ BN F ⊕ IN B)
apply F I I⊨STA = extension (impl✓ F I I⊨STA)

apply-init : ∀ {A B} (F : A ⇒ B) I I⊨STA →
  (apply F I I⊨STA ∈ Initial I (S , impl F))
apply-init F I I⊨STA = ext-init (impl✓ F I I⊨STA)

apply-⊨ : ∀ {A B} (F : A ⇒ B) I I⊨STA →
  (enode * (apply F I I⊨STA) ⊨ (T , iface B))
apply-⊨ F I I⊨STA = ext-⊨ (impl✓ F I I⊨STA)

apply-≲ : ∀ {A B} (F : A ⇒ B) I I⊨STA → (I ⊨a impl F) →
  (apply F (inode * I) I⊨STA ≲ I)
apply-≲ F I ((I⊨S , I⊨T) , I⊨A) I⊨F =
  med-≲ (init-med
    (apply-init F (inode * I) ((I⊨S , I⊨T) , I⊨A))
    I
    (≲-refl (inode * I))
    (I⊨S , I⊨F))

apply✓ : ∀ {A B} (F : A ⇒ B) I I⊨STA →
  (enode * apply F I I⊨STA ⊨ (S , T) , iface B)
apply✓ F I I⊨STA = ext✓ (impl✓ F I I⊨STA)

-- Morphisms F and G are equivalent whenever
-- in any interpretation I ⊨ S,T
-- we have I ⊨ F iff I ⊨ G.

infix 2 _⊑_ _⊑′_ _≣_

_⊑_ : ∀ {A B : Object S T} → (A ⇒ B) → (A ⇒ B) → Set₁
_⊑_ {A} F G =
  ∀ I → (inode * I ⊨ (S , T) , iface A) → (I ⊨a impl F) → (I ⊨b impl G)

data _≣_ {A B : Object S T} (F G : A ⇒ B) : Set₁ where
  _,_ : (F ⊑ G) → (G ⊑ F) → (F ≣ G)

-- An alternative characterization, which may be easier
-- to work with.

_⊑′_ : ∀ {A B : Object S T} → (A ⇒ B) → (A ⇒ B) → Set₁
F ⊑′ G = ∀ I I⊨STA → (apply F I I⊨STA) ⊨b (impl G)

⊑′-impl-⊑ : ∀ {A B : Object S T} → (F G : A ⇒ B) → (F ⊑′ G) → (F ⊑ G)
⊑′-impl-⊑ F G F⊑′G I I⊨STA I⊨F =
  ⊨b-resp-≲ (apply-≲ F I I⊨STA I⊨F) (impl G) (F⊑′G (inode * I) I⊨STA)

⊑-impl-⊑′ : ∀ {A B : Object S T} → (F G : A ⇒ B) → (F ⊑ G) → (F ⊑′ G)
⊑-impl-⊑′ {A} {B} F G F⊑G I (I⊨ST , I⊨A) = J⊨G where

  J : Interp Σ (IN A ⊕ BN F ⊕ IN B)
  J = apply F I (I⊨ST , I⊨A)

  J⊨S : ⌊ J ⌋ ⊨t S
  J⊨S = proj₁ (init-⊨ (apply-init F I (I⊨ST , I⊨A)))

  J⊨T : ⌊ J ⌋ ⊨t T
  J⊨T = proj₁ (apply-⊨ F I (I⊨ST , I⊨A))

  J⊨A : inode * J ⊨a iface A
  J⊨A = ⊨a-resp-≲ (init-≲ (apply-init F I (I⊨ST , I⊨A))) (iface A) I⊨A

  J⊨F : J ⊨a impl F
  J⊨F = proj₂ (init-⊨ (apply-init F I (I⊨ST , I⊨A)))

  J⊨G : J ⊨b impl G
  J⊨G = F⊑G J ((J⊨S , J⊨T) , J⊨A) J⊨F

ext: agda

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
module x03-842Relations-hc where

-- Library

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym) -- added sym
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-comm)

-- The less-than-or-equal-to relation.

data _≤_ : ℕ → ℕ → Set where

  z≤n : ∀ {n : ℕ}
      --------
    → zero ≤ n

  s≤s : ∀ {m n : ℕ}
    → m ≤ n
      -------------
    → suc m ≤ suc n

-- Some examples.

_ : 2 ≤ 4 -- can do just by refine
_ = s≤s (s≤s z≤n)

_ : 2 ≤ 4 -- with implicit args
_ = s≤s {1} {3} (s≤s {0} {2} z≤n)

_ : 2 ≤ 4 -- with named implicit args
_ = s≤s {m = 1} {n = 3} (s≤s {m = 0} {n = 2} z≤n)

_ : 2 ≤ 4 -- with some implicit named args
_ = s≤s {n = 3} (s≤s {m = 0} z≤n)

infix 4 _≤_

-- Inversion.

inv-s≤s : ∀ {m n : ℕ}
  → suc m ≤ suc n
    -------------
  → m ≤ n

inv-s≤s (s≤s x) = x

inv-z≤n : ∀ {m : ℕ}
  → m ≤ zero
    --------
  → m ≡ zero

inv-z≤n z≤n = refl

-- Properties.

-- Reflexivity.

≤-refl : ∀ {n : ℕ}
    -----
  → n ≤ n

≤-refl {zero} = z≤n
≤-refl {suc n} = s≤s (≤-refl {n})

-- Transitivity.

≤-trans : ∀ {m n p : ℕ} -- note implicit arguments
  → m ≤ n
  → n ≤ p
    -----
  → m ≤ p

≤-trans z≤n n≤p = z≤n
≤-trans (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans m≤n n≤p)

≤-trans′ : ∀ (m n p : ℕ) -- without implicit arguments
  → m ≤ n
  → n ≤ p
    -----
  → m ≤ p

≤-trans′ .0 _ _ z≤n n≤p = z≤n
≤-trans′ (suc m) (suc n) (suc p) (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans′ m n p m≤n n≤p)

-- Antisymmetry.

≤-antisym : ∀ {m n : ℕ}
  → m ≤ n
  → n ≤ m
    -----
  → m ≡ n

≤-antisym z≤n z≤n = refl
≤-antisym (s≤s m≤n) (s≤s n≤m) rewrite ≤-antisym m≤n n≤m = refl

-- Total ordering.

-- A definition with parameters.

data Total (m n : ℕ) : Set where

  forward :
      m ≤ n
      ---------
    → Total m n

  flipped :
      n ≤ m
      ---------
    → Total m n

-- An equivalent definition without parameters.

data Total′ : ℕ → ℕ → Set where

  forward′ : ∀ {m n : ℕ}
    → m ≤ n
      ----------
    → Total′ m n

  flipped′ : ∀ {m n : ℕ}
    → n ≤ m
      ----------
    → Total′ m n

-- Showing that ≤ is a total order.

≤-total : ∀ (m n : ℕ) → Total m n -- introducing with clause
≤-total zero n = forward z≤n
≤-total (suc m) zero = flipped z≤n
≤-total (suc m) (suc n) with ≤-total m n
... | forward x = forward (s≤s x)
... | flipped x = flipped (s≤s x)

≤-total′ : ∀ (m n : ℕ) → Total m n -- with helper function and where
≤-total′ zero n = forward z≤n
≤-total′ (suc m) zero = flipped z≤n
≤-total′ (suc m) (suc n) = helper (≤-total m n)
  where
    helper : Total m n → Total (suc m) (suc n)
    helper (forward x) = forward (s≤s x)
    helper (flipped x) = flipped (s≤s x)

-- Splitting on n first gives different code (see PLFA or try it yourself).

-- Monotonicity.

+-monoʳ-≤ : ∀ (m p q : ℕ)
  → p ≤ q
    -------------
  → m + p ≤ m + q

+-monoʳ-≤ zero p q p≤q = p≤q -- split on m
+-monoʳ-≤ (suc m) p q p≤q = s≤s (+-monoʳ-≤ m p q p≤q) -- refine, recurse

+-monoˡ-≤ : ∀ (m n p : ℕ)
  → m ≤ n
    -------------
  → m + p ≤ n + p

+-monoˡ-≤ m n p m≤n rewrite +-comm m p | +-comm n p = +-monoʳ-≤ p m n m≤n -- use commutativity

+-mono-≤ : ∀ (m n p q : ℕ) -- combine above
  → m ≤ n
  → p ≤ q
    -------------
  → m + p ≤ n + q

+-mono-≤ m n p q m≤n p≤q = ≤-trans (+-monoʳ-≤ m p q p≤q ) (+-monoˡ-≤ m n q m≤n)

-- PLFA exercise: show *-mono-≤.

-- Strict inequality.

infix 4 _<_

data _<_ : ℕ → ℕ → Set where

  z<s : ∀ {n : ℕ}
      ------------
    → zero < suc n

  s<s : ∀ {m n : ℕ}
    → m < n
      -------------
    → suc m < suc n

-- 842 exercise: LTTrans (1 point)
-- Prove that < is transitive.
-- Order of arguments changed from PLFA, to match ≤-trans.

<-trans : ∀ {m n p : ℕ} → m < n → n < p → m < p -- TODO
<-trans m<n n<p = {!!}

-- 842 exercise: Trichotomy (2 points)
-- Prove that either m < n, m ≡ n, or m > n for all m and n.

data Trichotomy (m n : ℕ) : Set where
  is-< : m < n → Trichotomy m n
  is-≡ : m ≡ n → Trichotomy m n
  is-> : n < m → Trichotomy m n

<-trichotomy : ∀ (m n : ℕ) → Trichotomy m n -- TODO
<-trichotomy m n = {!!}

-- PLFA exercise: show +-mono-<.

-- Prove that suc m ≤ n implies m < n, and conversely,
-- and do the same for (m ≤ n) and (m < suc n).
-- Hint: if you do the proofs in the order below, you can avoid induction
-- for two of the four proofs.

-- 842 exercise: LEtoLTS (1 point)

≤-<-to : ∀ {m n : ℕ} → m ≤ n → m < suc n -- TODO
≤-<-to m≤n = {!!}

-- 842 exercise: LEStoLT (1 point)

≤-<--to′ : ∀ {m n : ℕ} → suc m ≤ n → m < n -- TODO
≤-<--to′ sm≤n = {!!}

-- 842 exercise: LTtoSLE (1 point)

≤-<-from : ∀ {m n : ℕ} → m < n → suc m ≤ n -- TODO
≤-<-from m<n = {!!}

-- 842 exercise: LTStoLE (1 point)

≤-<-from′ : ∀ {m n : ℕ} → m < suc n → m ≤ n -- TODO
≤-<-from′ m<sn = {!!}

-- PLFA exercise: use the above to give a proof of <-trans that uses ≤-trans. -- TODO

-- Mutually recursive datatypes.
-- Specify the types first, then give the definitions.

data even : ℕ → Set
data odd  : ℕ → Set

data even where

  zero :
      ---------
      even zero

  suc  : ∀ {n : ℕ}
    → odd n
      ------------
    → even (suc n)

data odd where

  suc   : ∀ {n : ℕ}
    → even n
      -----------
    → odd (suc n)

-- Theorems about these datatypes.
-- The proofs are also mutually recursive.
-- So we give the types first, then the implementations.

e+e≡e : ∀ {m n : ℕ}
  → even m
  → even n
    ------------
  → even (m + n)

o+e≡o : ∀ {m n : ℕ}
  → odd m
  → even n
    -----------
  → odd (m + n)

e+e≡e zero en = en
e+e≡e (suc x) en = suc (o+e≡o x en)

o+e≡o (suc x) en = suc (e+e≡e x en)

-- 842 exercise: OPOE (2 points)
-- Prove that the sum of two odds is even.
-- Hint: You will need to define another theorem and prove both
--       by mutual induction, as with the theorems above.

o+o≡e : ∀ {m n : ℕ} → odd m → odd n → even (m + n) -- TODO
o+o≡e om on = {!!}

-- For remarks on which of these definitions are in the standard library, see PLFA.

-- Here is the new Unicode used in this file.

{-

≤  U+2264  LESS-THAN OR EQUAL TO (\<=, \le)
≥  U+2265  GREATER-THAN OR EQUAL TO (\>=, \ge)
ˡ  U+02E1  MODIFIER LETTER SMALL L (\^l)
ʳ  U+02B3  MODIFIER LETTER SMALL R (\^r)

-}

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
{-# OPTIONS --cubical --no-import-sorts #-}

module Test4 where

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Foundations.Logic
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv

record !_ {ℓ} (X : Type ℓ) : Type ℓ where
  inductive
  constructor !!_
  field x : X

open !_ hiding (x)
infix 1 !!_
infix 1 !_

!-iso : ∀{ℓ} {X : Type ℓ} → Iso (! X) X
Iso.fun      !-iso = !_.x
Iso.inv      !-iso = !!_
Iso.rightInv !-iso = λ      x  → refl
Iso.leftInv  !-iso = λ{ (!! x) → refl }

!-≡ : ∀{ℓ} {X : Type ℓ} → (! X) ≡ X
!-≡ {X = X} = isoToPath !-iso

!-equiv : ∀{ℓ} {X : Type ℓ} → (! X) ≃ X
!-equiv = !_.x , λ where .equiv-proof x → ((!! x) , refl) , λ{ ((!! y) , p) → λ i → (!! p (~ i)) , (λ j → p (~ i ∨ j)) }

hPropRel : ∀ {ℓ} (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
hPropRel A B ℓ' = A → B → hProp ℓ'

module TestB {ℓ ℓ'} (X : Type ℓ)
             (0ˣ : X) (_+_ _·_ : X → X → X) (_<_ : hPropRel X X ℓ')
             (let infixl 5 _+_; _+_ = _+_) where

  _≤_ : hPropRel X X ℓ'
  x ≤ y = ¬(y < x)

  postulate
    sqrt : (x : X) → {{ ! [ 0ˣ ≤ x ] }} → X
    0≤x² : ∀ x → [ 0ˣ ≤ (x · x) ]

  instance -- module-scope instances
    _ = λ {x} → !! 0≤x² x

  test4 : (x y z : X) → [ 0ˣ ≤ x ] → [ 0ˣ ≤ y ] → X
  test4 x y z 0≤x 0≤y =
    let instance -- let-scope instances
          _ = !! 0≤x
          _ = !! 0≤y
          _ = !! 0≤x² x -- preferred over the instance from module-scope
    in ( (sqrt x)       -- works
       + (sqrt y)       -- also works
       + (sqrt (z · z)) -- uses instance from module scope
       + (sqrt (x · x)) -- uses instance from let-scope (?) -- NOTE: see https://github.com/agda/agda/issues/4688
       )

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
----------------------------------------------------------------
-- This file contains the definition of categories.           --
----------------------------------------------------------------
module Category.Category where

open import Level public renaming (suc to lsuc)
open import Data.Product

open import Setoid.Total public
open import Relation.Relation

open Setoid public

record Cat {l : Level} : Set (lsuc l) where
  field
    Obj     : Set l
    Hom     : Obj → Obj → Setoid {l}
    comp    : {A B C : Obj} → BinSetoidFun (Hom A B) (Hom B C) (Hom A C)
    id      : {A : Obj} → el (Hom A A)
    assocPf : ∀{A B C D}{f : el (Hom A B)}{g : el (Hom B C)}{h : el (Hom C D)}
               → ⟨ Hom A D ⟩[ f ○[ comp ] (g ○[ comp ] h)  ≡  (f ○[ comp ] g) ○[ comp ] h ]
    idPfCom : ∀{A B}{f : el (Hom A B)} → ⟨ Hom A B ⟩[ id ○[ comp ] f ≡ f ○[ comp ] id  ]
    idPf    : ∀{A B}{f : el (Hom A B)} → ⟨ Hom A B ⟩[ id ○[ comp ] f ≡ f ]

open Cat public

objectSetoid : {l : Level} → (ℂ : Cat {l}) → Setoid {l}
objectSetoid {l} ℂ = record { el = Obj ℂ;
                              eq = λ a b → _≅_ a b;
                           eqRpf = record { parEqPf = record { symPf = λ x₁ → sym x₁ ; transPf = λ x₁ x₂ → trans x₁ x₂ } ; refPf = refl }
                 }

-- Identities composed on the left cancel.
idPf-left : ∀{l}{ℂ : Cat {l}}{A B : Obj ℂ}{f : el (Hom ℂ A B)} → ⟨ Hom ℂ A B ⟩[ f ○[ comp ℂ ] id ℂ ≡ f ]
idPf-left {_}{ℂ}{A}{B}{f} =
  transPf (parEqPf (eqRpf (Hom ℂ A B)))
          (symPf (parEqPf (eqRpf (Hom ℂ A B))) (idPfCom ℂ {A} {B} {f}))
          (idPf ℂ)

-- Congruence results for composition.
eq-comp-right : ∀{l}
    {ℂ : Cat {l}}
    {A B C : Obj ℂ}
    {f : el (Hom ℂ A B)}
    {g₁ g₂ : el (Hom ℂ B C)}
  → ⟨ Hom ℂ B C ⟩[ g₁ ≡ g₂ ]
  → ⟨ Hom ℂ A C ⟩[ f ○[ comp ℂ ] g₁ ≡ f ○[ comp ℂ ] g₂ ]
eq-comp-right {_}{ℂ}{A}{B}{C}{f}{g₁}{g₂} eq =
  extT (appT {_}{_}{Hom ℂ A B}{SetoidFunSpace (Hom ℂ B C) (Hom ℂ A C)} (comp ℂ) f) eq

eq-comp-left : ∀{l}
    {ℂ : Cat {l}}
    {A B C : Obj ℂ}
    {f₁ f₂ : el (Hom ℂ A B)}
    {g : el (Hom ℂ B C)}
  → ⟨ Hom ℂ A B ⟩[ f₁ ≡ f₂ ]
  → ⟨ Hom ℂ A C ⟩[ f₁ ○[ comp ℂ ] g ≡ f₂ ○[ comp ℂ ] g ]
eq-comp-left {_}{ℂ}{A}{B}{C}{f₁}{f₂}{g} eq = extT (comp ℂ) {f₁}{f₂} eq g

eq-comp-all : ∀{l}
    {ℂ : Cat {l}}
    {A B C : Obj ℂ}
    {f₁ f₂ : el (Hom ℂ A B)}
    {g₁ g₂ : el (Hom ℂ B C)}
  → ⟨ Hom ℂ A B ⟩[ f₁ ≡ f₂ ]
  → ⟨ Hom ℂ B C ⟩[ g₁ ≡ g₂ ]
  → ⟨ Hom ℂ A C ⟩[ f₁ ○[ comp ℂ ] g₁ ≡ f₂ ○[ comp ℂ ] g₂ ]
eq-comp-all {_}{ℂ}{A}{B}{C}{f₁}{f₂}{g₁}{g₂} eq₁ eq₂
  with eq-comp-left {_}{ℂ}{A}{B}{C}{f₁}{f₂}{g₁} eq₁ |
       eq-comp-right {_}{ℂ}{A}{B}{C}{f₂}{g₁}{g₂} eq₂
... | eq₃ | eq₄ = transPf (parEqPf (eqRpf (Hom ℂ A C))) eq₃ eq₄

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
------------------------------------------------------------------------
-- The "circle"
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

-- Partly following the HoTT book.

-- The module is parametrised by a notion of equality. The higher
-- constructor of the HIT defining the circle uses path equality, but
-- the supplied notion of equality is used for many other things.

import Equality.Path as P

module Circle {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq hiding (elim)

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J as Bijection using (_↔_)
import Bijection P.equality-with-J as PB
open import Equality.Groupoid equality-with-J
open import Equality.Path.Isomorphisms eq
open import Equality.Path.Isomorphisms.Univalence eq
import Equality.Path.Isomorphisms P.equality-with-paths as PI
open import Equality.Tactic equality-with-J hiding (module Eq)
open import Equivalence equality-with-J as Eq using (_≃_)
import Equivalence P.equality-with-J as PE
import Erased.Cubical eq as E
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import Group equality-with-J as G using (_≃ᴳ_)
import Group.Cyclic eq as C
open import Groupoid equality-with-J
open import H-level equality-with-J as H-level
open import H-level.Closure equality-with-J
open import H-level.Truncation eq as T using (∥_∥[1+_])
open import H-level.Truncation.Propositional eq as Trunc
  using (∥_∥; ∣_∣)
open import H-level.Truncation.Propositional.One-step eq as O
  using (∥_∥¹)
open import Integer equality-with-J as Int
  using (ℤ; +_; -[1+_]; ℤ-group)
open import Nat equality-with-J
open import Pointed-type equality-with-J as PT using (_≃ᴮ_)
open import Pointed-type.Homotopy-group eq
open import Sphere eq as Sphere using (𝕊)
open import Suspension eq as Suspension
  using (Susp; north; south; meridian)
open import Univalence-axiom equality-with-J as Univ using (Univalence)

private
  variable
    a p   : Level
    A     : Type p
    P     : A → Type p
    f     : (x : A) → P x
    b ℓ x : A

------------------------------------------------------------------------
-- The type and some eliminators

-- The circle.

data 𝕊¹ : Type where
  base  : 𝕊¹
  loopᴾ : base P.≡ base

loop : base ≡ base
loop = _↔_.from ≡↔≡ loopᴾ

-- A dependent eliminator, expressed using paths.

elimᴾ :
  (P : 𝕊¹ → Type p)
  (b : P base) →
  P.[ (λ i → P (loopᴾ i)) ] b ≡ b →
  (x : 𝕊¹) → P x
elimᴾ P b ℓ base      = b
elimᴾ P b ℓ (loopᴾ i) = ℓ i

-- A non-dependent eliminator, expressed using paths.

recᴾ : (b : A) → b P.≡ b → 𝕊¹ → A
recᴾ = elimᴾ _

-- A dependent eliminator.

elim :
  (P : 𝕊¹ → Type p)
  (b : P base) →
  subst P loop b ≡ b →
  (x : 𝕊¹) → P x
elim P b ℓ = elimᴾ P b (subst≡→[]≡ ℓ)

-- A "computation" rule.

elim-loop : dcong (elim P b ℓ) loop ≡ ℓ
elim-loop = dcong-subst≡→[]≡ (refl _)

-- Every dependent function of type (x : 𝕊¹) → P x can be expressed
-- using elim.

η-elim :
  {f : (x : 𝕊¹) → P x} →
  f ≡ elim P (f base) (dcong f loop)
η-elim {P = P} {f = f} =
  ⟨ext⟩ $ elim _ (refl _)
    (subst (λ x → f x ≡ elim P (f base) (dcong f loop) x) loop (refl _)  ≡⟨ subst-in-terms-of-trans-and-dcong ⟩

     trans (sym (dcong f loop))
       (trans (cong (subst P loop) (refl _))
          (dcong (elim P (f base) (dcong f loop)) loop))                 ≡⟨ cong (trans (sym (dcong f loop))) $
                                                                            trans (cong (flip trans _) $ cong-refl _) $
                                                                            trans-reflˡ _ ⟩
     trans (sym (dcong f loop))
       (dcong (elim P (f base) (dcong f loop)) loop)                     ≡⟨ cong (trans (sym (dcong f loop))) elim-loop ⟩

     trans (sym (dcong f loop)) (dcong f loop)                           ≡⟨ trans-symˡ _ ⟩∎

     refl _                                                              ∎)

-- A non-dependent eliminator.

rec : (b : A) → b ≡ b → 𝕊¹ → A
rec b ℓ = recᴾ b (_↔_.to ≡↔≡ ℓ)

-- A "computation" rule.

rec-loop : cong (rec b ℓ) loop ≡ ℓ
rec-loop = cong-≡↔≡ (refl _)

-- Every function from 𝕊¹ to A can be expressed using rec.

η-rec : {f : 𝕊¹ → A} → f ≡ rec (f base) (cong f loop)
η-rec {f = f} =
  ⟨ext⟩ $ elim _ (refl _)
    (subst (λ x → f x ≡ rec (f base) (cong f loop) x) loop (refl _)      ≡⟨ subst-in-terms-of-trans-and-cong ⟩

     trans (sym (cong f loop))
       (trans (refl _) (cong (rec (f base) (cong f loop)) loop))         ≡⟨ cong (trans (sym (cong f loop))) $ trans-reflˡ _ ⟩

     trans (sym (cong f loop)) (cong (rec (f base) (cong f loop)) loop)  ≡⟨ cong (trans (sym (cong f loop))) rec-loop ⟩

     trans (sym (cong f loop)) (cong f loop)                             ≡⟨ trans-symˡ _ ⟩∎

     refl _                                                              ∎)

-- An alternative non-dependent eliminator.

rec′ : (b : A) → b ≡ b → 𝕊¹ → A
rec′ {A = A} b ℓ = elim
  (const A)
  b
  (subst (const A) loop b  ≡⟨ subst-const _ ⟩
   b                       ≡⟨ ℓ ⟩∎
   b                       ∎)

-- A "computation" rule.

rec′-loop : cong (rec′ b ℓ) loop ≡ ℓ
rec′-loop = dcong≡→cong≡ elim-loop

------------------------------------------------------------------------
-- Some equivalences

-- The circle can be expressed as a suspension.

𝕊¹≃Susp-Bool : 𝕊¹ ≃ Susp Bool
𝕊¹≃Susp-Bool = Eq.↔→≃ to from to∘from from∘to
  where
  north≡north =
    north  ≡⟨ meridian false ⟩
    south  ≡⟨ sym $ meridian true ⟩∎
    north  ∎

  to : 𝕊¹ → Susp Bool
  to = rec north north≡north

  module From = Suspension.Rec base base (if_then refl base else loop)

  from : Susp Bool → 𝕊¹
  from = From.rec

  to∘from : ∀ x → to (from x) ≡ x
  to∘from = Suspension.elim _
    (to (from north)  ≡⟨⟩
     north            ∎)
    (to (from south)  ≡⟨⟩
     north            ≡⟨ meridian true ⟩∎
     south            ∎)
    (λ b →
       subst (λ x → to (from x) ≡ x) (meridian b) (refl north)  ≡⟨ subst-in-terms-of-trans-and-cong ⟩

       trans (sym (cong (to ∘ from) (meridian b)))
         (trans (refl _) (cong id (meridian b)))                ≡⟨ cong₂ (trans ∘ sym)
                                                                     (trans (sym $ cong-∘ _ _ _) $
                                                                      cong (cong to) From.rec-meridian)
                                                                     (trans (trans-reflˡ _) $
                                                                      sym $ cong-id _) ⟩
       trans (sym (cong to (if b then refl base else loop)))
             (meridian b)                                       ≡⟨ lemma b ⟩∎

       meridian true                                            ∎)
    where
    lemma : (b : Bool) → _ ≡ _
    lemma true  =
      trans (sym (cong to (if true ⦂ Bool then refl base else loop)))
            (meridian true)                                            ≡⟨⟩

      trans (sym (cong to (refl base))) (meridian true)                ≡⟨ prove (Trans (Sym (Cong _ Refl)) (Lift _)) (Lift _) (refl _) ⟩∎

      meridian true                                                    ∎

    lemma false =
      trans (sym (cong to (if false ⦂ Bool then refl base else loop)))
            (meridian false)                                            ≡⟨⟩

      trans (sym (cong to loop)) (meridian false)                       ≡⟨ cong (λ p → trans (sym p) (meridian false)) rec-loop ⟩

      trans (sym north≡north) (meridian false)                          ≡⟨ prove (Trans (Sym (Trans (Lift _) (Sym (Lift _)))) (Lift _))
                                                                                (Trans (Trans (Lift _) (Sym (Lift _))) (Lift _))
                                                                                (refl _) ⟩
      trans (trans (meridian true) (sym $ meridian false))
            (meridian false)                                            ≡⟨ trans-[trans-sym]- _ _ ⟩∎

      meridian true                                                     ∎

  from∘to : ∀ x → from (to x) ≡ x
  from∘to = elim _
    (from (to base)  ≡⟨⟩
     base            ∎)
    (subst (λ x → from (to x) ≡ x) loop (refl base)                  ≡⟨ subst-in-terms-of-trans-and-cong ⟩

     trans (sym (cong (from ∘ to) loop))
           (trans (refl base) (cong id loop))                        ≡⟨ cong₂ (trans ∘ sym)
                                                                          (trans (sym $ cong-∘ _ to _) $
                                                                           cong (cong from) rec-loop)
                                                                          (trans (trans-reflˡ _) $
                                                                           sym $ cong-id _) ⟩

     trans (sym (cong from north≡north)) loop                        ≡⟨ prove (Trans (Sym (Cong _ (Trans (Lift _) (Sym (Lift _))))) (Lift _))
                                                                              (Trans (Trans (Cong from (Lift (meridian true)))
                                                                                (Sym (Cong from (Lift (meridian false)))))
                                                                                (Lift _))
                                                                              (refl _) ⟩
     trans (trans (cong from (meridian true))
                  (sym $ cong from (meridian false)))
           loop                                                      ≡⟨ cong₂ (λ p q → trans (trans p (sym q)) loop)
                                                                          From.rec-meridian
                                                                          From.rec-meridian ⟩
     trans (trans (if true ⦂ Bool then refl base else loop)
                  (sym $ if false ⦂ Bool then refl base else loop))
           loop                                                      ≡⟨⟩

     trans (trans (refl base) (sym loop)) loop                       ≡⟨ trans-[trans-sym]- _ _ ⟩∎

     refl base                                                       ∎)

-- The circle is equivalent to the 1-dimensional sphere.

𝕊¹≃𝕊¹ : 𝕊¹ ≃ 𝕊 1
𝕊¹≃𝕊¹ =
  𝕊¹          ↝⟨ 𝕊¹≃Susp-Bool ⟩
  Susp Bool   ↔⟨ Suspension.cong-↔ Sphere.Bool↔𝕊⁰ ⟩
  Susp (𝕊 0)  ↔⟨⟩
  𝕊 1         □

------------------------------------------------------------------------
-- The loop space of the circle

-- The function trans is commutative for the loop space of the circle.

trans-commutative : (p q : base ≡ base) → trans p q ≡ trans q p
trans-commutative =
  flip $ Transitivity-commutative.commutative base _∙_ ∙-base base-∙
  where
  _∙_ : 𝕊¹ → 𝕊¹ → 𝕊¹
  x ∙ y = rec x (elim (λ x → x ≡ x) loop lemma x) y
    where
    lemma : subst (λ x → x ≡ x) loop loop ≡ loop
    lemma = ≡⇒↝ _ (sym [subst≡]≡[trans≡trans]) (refl _)

  base-∙ : ∀ x → x ∙ base ≡ x
  base-∙ _ = refl _

  ∙-base : ∀ y → base ∙ y ≡ y
  ∙-base =
    elim _ (refl _)
      (subst (λ x → rec base loop x ≡ x) loop (refl _)         ≡⟨ subst-in-terms-of-trans-and-cong ⟩

       trans (sym (cong (rec base loop) loop))
         (trans (refl _) (cong id loop))                       ≡⟨ cong (trans _) $ trans-reflˡ _ ⟩

       trans (sym (cong (rec base loop) loop)) (cong id loop)  ≡⟨ cong₂ (trans ∘ sym)
                                                                    rec-loop
                                                                    (sym $ cong-id _) ⟩

       trans (sym loop) loop                                   ≡⟨ trans-symˡ _ ⟩∎

       refl _                                                  ∎)

-- The loop space is equivalent to x ≡ x, for any x : 𝕊¹.

base≡base≃≡ : {x : 𝕊¹} → (base ≡ base) ≃ (x ≡ x)
base≡base≃≡ = elim
  (λ x → (base ≡ base) ≃ (x ≡ x))
  Eq.id
  (Eq.lift-equality ext $ ⟨ext⟩ λ eq →
   _≃_.to (subst (λ x → (base ≡ base) ≃ (x ≡ x)) loop Eq.id) eq        ≡⟨ cong (_$ eq) Eq.to-subst ⟩
   subst (λ x → base ≡ base → x ≡ x) loop id eq                        ≡⟨ subst-→ ⟩
   subst (λ x → x ≡ x) loop (subst (λ _ → base ≡ base) (sym loop) eq)  ≡⟨ cong (subst (λ x → x ≡ x) loop) $ subst-const _ ⟩
   subst (λ x → x ≡ x) loop eq                                         ≡⟨ ≡⇒↝ _ (sym [subst≡]≡[trans≡trans]) (

       trans eq loop                                                        ≡⟨ trans-commutative _ _ ⟩∎
       trans loop eq                                                        ∎) ⟩∎

   eq                                                                  ∎)
  _

private

  -- Definitions used to define base≡base≃ℤ and Fundamental-group≃ℤ.

  module base≡base≃ℤ (univ : Univalence lzero) where

    -- The universal cover of the circle.

    Cover : 𝕊¹ → Type
    Cover = rec ℤ (Univ.≃⇒≡ univ Int.successor)

    to : base ≡ x → Cover x
    to = flip (subst Cover) (+ 0)

    ≡⇒≃-cong-Cover-loop : Univ.≡⇒≃ (cong Cover loop) ≡ Int.successor
    ≡⇒≃-cong-Cover-loop =
      Univ.≡⇒≃ (cong Cover loop)              ≡⟨ cong Univ.≡⇒≃ rec-loop ⟩
      Univ.≡⇒≃ (Univ.≃⇒≡ univ Int.successor)  ≡⟨ _≃_.right-inverse-of (Univ.≡≃≃ univ) _ ⟩∎
      Int.successor                           ∎

    subst-Cover-loop :
      ∀ i → subst Cover loop i ≡ Int.suc i
    subst-Cover-loop i =
      subst Cover loop i            ≡⟨ subst-in-terms-of-≡⇒↝ equivalence _ _ _ ⟩
      Univ.≡⇒→ (cong Cover loop) i  ≡⟨ cong (λ eq → _≃_.to eq _) ≡⇒≃-cong-Cover-loop ⟩∎
      _≃_.to Int.successor i        ∎

    subst-Cover-sym-loop :
      ∀ i → subst Cover (sym loop) i ≡ Int.pred i
    subst-Cover-sym-loop i =
      subst Cover (sym loop) i                 ≡⟨ subst-in-terms-of-inverse∘≡⇒↝ equivalence _ _ _ ⟩
      _≃_.from (Univ.≡⇒≃ (cong Cover loop)) i  ≡⟨ cong (λ eq → _≃_.from eq _) ≡⇒≃-cong-Cover-loop ⟩∎
      _≃_.from Int.successor i                 ∎

    module 𝕊¹-G = Groupoid (groupoid 𝕊¹)

    loops : ℤ → base ≡ base
    loops = loop 𝕊¹-G.^_

    to-loops : ∀ i → to (loops i) ≡ i
    to-loops (+ zero) =
      subst Cover (refl _) (+ 0)  ≡⟨ subst-refl _ _ ⟩∎
      + zero                      ∎
    to-loops (+ suc n) =
      subst Cover (trans (loops (+ n)) loop) (+ 0)        ≡⟨ sym $ subst-subst _ _ _ _ ⟩
      subst Cover loop (subst Cover (loops (+ n)) (+ 0))  ≡⟨⟩
      subst Cover loop (to (loops (+ n)))                 ≡⟨ cong (subst Cover loop) $ to-loops (+ n) ⟩
      subst Cover loop (+ n)                              ≡⟨ subst-Cover-loop _ ⟩∎
      + suc n                                             ∎
    to-loops -[1+ zero ] =
      subst Cover (trans (refl _) (sym loop)) (+ 0)  ≡⟨ cong (flip (subst Cover) _) $ trans-reflˡ _ ⟩
      subst Cover (sym loop) (+ 0)                   ≡⟨ subst-Cover-sym-loop _ ⟩∎
      -[1+ zero ]                                    ∎
    to-loops -[1+ suc n ] =
      subst Cover (trans (loops -[1+ n ]) (sym loop)) (+ 0)        ≡⟨ sym $ subst-subst _ _ _ _ ⟩
      subst Cover (sym loop) (subst Cover (loops -[1+ n ]) (+ 0))  ≡⟨⟩
      subst Cover (sym loop) (to (loops -[1+ n ]))                 ≡⟨ cong (subst Cover (sym loop)) $ to-loops -[1+ n ] ⟩
      subst Cover (sym loop) -[1+ n ]                              ≡⟨ subst-Cover-sym-loop _ ⟩∎
      -[1+ suc n ]                                                 ∎

    loops-pred-loop :
      ∀ i → trans (loops (Int.pred i)) loop ≡ loops i
    loops-pred-loop i =
      trans (loops (Int.pred i)) loop                           ≡⟨ cong (flip trans _ ∘ loops) $ Int.pred≡-1+ i ⟩
      trans (loops (Int.-[ 1 ] Int.+ i)) loop                   ≡⟨ cong (flip trans _) $ sym $ 𝕊¹-G.^∘^ {j = i} Int.-[ 1 ] ⟩
      trans (trans (loops i) (loops (Int.-[ 1 ]))) loop         ≡⟨⟩
      trans (trans (loops i) (trans (refl _) (sym loop))) loop  ≡⟨ cong (flip trans _) $ cong (trans _) $ trans-reflˡ _ ⟩
      trans (trans (loops i) (sym loop)) loop                   ≡⟨ trans-[trans-sym]- _ _ ⟩∎
      loops i                                                   ∎

    from : ∀ x → Cover x → base ≡ x
    from = elim _
      loops
      (⟨ext⟩ λ i →
       subst (λ x → Cover x → base ≡ x) loop loops i            ≡⟨ subst-→ ⟩
       subst (base ≡_) loop (loops (subst Cover (sym loop) i))  ≡⟨ sym trans-subst ⟩
       trans (loops (subst Cover (sym loop) i)) loop            ≡⟨ cong (flip trans _ ∘ loops) $ subst-Cover-sym-loop _ ⟩
       trans (loops (Int.pred i)) loop                          ≡⟨ loops-pred-loop i ⟩∎
       loops i                                                  ∎)

    from-to : (eq : base ≡ x) → from x (to eq) ≡ eq
    from-to = elim¹
      (λ {x} eq → from x (to eq) ≡ eq)
      (from base (to (refl base))             ≡⟨⟩
       loops (subst Cover (refl base) (+ 0))  ≡⟨ cong loops $ subst-refl _ _ ⟩
       loops (+ 0)                            ≡⟨⟩
       refl base                              ∎)

    loops-+ : ∀ i j → loops (i Int.+ j) ≡ trans (loops i) (loops j)
    loops-+ i j =
      loops (i Int.+ j)          ≡⟨ cong loops $ Int.+-comm i ⟩
      loops (j Int.+ i)          ≡⟨ sym $ 𝕊¹-G.^∘^ j ⟩∎
      trans (loops i) (loops j)  ∎

-- The loop space of the circle is equivalent to the type of integers
-- (assuming univalence).
--
-- The proof is based on the one presented by Licata and Shulman in
-- "Calculating the Fundamental Group of the Circle in Homotopy Type
-- Theory".

base≡base≃ℤ :
  Univalence lzero →
  (base ≡ base) ≃ ℤ
base≡base≃ℤ univ = Eq.↔→≃ to loops to-loops from-to
  where
  open base≡base≃ℤ univ

-- The circle's fundamental group is equivalent to the group of
-- integers (assuming univalence).

Fundamental-group≃ℤ :
  Univalence lzero →
  Fundamental-group (𝕊¹ , base) ≃ᴳ ℤ-group
Fundamental-group≃ℤ univ = G.≃ᴳ-sym λ where
    .G.Homomorphic.related → inverse
      (∥ base ≡ base ∥[1+ 1 ]  ↝⟨ T.∥∥-cong $ base≡base≃ℤ univ ⟩
       ∥ ℤ ∥[1+ 1 ]            ↔⟨ _⇔_.to (T.+⇔∥∥↔ {n = 1}) Int.ℤ-set ⟩□
       ℤ                       □)
    .G.Homomorphic.homomorphic i j → cong T.∣_∣ (loops-+ i j)
  where
  open base≡base≃ℤ univ

-- The circle is a groupoid (assuming univalence).

𝕊¹-groupoid :
  Univalence lzero →
  H-level 3 𝕊¹
𝕊¹-groupoid univ {x = x} {y = y} =
                        $⟨ (λ {_ _} → Int.ℤ-set) ⟩
  Is-set ℤ              ↝⟨ H-level-cong _ 2 (inverse $ base≡base≃ℤ univ) ⦂ (_ → _) ⟩
  Is-set (base ≡ base)  ↝⟨ (λ s →
                              elim
                                (λ x → ∀ y → Is-set (x ≡ y))
                                (elim _ s (H-level-propositional ext 2 _ _))
                                ((Π-closure ext 1 λ _ →
                                  H-level-propositional ext 2)
                                   _ _)
                                x y) ⟩□
  Is-set (x ≡ y)        □

-- The type of endofunctions on 𝕊¹ is equivalent to
-- ∃ λ (x : 𝕊¹) → x ≡ x.

𝕊¹→𝕊¹≃Σ𝕊¹≡ : (𝕊¹ → 𝕊¹) ≃ ∃ λ (x : 𝕊¹) → x ≡ x
𝕊¹→𝕊¹≃Σ𝕊¹≡ = Eq.↔→≃ to from to-from from-to
  where
  to : (𝕊¹ → 𝕊¹) → ∃ λ (x : 𝕊¹) → x ≡ x
  to f = f base , cong f loop

  from : (∃ λ (x : 𝕊¹) → x ≡ x) → (𝕊¹ → 𝕊¹)
  from = uncurry rec

  to-from : ∀ p → to (from p) ≡ p
  to-from (x , eq) = cong (x ,_)
    (cong (rec x eq) loop  ≡⟨ rec-loop ⟩∎
     eq                    ∎)

  from-to : ∀ f → from (to f) ≡ f
  from-to f =
    rec (f base) (cong f loop)  ≡⟨ sym η-rec ⟩∎
    f                           ∎

-- The type of endofunctions on 𝕊¹ is equivalent to 𝕊¹ × ℤ (assuming
-- univalence).
--
-- This result was pointed out to me by Paolo Capriotti.

𝕊¹→𝕊¹≃𝕊¹×ℤ :
  Univalence lzero →
  (𝕊¹ → 𝕊¹) ≃ (𝕊¹ × ℤ)
𝕊¹→𝕊¹≃𝕊¹×ℤ univ =
  (𝕊¹ → 𝕊¹)               ↝⟨ 𝕊¹→𝕊¹≃Σ𝕊¹≡ ⟩
  (∃ λ (x : 𝕊¹) → x ≡ x)  ↝⟨ (∃-cong λ _ → inverse base≡base≃≡) ⟩
  𝕊¹ × base ≡ base        ↝⟨ (∃-cong λ _ → base≡base≃ℤ univ) ⟩□
  𝕊¹ × ℤ                  □

-- The forward direction of 𝕊¹→𝕊¹≃𝕊¹×ℤ maps the identity function to
-- base , + 1.

𝕊¹→𝕊¹≃𝕊¹×ℤ-id :
  (univ : Univalence lzero) →
  _≃_.to (𝕊¹→𝕊¹≃𝕊¹×ℤ univ) id ≡ (base , + 1)
𝕊¹→𝕊¹≃𝕊¹×ℤ-id univ = _≃_.from-to (𝕊¹→𝕊¹≃𝕊¹×ℤ univ)
  (rec base (trans (refl base) loop)  ≡⟨ cong (rec base) $ trans-reflˡ _ ⟩
   rec base loop                      ≡⟨ cong (rec base) $ cong-id _ ⟩
   rec base (cong id loop)            ≡⟨ sym η-rec ⟩∎
   id                                 ∎)

-- The forward direction of 𝕊¹→𝕊¹≃𝕊¹×ℤ maps the constant function
-- returning base to base , + 0.

𝕊¹→𝕊¹≃𝕊¹×ℤ-const :
  (univ : Univalence lzero) →
  _≃_.to (𝕊¹→𝕊¹≃𝕊¹×ℤ univ) (const base) ≡ (base , + 0)
𝕊¹→𝕊¹≃𝕊¹×ℤ-const univ = _≃_.from-to (𝕊¹→𝕊¹≃𝕊¹×ℤ univ)
  (rec base (refl base)               ≡⟨ cong (rec base) $ sym $ cong-const _ ⟩
   rec base (cong (const base) loop)  ≡⟨ sym η-rec ⟩∎
   const base                         ∎)

------------------------------------------------------------------------
-- A conversion function

-- The one-step truncation of the unit type is equivalent to the
-- circle.
--
-- Paolo Capriotti informed me about this result.

∥⊤∥¹≃𝕊¹ : ∥ ⊤ ∥¹ ≃ 𝕊¹
∥⊤∥¹≃𝕊¹ = _↔_.from ≃↔≃ $ PE.↔→≃
  (O.recᴾ λ where
     .O.∣∣ʳ _            → base
     .O.∣∣-constantʳ _ _ → loopᴾ)
  (recᴾ O.∣ _ ∣ (O.∣∣-constantᴾ _ _))
  (elimᴾ _ P.refl (λ _ → P.refl))
  (O.elimᴾ λ where
     .O.∣∣ʳ _              → P.refl
     .O.∣∣-constantʳ _ _ _ → P.refl)

------------------------------------------------------------------------
-- Some negative results

-- The equality loop is not equal to refl base.

loop≢refl : loop ≢ refl base
loop≢refl =
  E.Stable-¬
    E.[ loop ≡ refl base  →⟨ Type-set ⟩
        Is-set Type       →⟨ Univ.¬-Type-set univ ⟩□
        ⊥                 □
      ]
  where
  module _ (loop≡refl : loop ≡ refl base) where

    refl≡ : (A : Type) (A≡A : A ≡ A) → refl A ≡ A≡A
    refl≡ A A≡A =
      refl A                        ≡⟨⟩
      refl (rec A A≡A base)         ≡⟨ sym $ cong-refl _ ⟩
      cong (rec A A≡A) (refl base)  ≡⟨ cong (cong (rec A A≡A)) $ sym loop≡refl ⟩
      cong (rec A A≡A) loop         ≡⟨ rec-loop ⟩∎
      A≡A                           ∎

    Type-set : Is-set Type
    Type-set {x = A} {y = B} =
      elim¹ (λ p → ∀ q → p ≡ q)
            (refl≡ A)

-- Thus the circle is not a set.

¬-𝕊¹-set : ¬ Is-set 𝕊¹
¬-𝕊¹-set =
  Is-set 𝕊¹                     ↝⟨ (λ h → h) ⟩
  Is-proposition (base ≡ base)  ↝⟨ (λ h → h _ _) ⟩
  loop ≡ refl base              ↝⟨ loop≢refl ⟩□
  ⊥                             □

-- It is not necessarily the case that the one-step truncation of a
-- proposition is a proposition.

¬-Is-proposition-∥∥¹ :
  ¬ ({A : Type a} → Is-proposition A → Is-proposition ∥ A ∥¹)
¬-Is-proposition-∥∥¹ {a = a} =
  ({A : Type a} → Is-proposition A → Is-proposition ∥ A ∥¹)  ↝⟨ _$ H-level.mono₁ 0 (↑-closure 0 ⊤-contractible) ⟩
  Is-proposition ∥ ↑ a ⊤ ∥¹                                  ↝⟨ H-level-cong _ 1 (O.∥∥¹-cong-↔ Bijection.↑↔) ⟩
  Is-proposition ∥ ⊤ ∥¹                                      ↝⟨ H-level-cong _ 1 ∥⊤∥¹≃𝕊¹ ⟩
  Is-proposition 𝕊¹                                          ↝⟨ ¬-𝕊¹-set ∘ H-level.mono₁ 1 ⟩□
  ⊥                                                          □

-- A function with the type of refl (for 𝕊¹) that is not equal to
-- refl.

not-refl : (x : 𝕊¹) → x ≡ x
not-refl = elim _
  loop
  (subst (λ z → z ≡ z) loop loop  ≡⟨ ≡⇒↝ _ (sym [subst≡]≡[trans≡trans]) (refl _) ⟩∎
   loop                           ∎)

-- The function not-refl is not equal to refl.

not-refl≢refl : not-refl ≢ refl
not-refl≢refl =
  not-refl ≡ refl   ↝⟨ cong (_$ _) ⟩
  loop ≡ refl base  ↝⟨ loop≢refl ⟩□
  ⊥                 □

-- There is a value with the type of refl that is not equal to refl.

∃≢refl : ∃ λ (f : (x : 𝕊¹) → x ≡ x) → f ≢ refl
∃≢refl = not-refl , not-refl≢refl

-- For every universe level there is a type A such that
-- (x : A) → x ≡ x is not a proposition.

¬-type-of-refl-propositional :
  ∃ λ (A : Type a) → ¬ Is-proposition ((x : A) → x ≡ x)
¬-type-of-refl-propositional {a = a} =
    ↑ _ 𝕊¹
  , (Is-proposition (∀ x → x ≡ x)                                 ↝⟨ (λ prop → prop _ _) ⟩

     cong lift ∘ proj₁ ∃≢refl ∘ lower ≡ cong lift ∘ refl ∘ lower  ↝⟨ cong (_∘ lift) ⟩

     cong lift ∘ proj₁ ∃≢refl ≡ cong lift ∘ refl                  ↝⟨ cong (cong lower ∘_) ⟩

     cong lower ∘ cong lift ∘ proj₁ ∃≢refl ≡
     cong lower ∘ cong lift ∘ refl                                ↝⟨ ≡⇒↝ _ (cong₂ _≡_ (⟨ext⟩ λ _ → cong-∘ _ _ _) (⟨ext⟩ λ _ → cong-∘ _ _ _)) ⟩

     cong id ∘ proj₁ ∃≢refl ≡ cong id ∘ refl                      ↝⟨ ≡⇒↝ _ (sym $ cong₂ _≡_ (⟨ext⟩ λ _ → cong-id _) (⟨ext⟩ λ _ → cong-id _)) ⟩

     proj₁ ∃≢refl ≡ refl                                          ↝⟨ proj₂ ∃≢refl ⟩□

     ⊥                                                            □)

-- Every element of the circle is /merely/ equal to the base point.
--
-- This lemma was mentioned by Mike Shulman in a blog post
-- (http://homotopytypetheory.org/2013/07/24/cohomology/).

all-points-on-the-circle-are-merely-equal :
  (x : 𝕊¹) → ∥ x ≡ base ∥
all-points-on-the-circle-are-merely-equal =
  elim _
       ∣ refl base ∣
       (Trunc.truncation-is-proposition _ _)

-- Thus every element of the circle is not not equal to the base
-- point.

all-points-on-the-circle-are-¬¬-equal :
  (x : 𝕊¹) → ¬ ¬ x ≡ base
all-points-on-the-circle-are-¬¬-equal x =
  x ≢ base        ↝⟨ Trunc.rec ⊥-propositional ⟩
  ¬ ∥ x ≡ base ∥  ↝⟨ _$ all-points-on-the-circle-are-merely-equal x ⟩□
  ⊥               □

-- It is not the case that every point on the circle is equal to the
-- base point.

¬-all-points-on-the-circle-are-equal :
  ¬ ((x : 𝕊¹) → x ≡ base)
¬-all-points-on-the-circle-are-equal =
  ((x : 𝕊¹) → x ≡ base)  ↝⟨ (λ hyp x y → x     ≡⟨ hyp x ⟩
                                         base  ≡⟨ sym (hyp y) ⟩∎
                                         y     ∎) ⟩
  Is-proposition 𝕊¹      ↝⟨ mono₁ 1 ⟩
  Is-set 𝕊¹              ↝⟨ ¬-𝕊¹-set ⟩□
  ⊥                      □

-- Thus double-negation shift for Type-valued predicates over 𝕊¹ does
-- not hold in general.

¬-double-negation-shift :
  ¬ ({P : 𝕊¹ → Type} → ((x : 𝕊¹) → ¬ ¬ P x) → ¬ ¬ ((x : 𝕊¹) → P x))
¬-double-negation-shift =
  ({P : 𝕊¹ → Type} → ((x : 𝕊¹) → ¬ ¬ P x) → ¬ ¬ ((x : 𝕊¹) → P x))  ↝⟨ _$ all-points-on-the-circle-are-¬¬-equal ⟩
  ¬ ¬ ((x : 𝕊¹) → x ≡ base)                                        ↝⟨ _$ ¬-all-points-on-the-circle-are-equal ⟩□
  ⊥                                                                □

-- Furthermore excluded middle for arbitrary types (in Type) does not
-- hold.

¬-excluded-middle : ¬ ({A : Type} → Dec A)
¬-excluded-middle =
  ({A : Type} → Dec A)                                             ↝⟨ (λ em ¬¬a → [ id , ⊥-elim ∘ ¬¬a ] em) ⟩
  ({A : Type} → ¬ ¬ A → A)                                         ↝⟨ (λ dne → flip _$_ ∘ (dne ∘_)) ⟩
  ({P : 𝕊¹ → Type} → ((x : 𝕊¹) → ¬ ¬ P x) → ¬ ¬ ((x : 𝕊¹) → P x))  ↝⟨ ¬-double-negation-shift ⟩□
  ⊥                                                                □

-- H-level.Closure.proj₁-closure cannot be generalised by replacing
-- the assumption ∀ a → B a with ∀ a → ∥ B a ∥.
--
-- This observation is due to Andrea Vezzosi.

¬-generalised-proj₁-closure :
  ¬ ({A : Type} {B : A → Type} →
     (∀ a → ∥ B a ∥) →
     ∀ n → H-level n (Σ A B) → H-level n A)
¬-generalised-proj₁-closure generalised-proj₁-closure =
                                 $⟨ singleton-contractible _ ⟩
  Contractible (Σ 𝕊¹ (_≡ base))  ↝⟨ generalised-proj₁-closure
                                      all-points-on-the-circle-are-merely-equal
                                      0 ⟩
  Contractible 𝕊¹                ↝⟨ mono (zero≤ 2) ⟩
  Is-set 𝕊¹                      ↝⟨ ¬-𝕊¹-set ⟩□
  ⊥                              □

-- There is no based equivalence between the circle and the product of
-- the circle with itself.
--
-- This result was pointed out to me by Paolo Capriotti.

𝕊¹≄ᴮ𝕊¹×𝕊¹ : ¬ (𝕊¹ , base) ≃ᴮ ((𝕊¹ , base) PT.× (𝕊¹ , base))
𝕊¹≄ᴮ𝕊¹×𝕊¹ =
  E.Stable-¬
    E.[ (𝕊¹ , base) ≃ᴮ ((𝕊¹ , base) PT.× (𝕊¹ , base))                      ↝⟨ ≃ᴮ→≃ᴳ (𝕊¹ , base) ((𝕊¹ , base) PT.× (𝕊¹ , base)) 0 ⟩

        Fundamental-group (𝕊¹ , base) ≃ᴳ
        Fundamental-group ((𝕊¹ , base) PT.× (𝕊¹ , base))                   ↝⟨ flip G.↝ᴳ-trans (Homotopy-group-[1+ 0 ]-× (𝕊¹ , base) (𝕊¹ , base)) ⟩

        Fundamental-group (𝕊¹ , base) ≃ᴳ
        (Fundamental-group (𝕊¹ , base) G.× Fundamental-group (𝕊¹ , base))  ↝⟨ flip G.↝ᴳ-trans
                                                                                (G.↝-× (Fundamental-group≃ℤ univ) (Fundamental-group≃ℤ univ)) ∘
                                                                              G.↝ᴳ-trans (G.≃ᴳ-sym (Fundamental-group≃ℤ univ)) ⟩

        ℤ-group ≃ᴳ (ℤ-group G.× ℤ-group)                                   ↝⟨ C.ℤ≄ᴳℤ×ℤ ⟩□

        ⊥                                                                  □
      ]

-- 𝕊¹ is not equivalent to 𝕊¹ × 𝕊¹.
--
-- This result was pointed out to me by Paolo Capriotti.

𝕊¹≄𝕊¹×𝕊¹ : ¬ 𝕊¹ ≃ (𝕊¹ × 𝕊¹)
𝕊¹≄𝕊¹×𝕊¹ hyp =
  let x , y = _≃_.to hyp base in
  all-points-on-the-circle-are-¬¬-equal x λ x≡base →
  all-points-on-the-circle-are-¬¬-equal y λ y≡base →
  𝕊¹≄ᴮ𝕊¹×𝕊¹ (hyp , cong₂ _,_ x≡base y≡base)

------------------------------------------------------------------------
-- An alternative approach to defining eliminators and proving
-- computation rules for arbitrary notions of equality, based on an
-- anonymous reviewer's suggestion

-- Circle eq p is an axiomatisation of the circle, for the given
-- notion of equality eq, eliminating into Type p.
--
-- Note that the statement of the computation rule for "loop" is more
-- complicated than above (elim-loop). The reason is that the
-- computation rule for "base" does not hold definitionally.

Circle :
  ∀ {e⁺} →
  (∀ {a p} → P.Equality-with-paths a p e⁺) →
  (p : Level) → Type (lsuc p)
Circle eq p =
  ∃ λ (𝕊¹ : Type) →
  ∃ λ (base : 𝕊¹) →
  ∃ λ (loop : base ≡.≡ base) →
    (P : 𝕊¹ → Type p)
    (b : P base)
    (ℓ : ≡.subst P loop b ≡.≡ b) →
    ∃ λ (elim : (x : 𝕊¹) → P x) →
    ∃ λ (elim-base : elim base ≡.≡ b) →
      ≡.subst (λ b → ≡.subst P loop b ≡.≡ b)
              elim-base
              (≡.dcong elim loop)
        ≡.≡
      ℓ
  where
  module ≡ = P.Derived-definitions-and-properties eq

-- A circle defined for paths (P.equality-with-J) is equivalent to one
-- defined for eq.

Circle≃Circle : Circle P.equality-with-paths p ≃ Circle eq p
Circle≃Circle =
  ∃-cong λ _ →
  ∃-cong λ _ →
  Σ-cong (inverse ≡↔≡) λ loop →
  ∀-cong ext λ P →
  ∀-cong ext λ b →
  Π-cong-contra ext subst≡↔subst≡ λ ℓ →
  ∃-cong λ f →
  Σ-cong (inverse ≡↔≡) λ f-base →
  let lemma = P.elim¹
        (λ eq → _↔_.from subst≡↔subst≡
                  (P.subst
                     (λ b → P.subst P loop b P.≡ b)
                     eq
                     (P.dcong f loop)) ≡
                P.subst
                  (λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b)
                  eq
                  (_↔_.from subst≡↔subst≡ (P.dcong f loop)))
        (_↔_.from subst≡↔subst≡
           (P.subst
              (λ b → P.subst P loop b P.≡ b)
              P.refl
              (P.dcong f loop))                       ≡⟨ cong (_↔_.from subst≡↔subst≡) $ _↔_.from ≡↔≡ $
                                                         P.subst-refl (λ b → P.subst P loop b P.≡ b) _ ⟩

         _↔_.from subst≡↔subst≡ (P.dcong f loop)      ≡⟨ sym $ _↔_.from ≡↔≡ $
                                                         P.subst-refl (λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b) _ ⟩∎
         P.subst
           (λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b)
           P.refl
           (_↔_.from subst≡↔subst≡ (P.dcong f loop))  ∎)
        _
  in
  P.subst
    (λ b → P.subst P loop b P.≡ b)
    f-base
    (P.dcong f loop) P.≡
  _↔_.to subst≡↔subst≡ ℓ                           ↔⟨ ≡↔≡ F.∘ inverse (from≡↔≡to (Eq.↔⇒≃ subst≡↔subst≡)) F.∘ inverse ≡↔≡ ⟩

  _↔_.from subst≡↔subst≡
    (P.subst
       (λ b → P.subst P loop b P.≡ b)
       f-base
       (P.dcong f loop)) P.≡
  ℓ                                                ↝⟨ ≡⇒↝ _ (cong (P._≡ _) lemma) ⟩

  P.subst
    (λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b)
    f-base
    (_↔_.from subst≡↔subst≡ (P.dcong f loop)) P.≡
  ℓ                                                ↝⟨ ≡⇒↝ _ $ cong (λ eq → P.subst (λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b) f-base eq P.≡ ℓ) $
                                                      _↔_.from-to (inverse subst≡↔subst≡) dcong≡dcong ⟩
  P.subst
    (λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b)
    f-base
    (dcong f (_↔_.from ≡↔≡ loop)) P.≡
  ℓ                                                ↔⟨ inverse subst≡↔subst≡ ⟩□

  subst
    (λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b)
    (_↔_.from ≡↔≡ f-base)
    (dcong f (_↔_.from ≡↔≡ loop)) ≡
  ℓ                                                □

-- An implemention of the circle for paths (P.equality-with-paths).

circleᴾ : Circle P.equality-with-paths p
circleᴾ =
    𝕊¹
  , base
  , loopᴾ
  , λ P b ℓ →
      let elim = elimᴾ P b (PI.subst≡→[]≡ {B = P} ℓ)
      in
        elim
      , P.refl
      , (P.subst (λ b → P.subst P loopᴾ b P.≡ b) P.refl
           (P.dcong elim loopᴾ)                          P.≡⟨ P.subst-refl (λ b → P.subst P loopᴾ b P.≡ b) _ ⟩

         P.dcong elim loopᴾ                              P.≡⟨ PI.dcong-subst≡→[]≡ {f = elim} {eq₂ = ℓ} P.refl ⟩∎

         ℓ                                               ∎)

-- An implementation of the circle for eq.

circle : Circle eq p
circle = _≃_.to Circle≃Circle circleᴾ

-- The latter implementation computes in the right way for "base".

_ :
  let _ , base′ , _ , elim′ = circle {p = p} in
  ∀ {P b ℓ} →
  proj₁ (elim′ P b ℓ) base′ ≡ b
_ = refl _

-- The usual computation rule for "loop" can be derived.

elim-loop-circle :
  let _ , _ , loop′ , elim′ = circle {p = p} in
  ∀ {P b ℓ} →
  dcong (proj₁ (elim′ P b ℓ)) loop′ ≡ ℓ
elim-loop-circle {P = P} {b = b} {ℓ = ℓ} =
  let _ , _ , loop′ , elim′           = circle
      elim″ , elim″-base , elim″-loop = elim′ P b ℓ

      lemma =
        refl _               ≡⟨ sym from-≡↔≡-refl ⟩
        _↔_.from ≡↔≡ P.refl  ≡⟨⟩
        elim″-base           ∎
  in
  dcong elim″ loop′                                                 ≡⟨ sym $ subst-refl _ _ ⟩
  subst (λ b → subst P loop′ b ≡ b) (refl _) (dcong elim″ loop′)    ≡⟨ cong (λ eq → subst (λ b → subst P loop′ b ≡ b) eq (dcong elim″ loop′)) lemma ⟩
  subst (λ b → subst P loop′ b ≡ b) elim″-base (dcong elim″ loop′)  ≡⟨ elim″-loop ⟩∎
  ℓ                                                                 ∎

-- An alternative to Circle≃Circle that does not give the "right"
-- computational behaviour for circle′ below.

Circle≃Circle′ : Circle P.equality-with-paths p ≃ Circle eq p
Circle≃Circle′ =
  ∃-cong λ _ →
  ∃-cong λ _ →
  Σ-cong (inverse ≡↔≡) λ loop →
  ∀-cong ext λ P →
  ∀-cong ext λ b →
  Π-cong ext (inverse subst≡↔subst≡) λ ℓ →
  ∃-cong λ f →
  Σ-cong (inverse ≡↔≡) λ f-base →
  let lemma = P.elim¹
        (λ eq → _↔_.from subst≡↔subst≡
                  (P.subst
                     (λ b → P.subst P loop b P.≡ b)
                     eq
                     (P.dcong f loop)) ≡
                P.subst
                  (λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b)
                  eq
                  (_↔_.from subst≡↔subst≡ (P.dcong f loop)))
        (_↔_.from subst≡↔subst≡
           (P.subst
              (λ b → P.subst P loop b P.≡ b)
              P.refl
              (P.dcong f loop))                       ≡⟨ cong (_↔_.from subst≡↔subst≡) $ _↔_.from ≡↔≡ $
                                                         P.subst-refl (λ b → P.subst P loop b P.≡ b) _ ⟩

         _↔_.from subst≡↔subst≡ (P.dcong f loop)      ≡⟨ sym $ _↔_.from ≡↔≡ $
                                                         P.subst-refl (λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b) _ ⟩∎
         P.subst
           (λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b)
           P.refl
           (_↔_.from subst≡↔subst≡ (P.dcong f loop))  ∎)
        _
  in
  P.subst
    (λ b → P.subst P loop b P.≡ b)
    f-base
    (P.dcong f loop) P.≡
  ℓ                                                ↔⟨ ≡↔≡ F.∘ from-isomorphism (inverse $ Eq.≃-≡ $ Eq.↔⇒≃ $ inverse subst≡↔subst≡) F.∘ inverse ≡↔≡ ⟩

  _↔_.from subst≡↔subst≡
    (P.subst
       (λ b → P.subst P loop b P.≡ b)
       f-base
       (P.dcong f loop)) P.≡
  _↔_.from subst≡↔subst≡ ℓ                         ↝⟨ ≡⇒↝ _ (cong (P._≡ _↔_.from subst≡↔subst≡ ℓ) lemma) ⟩

  P.subst
    (λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b)
    f-base
    (_↔_.from subst≡↔subst≡ (P.dcong f loop)) P.≡
  _↔_.from subst≡↔subst≡ ℓ                         ↝⟨ ≡⇒↝ _ $ cong (λ eq → P.subst (λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b) f-base eq P.≡ _↔_.from subst≡↔subst≡ ℓ) $
                                                      _↔_.from-to (inverse subst≡↔subst≡) dcong≡dcong ⟩
  P.subst
    (λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b)
    f-base
    (dcong f (_↔_.from ≡↔≡ loop)) P.≡
  _↔_.from subst≡↔subst≡ ℓ                         ↔⟨ inverse subst≡↔subst≡ ⟩□

  subst
    (λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b)
    (_↔_.from ≡↔≡ f-base)
    (dcong f (_↔_.from ≡↔≡ loop)) ≡
  _↔_.from subst≡↔subst≡ ℓ                         □

-- An alternative implementation of the circle for eq.

circle′ : Circle eq p
circle′ = _≃_.to Circle≃Circle′ circleᴾ

-- This implementation does not compute in the right way for "base".
-- The following code is (at the time of writing) rejected by Agda.

-- _ :
--   let _ , base′ , _ , elim′ = circle′ {p = p} in
--   ∀ {P b ℓ} →
--   proj₁ (elim′ P b ℓ) base′ ≡ b
-- _ = refl _