text:
{-# OPTIONS --without-K --exact-split --safe #-}

module 07-finite-sets where

import 06-universes
open 06-universes public

--------------------------------------------------------------------------------

{- Section 7.1 The congruence relations -}

{- Definition 7.1.1 -}

-- We introduce the divisibility relation. --

div-ℕ : ℕ → ℕ → UU lzero
div-ℕ m n = Σ ℕ (λ k → Id (mul-ℕ k m) n)

{- Proposition 7.1.2 -}

{- In the following three constructions we show that if any two of the three
   numbers x, y, and x + y, is divisible by d, then so is the third. -}

div-add-ℕ :
  (d x y : ℕ) → div-ℕ d x → div-ℕ d y → div-ℕ d (add-ℕ x y)
div-add-ℕ d x y (pair n p) (pair m q) =
  pair
    ( add-ℕ n m)
    ( ( right-distributive-mul-add-ℕ n m d) ∙
      ( ap-add-ℕ p q))

div-left-summand-ℕ :
  (d x y : ℕ) → div-ℕ d y → div-ℕ d (add-ℕ x y) → div-ℕ d x
div-left-summand-ℕ zero-ℕ x y (pair m q) (pair n p) =
  pair zero-ℕ
    ( ( inv (right-zero-law-mul-ℕ n)) ∙
      ( p ∙ (ap (add-ℕ x) ((inv q) ∙ (right-zero-law-mul-ℕ m)))))
div-left-summand-ℕ (succ-ℕ d) x y (pair m q) (pair n p) =
  pair
    ( dist-ℕ m n)
    ( is-injective-add-ℕ (mul-ℕ m (succ-ℕ d)) (mul-ℕ (dist-ℕ m n) (succ-ℕ d)) x
      ( ( inv
          ( ( right-distributive-mul-add-ℕ m (dist-ℕ m n) (succ-ℕ d)) ∙
            ( commutative-add-ℕ
              ( mul-ℕ m (succ-ℕ d))
              ( mul-ℕ (dist-ℕ m n) (succ-ℕ d))))) ∙
        ( ( ap
            ( mul-ℕ' (succ-ℕ d))
            ( leq-dist-ℕ m n
              ( leq-leq-mul-ℕ' m n d
                ( concatenate-eq-leq-eq-ℕ q
                  ( leq-add-ℕ' y x)
                  ( inv p))))) ∙
          ( p ∙ (ap (add-ℕ x) (inv q))))))

div-right-summand-ℕ :
  (d x y : ℕ) → div-ℕ d x → div-ℕ d (add-ℕ x y) → div-ℕ d y
div-right-summand-ℕ d x y H1 H2 =
  div-left-summand-ℕ d y x H1 (tr (div-ℕ d) (commutative-add-ℕ x y) H2)

{- Definition 7.1.3 -}

{- We define the congruence relation on ℕ and we do some bureaucracy that will
   help us in calculations involving the congruence relations. -}

cong-ℕ :
  ℕ → ℕ → ℕ → UU lzero
cong-ℕ k x y = div-ℕ k (dist-ℕ x y)

_≡_mod_ : ℕ → ℕ → ℕ → UU lzero
x ≡ y mod k = cong-ℕ k x y

concatenate-eq-cong-eq-ℕ :
  (k : ℕ) {x1 x2 x3 x4 : ℕ} →
  Id x1 x2 → cong-ℕ k x2 x3 → Id x3 x4 → cong-ℕ k x1 x4
concatenate-eq-cong-eq-ℕ k refl H refl = H

concatenate-eq-cong-ℕ :
  (k : ℕ) {x1 x2 x3 : ℕ} →
  Id x1 x2 → cong-ℕ k x2 x3 → cong-ℕ k x1 x3
concatenate-eq-cong-ℕ k refl H = H

concatenate-cong-eq-ℕ :
  (k : ℕ) {x1 x2 x3 : ℕ} →
  cong-ℕ k x1 x2 → Id x2 x3 → cong-ℕ k x1 x3
concatenate-cong-eq-ℕ k H refl = H

{- Proposition 7.1.4 -}

-- We show that cong-ℕ is an equivalence relation.

reflexive-cong-ℕ :
  (k x : ℕ) → cong-ℕ k x x
reflexive-cong-ℕ k x =
  pair zero-ℕ ((left-zero-law-mul-ℕ (succ-ℕ k)) ∙ (dist-eq-ℕ x x refl))

cong-identification-ℕ :
  (k : ℕ) {x y : ℕ} → Id x y → cong-ℕ k x y
cong-identification-ℕ k {x} refl = reflexive-cong-ℕ k x

symmetric-cong-ℕ :
  (k x y : ℕ) → cong-ℕ k x y → cong-ℕ k y x
symmetric-cong-ℕ k x y (pair d p) =
  pair d (p ∙ (symmetric-dist-ℕ x y))

{- Before we show that cong-ℕ is transitive, we give some lemmas that will help
   us showing that cong is an equivalence relation. They are basically
   bureaucracy, manipulating already known facts. -}

-- Three elements can be ordered in 6 possible ways

cases-order-three-elements-ℕ :
  (x y z : ℕ) → UU lzero
cases-order-three-elements-ℕ x y z =
  coprod
    ( coprod ((leq-ℕ x y) × (leq-ℕ y z)) ((leq-ℕ x z) × (leq-ℕ z y)))
    ( coprod
      ( coprod ((leq-ℕ y z) × (leq-ℕ z x)) ((leq-ℕ y x) × (leq-ℕ x z)))
      ( coprod ((leq-ℕ z x) × (leq-ℕ x y)) ((leq-ℕ z y) × (leq-ℕ y x))))

order-three-elements-ℕ :
  (x y z : ℕ) → cases-order-three-elements-ℕ x y z
order-three-elements-ℕ zero-ℕ zero-ℕ zero-ℕ = inl (inl (pair star star))
order-three-elements-ℕ zero-ℕ zero-ℕ (succ-ℕ z) = inl (inl (pair star star))
order-three-elements-ℕ zero-ℕ (succ-ℕ y) zero-ℕ = inl (inr (pair star star))
order-three-elements-ℕ zero-ℕ (succ-ℕ y) (succ-ℕ z) =
  inl (functor-coprod (pair star) (pair star) (decide-leq-ℕ y z))
order-three-elements-ℕ (succ-ℕ x) zero-ℕ zero-ℕ =
  inr (inl (inl (pair star star)))
order-three-elements-ℕ (succ-ℕ x) zero-ℕ (succ-ℕ z) =
  inr (inl (functor-coprod (pair star) (pair star) (decide-leq-ℕ z x)))
order-three-elements-ℕ (succ-ℕ x) (succ-ℕ y) zero-ℕ =
  inr (inr (functor-coprod (pair star) (pair star) (decide-leq-ℕ x y)))
order-three-elements-ℕ (succ-ℕ x) (succ-ℕ y) (succ-ℕ z) =
  order-three-elements-ℕ x y z

{- We show that the distances of any three elements always add up, when they
   are added up in the right way :) -}

cases-dist-ℕ :
  (x y z : ℕ) → UU lzero
cases-dist-ℕ x y z =
  coprod
    ( Id (add-ℕ (dist-ℕ x y) (dist-ℕ y z)) (dist-ℕ x z))
    ( coprod
      ( Id (add-ℕ (dist-ℕ y z) (dist-ℕ x z)) (dist-ℕ x y))
      ( Id (add-ℕ (dist-ℕ x z) (dist-ℕ x y)) (dist-ℕ y z)))

is-total-dist-ℕ :
  (x y z : ℕ) → cases-dist-ℕ x y z
is-total-dist-ℕ x y z with order-three-elements-ℕ x y z
is-total-dist-ℕ x y z | inl (inl (pair H1 H2)) =
  inl (triangle-equality-dist-ℕ x y z H1 H2)
is-total-dist-ℕ x y z | inl (inr (pair H1 H2)) =
  inr
    ( inl
      ( ( commutative-add-ℕ (dist-ℕ y z) (dist-ℕ x z)) ∙
        ( ( ap (add-ℕ (dist-ℕ x z)) (symmetric-dist-ℕ y z)) ∙
          ( triangle-equality-dist-ℕ x z y H1 H2))))
is-total-dist-ℕ x y z | inr (inl (inl (pair H1 H2))) =
  inr
    ( inl
      ( ( ap (add-ℕ (dist-ℕ y z)) (symmetric-dist-ℕ x z)) ∙
        ( ( triangle-equality-dist-ℕ y z x H1 H2) ∙
          ( symmetric-dist-ℕ y x))))
is-total-dist-ℕ x y z | inr (inl (inr (pair H1 H2))) =
  inr
    ( inr
      ( ( ap (add-ℕ (dist-ℕ x z)) (symmetric-dist-ℕ x y)) ∙
        ( ( commutative-add-ℕ (dist-ℕ x z) (dist-ℕ y x)) ∙
          ( triangle-equality-dist-ℕ y x z H1 H2))))
is-total-dist-ℕ x y z | inr (inr (inl (pair H1 H2))) =
  inr
    ( inr
      ( ( ap (add-ℕ' (dist-ℕ x y)) (symmetric-dist-ℕ x z)) ∙
        ( ( triangle-equality-dist-ℕ z x y H1 H2) ∙
          ( symmetric-dist-ℕ z y))))
is-total-dist-ℕ x y z | inr (inr (inr (pair H1 H2))) =
  inl
    ( ( ap-add-ℕ (symmetric-dist-ℕ x y) (symmetric-dist-ℕ y z)) ∙
      ( ( commutative-add-ℕ (dist-ℕ y x) (dist-ℕ z y)) ∙
        ( ( triangle-equality-dist-ℕ z y x H1 H2) ∙
          ( symmetric-dist-ℕ z x))))

-- Finally, we show that cong-ℕ is transitive.

transitive-cong-ℕ :
  (k x y z : ℕ) →
  cong-ℕ k x y → cong-ℕ k y z → cong-ℕ k x z
transitive-cong-ℕ k x y z d e with is-total-dist-ℕ x y z
transitive-cong-ℕ k x y z d e | inl α =
  tr (div-ℕ k) α (div-add-ℕ k (dist-ℕ x y) (dist-ℕ y z) d e)
transitive-cong-ℕ k x y z d e | inr (inl α) =
  div-right-summand-ℕ k (dist-ℕ y z) (dist-ℕ x z) e (tr (div-ℕ k) (inv α) d)
transitive-cong-ℕ k x y z d e | inr (inr α) =
  div-left-summand-ℕ k (dist-ℕ x z) (dist-ℕ x y) d (tr (div-ℕ k) (inv α) e)

concatenate-cong-eq-cong-ℕ :
  {k x1 x2 x3 x4 : ℕ} →
  cong-ℕ k x1 x2 → Id x2 x3 → cong-ℕ k x3 x4 → cong-ℕ k x1 x4
concatenate-cong-eq-cong-ℕ {k} {x} {y} {.y} {z} H refl K =
  transitive-cong-ℕ k x y z H K

concatenate-eq-cong-eq-cong-eq-ℕ :
  (k : ℕ) {x1 x2 x3 x4 x5 x6 : ℕ} →
  Id x1 x2 → cong-ℕ k x2 x3 → Id x3 x4 →
  cong-ℕ k x4 x5 → Id x5 x6 → cong-ℕ k x1 x6
concatenate-eq-cong-eq-cong-eq-ℕ k {x} {.x} {y} {.y} {z} {.z} refl H refl K refl =
  transitive-cong-ℕ k x y z H K

{- Remark 7.1.6 (this is also Exercise 7.2) -}

-- We show that cong-ℕ one-ℕ is the indiscrete equivalence relation --

div-one-ℕ :
  (x : ℕ) → div-ℕ one-ℕ x
div-one-ℕ x = pair x (right-unit-law-mul-ℕ x)

is-indiscrete-cong-one-ℕ :
  (x y : ℕ) → cong-ℕ one-ℕ x y
is-indiscrete-cong-one-ℕ x y = div-one-ℕ (dist-ℕ x y)

-- We show that the congruence relation modulo 0 is discrete

div-zero-ℕ :
  (k : ℕ) → div-ℕ k zero-ℕ
div-zero-ℕ k = pair zero-ℕ (left-zero-law-mul-ℕ k)

is-discrete-cong-zero-ℕ :
  (x y : ℕ) → cong-ℕ zero-ℕ x y → Id x y
is-discrete-cong-zero-ℕ x y (pair k p) =
  eq-dist-ℕ x y ((inv (right-zero-law-mul-ℕ k)) ∙ p)

-- We show that d | 1 if and only if d = 1.

-- We show that 0 | x if and only if x = 0.

-- We show that zero-ℕ is congruent to n modulo n.

cong-zero-ℕ :
  (k : ℕ) → cong-ℕ k k zero-ℕ
cong-zero-ℕ k =
  pair one-ℕ ((left-unit-law-mul-ℕ k) ∙ (inv (right-zero-law-dist-ℕ k)))

cong-zero-ℕ' :
  (k : ℕ) → cong-ℕ k zero-ℕ k
cong-zero-ℕ' k =
  symmetric-cong-ℕ k k zero-ℕ (cong-zero-ℕ k)

--------------------------------------------------------------------------------

{- Section 7.2 The finite types -}

{- Definition 7.2.1 -}

-- We introduce the finite types as a family indexed by ℕ.

Fin : ℕ → UU lzero
Fin zero-ℕ = empty
Fin (succ-ℕ k) = coprod (Fin k) unit

inl-Fin :
  (k : ℕ) → Fin k → Fin (succ-ℕ k)
inl-Fin k = inl

neg-one-Fin : {k : ℕ} → Fin (succ-ℕ k)
neg-one-Fin {k} = inr star

{- Definition 7.2.4 -}

-- We define the inclusion of Fin k into ℕ.

nat-Fin : {k : ℕ} → Fin k → ℕ
nat-Fin {succ-ℕ k} (inl x) = nat-Fin x
nat-Fin {succ-ℕ k} (inr x) = k

{- Lemma 7.2.5 -}

-- We show that nat-Fin is bounded

strict-upper-bound-nat-Fin : {k : ℕ} (x : Fin k) → le-ℕ (nat-Fin x) k
strict-upper-bound-nat-Fin {succ-ℕ k} (inl x) =
  transitive-le-ℕ
    ( nat-Fin x)
    ( k)
    ( succ-ℕ k)
    ( strict-upper-bound-nat-Fin x)
    ( succ-le-ℕ k)
strict-upper-bound-nat-Fin {succ-ℕ k} (inr star) =
  succ-le-ℕ k

-- We also give a non-strict upper bound for convenience

upper-bound-nat-Fin : {k : ℕ} (x : Fin (succ-ℕ k)) → leq-ℕ (nat-Fin x) k
upper-bound-nat-Fin {zero-ℕ} (inr star) = star
upper-bound-nat-Fin {succ-ℕ k} (inl x) =
  preserves-leq-succ-ℕ (nat-Fin x) k (upper-bound-nat-Fin x)
upper-bound-nat-Fin {succ-ℕ k} (inr star) = reflexive-leq-ℕ (succ-ℕ k)

{- Proposition 7.2.6 -}

-- We show that nat-Fin is an injective function

neq-le-ℕ : {x y : ℕ} → le-ℕ x y → ¬ (Id x y)
neq-le-ℕ {zero-ℕ} {succ-ℕ y} H = Peano-8 y
neq-le-ℕ {succ-ℕ x} {succ-ℕ y} H p = neq-le-ℕ H (is-injective-succ-ℕ x y p)

is-injective-nat-Fin : {k : ℕ} {x y : Fin k} →
  Id (nat-Fin x) (nat-Fin y) → Id x y
is-injective-nat-Fin {succ-ℕ k} {inl x} {inl y} p =
  ap inl (is-injective-nat-Fin p)
is-injective-nat-Fin {succ-ℕ k} {inl x} {inr star} p =
  ex-falso (neq-le-ℕ (strict-upper-bound-nat-Fin x) p)
is-injective-nat-Fin {succ-ℕ k} {inr star} {inl y} p =
  ex-falso (neq-le-ℕ (strict-upper-bound-nat-Fin y) (inv p))
is-injective-nat-Fin {succ-ℕ k} {inr star} {inr star} p =
  refl

{- Definition 7.2.7 -}

-- We define the zero element of Fin k.

zero-Fin : {k : ℕ} → Fin (succ-ℕ k)
zero-Fin {zero-ℕ} = inr star
zero-Fin {succ-ℕ k} = inl zero-Fin

-- We define a function skip-zero-Fin in order to define succ-Fin.

skip-zero-Fin : {k : ℕ} → Fin k → Fin (succ-ℕ k)
skip-zero-Fin {succ-ℕ k} (inl x) = inl (skip-zero-Fin x)
skip-zero-Fin {succ-ℕ k} (inr star) = inr star

-- We define the successor function on Fin k.

succ-Fin : {k : ℕ} → Fin k → Fin k
succ-Fin {succ-ℕ k} (inl x) = skip-zero-Fin x
succ-Fin {succ-ℕ k} (inr star) = zero-Fin

{- Definition 7.2.8 -}

-- We define the negative two element of Fin k.

neg-two-Fin :
  {k : ℕ} → Fin (succ-ℕ k)
neg-two-Fin {zero-ℕ} = inr star
neg-two-Fin {succ-ℕ k} = inl (inr star)

-- We define a function skip-neg-two-Fin in order to define pred-Fin.

skip-neg-two-Fin :
  {k : ℕ} → Fin k → Fin (succ-ℕ k)
skip-neg-two-Fin {succ-ℕ k} (inl x) = inl (inl x)
skip-neg-two-Fin {succ-ℕ k} (inr x) = neg-one-Fin {succ-ℕ k}

-- We define the predecessor function on Fin k.

pred-Fin : {k : ℕ} → Fin k → Fin k
pred-Fin {succ-ℕ k} (inl x) = skip-neg-two-Fin (pred-Fin x)
pred-Fin {succ-ℕ k} (inr x) = neg-two-Fin

{- Definition 7.2.9 -}

-- We define the modulo function

mod-succ-ℕ : (k : ℕ) → ℕ → Fin (succ-ℕ k)
mod-succ-ℕ k zero-ℕ = zero-Fin
mod-succ-ℕ k (succ-ℕ n) = succ-Fin (mod-succ-ℕ k n)

mod-two-ℕ : ℕ → Fin two-ℕ
mod-two-ℕ = mod-succ-ℕ one-ℕ

mod-three-ℕ : ℕ → Fin three-ℕ
mod-three-ℕ = mod-succ-ℕ two-ℕ

{- Lemma 7.2.10 -}

successor-law-mod-succ-ℕ :
  (k x : ℕ) → leq-ℕ x k →
  Id (mod-succ-ℕ (succ-ℕ k) x) (inl (mod-succ-ℕ k x))
successor-law-mod-succ-ℕ k zero-ℕ star = refl
successor-law-mod-succ-ℕ (succ-ℕ k) (succ-ℕ x) p =
  ( ( ap succ-Fin
      ( successor-law-mod-succ-ℕ (succ-ℕ k) x
        ( preserves-leq-succ-ℕ x k p))) ∙
    ( ap succ-Fin (ap inl (successor-law-mod-succ-ℕ k x p)))) ∙
  ( ap inl (ap succ-Fin (inv (successor-law-mod-succ-ℕ k x p))))

{- Corollary 7.2.11 -}

neg-one-law-mod-succ-ℕ :
  (k : ℕ) → Id (mod-succ-ℕ k k) neg-one-Fin
neg-one-law-mod-succ-ℕ zero-ℕ = refl
neg-one-law-mod-succ-ℕ (succ-ℕ k) =
  ap succ-Fin
    ( ( successor-law-mod-succ-ℕ k k (reflexive-leq-ℕ k)) ∙
      ( ap inl (neg-one-law-mod-succ-ℕ k)))

base-case-is-periodic-mod-succ-ℕ :
  (k : ℕ) → Id (mod-succ-ℕ k (succ-ℕ k)) zero-Fin
base-case-is-periodic-mod-succ-ℕ zero-ℕ = refl
base-case-is-periodic-mod-succ-ℕ (succ-ℕ k) =
  ap succ-Fin (neg-one-law-mod-succ-ℕ (succ-ℕ k))

{- Theorem 7.2.12 -}

-- Now we show that Fin (succ-ℕ k) is a retract of ℕ

issec-nat-Fin : (k : ℕ) (x : Fin (succ-ℕ k)) → Id (mod-succ-ℕ k (nat-Fin x)) x
issec-nat-Fin zero-ℕ (inr star) = refl
issec-nat-Fin (succ-ℕ k) (inl x) =
  ( successor-law-mod-succ-ℕ k (nat-Fin x) (upper-bound-nat-Fin x)) ∙
  ( ap inl (issec-nat-Fin k x))
issec-nat-Fin (succ-ℕ k) (inr star) = neg-one-law-mod-succ-ℕ (succ-ℕ k)

--------------------------------------------------------------------------------

{- Section 7.3 The effectiveness theorem of modular arithmetic -}

{- Lemma 7.3.1 -}

-- We prove three things to help calculating with nat-Fin.

nat-zero-Fin :
  {k : ℕ} → Id (nat-Fin (zero-Fin {k})) zero-ℕ
nat-zero-Fin {zero-ℕ} = refl
nat-zero-Fin {succ-ℕ k} = nat-zero-Fin {k}

nat-skip-zero-Fin :
  {k : ℕ} (x : Fin k) → Id (nat-Fin (skip-zero-Fin x)) (succ-ℕ (nat-Fin x))
nat-skip-zero-Fin {succ-ℕ k} (inl x) = nat-skip-zero-Fin x
nat-skip-zero-Fin {succ-ℕ k} (inr star) = refl

cong-nat-succ-Fin :
  (k : ℕ) (x : Fin k) → cong-ℕ k (nat-Fin (succ-Fin x)) (succ-ℕ (nat-Fin x))
cong-nat-succ-Fin (succ-ℕ k) (inl x) =
  cong-identification-ℕ
    ( succ-ℕ k)
    { nat-Fin (succ-Fin (inl x))}
    { succ-ℕ (nat-Fin x)}
    ( nat-skip-zero-Fin x)
cong-nat-succ-Fin (succ-ℕ k) (inr star) =
  concatenate-eq-cong-ℕ
    ( succ-ℕ k)
    { nat-Fin {succ-ℕ k} zero-Fin}
    { zero-ℕ}
    { succ-ℕ k}
    ( nat-zero-Fin {k})
    ( cong-zero-ℕ' (succ-ℕ k))

{- Corollary 7.3.2 -}

-- We show that (nat-Fin (mod-succ-ℕ n x)) is congruent to x modulo n+1. --

cong-nat-mod-succ-ℕ :
  (k x : ℕ) → cong-ℕ (succ-ℕ k) (nat-Fin (mod-succ-ℕ k x)) x
cong-nat-mod-succ-ℕ k zero-ℕ =
  cong-identification-ℕ (succ-ℕ k) (nat-zero-Fin {k})
cong-nat-mod-succ-ℕ k (succ-ℕ x) =
  transitive-cong-ℕ
    ( succ-ℕ k)
    ( nat-Fin (mod-succ-ℕ k (succ-ℕ x)))
    ( succ-ℕ (nat-Fin (mod-succ-ℕ k x)))
    ( succ-ℕ x)
    ( cong-nat-succ-Fin (succ-ℕ k) (mod-succ-ℕ k x) )
    ( cong-nat-mod-succ-ℕ k x)

{- Proposition 7.3.4 -}

contradiction-leq-ℕ :
  (x y : ℕ) → leq-ℕ x y → leq-ℕ (succ-ℕ y) x → empty
contradiction-leq-ℕ (succ-ℕ x) (succ-ℕ y) H K = contradiction-leq-ℕ x y H K

eq-zero-div-ℕ :
  (d x : ℕ) → leq-ℕ x d → div-ℕ (succ-ℕ d) x → Id x zero-ℕ
eq-zero-div-ℕ d zero-ℕ H D = refl
eq-zero-div-ℕ d (succ-ℕ x) H (pair (succ-ℕ k) p) =
  ex-falso
    ( contradiction-leq-ℕ d x
      ( concatenate-eq-leq-eq-ℕ
        { x1 = succ-ℕ d}
        { x2 = succ-ℕ d}
        { x3 = succ-ℕ (add-ℕ (mul-ℕ k (succ-ℕ d)) d)}
        { x4 = succ-ℕ x}
        ( refl)
        ( leq-add-ℕ' d (mul-ℕ k (succ-ℕ d)))
        ( p)) H)

{- Theorem 7.3.5 -}

{- We show that if mod-succ-ℕ k x = mod-succ-ℕ k y, then x and y must be
   congruent modulo succ-ℕ n. This is the forward direction of the theorm. -}

cong-eq-ℕ :
  (k x y : ℕ) → Id (mod-succ-ℕ k x) (mod-succ-ℕ k y) → cong-ℕ (succ-ℕ k) x y
cong-eq-ℕ k x y p =
  concatenate-cong-eq-cong-ℕ {succ-ℕ k} {x}
    ( symmetric-cong-ℕ (succ-ℕ k) (nat-Fin (mod-succ-ℕ k x)) x
      ( cong-nat-mod-succ-ℕ k x))
    ( ap nat-Fin p)
    ( cong-nat-mod-succ-ℕ k y)

eq-cong-nat-Fin :
  (k : ℕ) (x y : Fin k) → cong-ℕ k (nat-Fin x) (nat-Fin y) → Id x y
eq-cong-nat-Fin (succ-ℕ k) x y H =
  is-injective-nat-Fin
    ( eq-dist-ℕ
      ( nat-Fin x)
      ( nat-Fin y)
      ( inv
        ( eq-zero-div-ℕ k
          ( dist-ℕ (nat-Fin x) (nat-Fin y))
          ( upper-bound-dist-ℕ k
            ( nat-Fin x)
            ( nat-Fin y)
            ( upper-bound-nat-Fin x)
            ( upper-bound-nat-Fin y))
          ( H))))

eq-cong-ℕ :
  (k x y : ℕ) → cong-ℕ (succ-ℕ k) x y → Id (mod-succ-ℕ k x) (mod-succ-ℕ k y)
eq-cong-ℕ k x y H =
  eq-cong-nat-Fin
    ( succ-ℕ k)
    ( mod-succ-ℕ k x)
    ( mod-succ-ℕ k y)
    ( transitive-cong-ℕ
      ( succ-ℕ k)
      ( nat-Fin (mod-succ-ℕ k x))
      ( x)
      ( nat-Fin (mod-succ-ℕ k y))
      ( cong-nat-mod-succ-ℕ k x)
      ( transitive-cong-ℕ (succ-ℕ k) x y (nat-Fin (mod-succ-ℕ k y)) H
        ( symmetric-cong-ℕ (succ-ℕ k) (nat-Fin (mod-succ-ℕ k y)) y
          ( cong-nat-mod-succ-ℕ k y))))

--------------------------------------------------------------------------------

{- Section 7.4 The cyclic group structure on the finite types -}

{- Definition 7.4.1 -}

-- Addition on finite sets --

add-Fin : {k : ℕ} → Fin k → Fin k → Fin k
add-Fin {succ-ℕ k} x y = mod-succ-ℕ k (add-ℕ (nat-Fin x) (nat-Fin y))

add-Fin' : {k : ℕ} → Fin k → Fin k → Fin k
add-Fin' x y = add-Fin y x

-- We define an action on paths of add-Fin on the two arguments at once.

ap-add-Fin :
  {k : ℕ} {x y x' y' : Fin k} →
  Id x x' → Id y y' → Id (add-Fin x y) (add-Fin x' y')
ap-add-Fin refl refl = refl

-- The negative of an element of Fin k --

neg-Fin :
  {k : ℕ} → Fin k → Fin k
neg-Fin {succ-ℕ k} x =
  mod-succ-ℕ k (dist-ℕ (nat-Fin x) (succ-ℕ k))

{- Remark 7.4.2 -}

cong-nat-zero-Fin :
  {k : ℕ} → cong-ℕ (succ-ℕ k) (nat-Fin (zero-Fin {k})) zero-ℕ
cong-nat-zero-Fin {k} = cong-nat-mod-succ-ℕ k zero-ℕ

cong-add-Fin :
  {k : ℕ} (x y : Fin k) →
  cong-ℕ k (nat-Fin (add-Fin x y)) (add-ℕ (nat-Fin x) (nat-Fin y))
cong-add-Fin {succ-ℕ k} x y =
  cong-nat-mod-succ-ℕ k (add-ℕ (nat-Fin x) (nat-Fin y))

cong-neg-Fin :
  {k : ℕ} (x : Fin k) →
  cong-ℕ k (nat-Fin (neg-Fin x)) (dist-ℕ (nat-Fin x) k)
cong-neg-Fin {succ-ℕ k} x =
  cong-nat-mod-succ-ℕ k (dist-ℕ (nat-Fin x) (succ-ℕ k))

{- Proposition 7.4.3 -}

-- We show that congruence is translation invariant --

translation-invariant-cong-ℕ :
  (k x y z : ℕ) → cong-ℕ k x y → cong-ℕ k (add-ℕ z x) (add-ℕ z y)
translation-invariant-cong-ℕ k x y z (pair d p) =
  pair d (p ∙ inv (translation-invariant-dist-ℕ z x y))

translation-invariant-cong-ℕ' :
  (k x y z : ℕ) → cong-ℕ k x y → cong-ℕ k (add-ℕ x z) (add-ℕ y z)
translation-invariant-cong-ℕ' k x y z H =
  concatenate-eq-cong-eq-ℕ k
    ( commutative-add-ℕ x z)
    ( translation-invariant-cong-ℕ k x y z H)
    ( commutative-add-ℕ z y)

step-invariant-cong-ℕ :
  (k x y : ℕ) → cong-ℕ k x y → cong-ℕ k (succ-ℕ x) (succ-ℕ y)
step-invariant-cong-ℕ k x y = translation-invariant-cong-ℕ' k x y one-ℕ

-- We show that addition respects the congruence relation --

congruence-add-ℕ :
  (k : ℕ) {x y x' y' : ℕ} →
  cong-ℕ k x x' → cong-ℕ k y y' → cong-ℕ k (add-ℕ x y) (add-ℕ x' y')
congruence-add-ℕ k {x} {y} {x'} {y'} H K =
  transitive-cong-ℕ k (add-ℕ x y) (add-ℕ x y') (add-ℕ x' y')
    ( translation-invariant-cong-ℕ k y y' x K)
    ( translation-invariant-cong-ℕ' k x x' y' H)

{- Theorem 7.4.4 -}

-- We show that addition is commutative --

commutative-add-Fin : {k : ℕ} (x y : Fin k) → Id (add-Fin x y) (add-Fin y x)
commutative-add-Fin {succ-ℕ k} x y =
  ap (mod-succ-ℕ k) (commutative-add-ℕ (nat-Fin x) (nat-Fin y))

-- We show that addition is associative --

associative-add-Fin :
  {k : ℕ} (x y z : Fin k) →
  Id (add-Fin (add-Fin x y) z) (add-Fin x (add-Fin y z))
associative-add-Fin {succ-ℕ k} x y z =
  eq-cong-ℕ k
    ( add-ℕ (nat-Fin (add-Fin x y)) (nat-Fin z))
    ( add-ℕ (nat-Fin x) (nat-Fin (add-Fin y z)))
    ( concatenate-cong-eq-cong-ℕ
      { x1 = add-ℕ (nat-Fin (add-Fin x y)) (nat-Fin z)}
      { x2 = add-ℕ (add-ℕ (nat-Fin x) (nat-Fin y)) (nat-Fin z)}
      { x3 = add-ℕ (nat-Fin x) (add-ℕ (nat-Fin y) (nat-Fin z))}
      { x4 = add-ℕ (nat-Fin x) (nat-Fin (add-Fin y z))}
      ( congruence-add-ℕ
        ( succ-ℕ k)
        { x = nat-Fin (add-Fin x y)}
        { y = nat-Fin z}
        { x' = add-ℕ (nat-Fin x) (nat-Fin y)}
        { y' = nat-Fin z}
        ( cong-add-Fin x y)
        ( reflexive-cong-ℕ (succ-ℕ k) (nat-Fin z)))
      ( associative-add-ℕ (nat-Fin x) (nat-Fin y) (nat-Fin z))
      ( congruence-add-ℕ
        ( succ-ℕ k)
        { x = nat-Fin x}
        { y = add-ℕ (nat-Fin y) (nat-Fin z)}
        { x' = nat-Fin x}
        { y' = nat-Fin (add-Fin y z)}
        ( reflexive-cong-ℕ (succ-ℕ k) (nat-Fin x))
        ( symmetric-cong-ℕ
          ( succ-ℕ k)
          ( nat-Fin (add-Fin y z))
          ( add-ℕ (nat-Fin y) (nat-Fin z))
          ( cong-add-Fin y z))))

-- We show that addition satisfies the right unit law --

right-unit-law-add-Fin :
  {k : ℕ} (x : Fin (succ-ℕ k)) → Id (add-Fin x zero-Fin) x
right-unit-law-add-Fin {k} x =
  ( eq-cong-ℕ k
    ( add-ℕ (nat-Fin x) (nat-Fin {succ-ℕ k} zero-Fin))
    ( add-ℕ (nat-Fin x) zero-ℕ)
    ( congruence-add-ℕ
      ( succ-ℕ k)
      { x = nat-Fin {succ-ℕ k} x}
      { y = nat-Fin {succ-ℕ k} zero-Fin}
      { x' = nat-Fin x}
      { y' = zero-ℕ}
      ( reflexive-cong-ℕ (succ-ℕ k) (nat-Fin {succ-ℕ k} x))
      ( cong-nat-zero-Fin {k}))) ∙
  ( issec-nat-Fin k x)

left-unit-law-add-Fin :
  {k : ℕ} (x : Fin (succ-ℕ k)) → Id (add-Fin zero-Fin x) x
left-unit-law-add-Fin {k} x =
  ( commutative-add-Fin zero-Fin x) ∙
  ( right-unit-law-add-Fin x)

-- We show that addition satisfies the left inverse law --

left-inverse-law-add-Fin :
  {k : ℕ} (x : Fin (succ-ℕ k)) → Id (add-Fin (neg-Fin x) x) zero-Fin
left-inverse-law-add-Fin {k} x =
  eq-cong-ℕ k (add-ℕ (nat-Fin (neg-Fin x)) (nat-Fin x)) zero-ℕ
    ( concatenate-cong-eq-cong-ℕ
      { succ-ℕ k}
      { x1 = add-ℕ (nat-Fin (neg-Fin x)) (nat-Fin x)}
      { x2 = add-ℕ (dist-ℕ (nat-Fin x) (succ-ℕ k)) (nat-Fin x)}
      { x3 = succ-ℕ k}
      { x4 = zero-ℕ}
      ( congruence-add-ℕ
        ( succ-ℕ k)
        { x = nat-Fin (neg-Fin x)}
        { y = nat-Fin x}
        ( cong-neg-Fin x)
        ( reflexive-cong-ℕ (succ-ℕ k) (nat-Fin x)))
      ( ( ap ( add-ℕ (dist-ℕ (nat-Fin x) (succ-ℕ k)))
             ( inv (left-zero-law-dist-ℕ (nat-Fin x)))) ∙
        ( ( commutative-add-ℕ
            ( dist-ℕ (nat-Fin x) (succ-ℕ k))
            ( dist-ℕ zero-ℕ (nat-Fin x))) ∙
          ( triangle-equality-dist-ℕ zero-ℕ (nat-Fin x) (succ-ℕ k) star
            ( preserves-leq-succ-ℕ (nat-Fin x) k (upper-bound-nat-Fin x)))))
      ( symmetric-cong-ℕ
          ( succ-ℕ k)
          ( zero-ℕ)
          ( succ-ℕ k)
          ( cong-zero-ℕ (succ-ℕ k))))

right-inverse-law-add-Fin :
  {k : ℕ} (x : Fin (succ-ℕ k)) → Id (add-Fin x (neg-Fin x)) zero-Fin
right-inverse-law-add-Fin x =
  ( commutative-add-Fin x (neg-Fin x)) ∙ (left-inverse-law-add-Fin x)

--------------------------------------------------------------------------------

{- Exercises -}

{- Exercise 7.1 -}

-- See Proposition 7.1.2

{- Exercise 7.2 -}

{- Exercise 7.3 -}

{- Exercise 7.4 -}

{- Exercise 7.5 -}

{- Exercise 7.6 -}

{- Exercise 7.7 -}

pred-zero-Fin :
  {k : ℕ} → Id (pred-Fin {succ-ℕ k} zero-Fin) neg-one-Fin
pred-zero-Fin {zero-ℕ} = refl
pred-zero-Fin {succ-ℕ k} = ap skip-neg-two-Fin (pred-zero-Fin {k})

succ-skip-neg-two-Fin :
  {k : ℕ} (x : Fin (succ-ℕ k)) →
  Id (succ-Fin (skip-neg-two-Fin x)) (inl (succ-Fin x))
succ-skip-neg-two-Fin {zero-ℕ} (inr star) = refl
succ-skip-neg-two-Fin {succ-ℕ k} (inl x) = refl
succ-skip-neg-two-Fin {succ-ℕ k} (inr star) = refl

succ-pred-Fin :
  {k : ℕ} (x : Fin k) → Id (succ-Fin (pred-Fin x)) x
succ-pred-Fin {succ-ℕ zero-ℕ} (inr star) = refl
succ-pred-Fin {succ-ℕ (succ-ℕ k)} (inl x) =
  succ-skip-neg-two-Fin (pred-Fin x) ∙ ap inl (succ-pred-Fin x)
succ-pred-Fin {succ-ℕ (succ-ℕ k)} (inr star) = refl

pred-succ-Fin :
  {k : ℕ} (x : Fin k) → Id (pred-Fin (succ-Fin x)) x
pred-succ-Fin {succ-ℕ zero-ℕ} (inr star) = refl
pred-succ-Fin {succ-ℕ (succ-ℕ k)} (inl (inl x)) =
  ap skip-neg-two-Fin (pred-succ-Fin (inl x))
pred-succ-Fin {succ-ℕ (succ-ℕ k)} (inl (inr star)) = refl
pred-succ-Fin {succ-ℕ (succ-ℕ k)} (inr star) = pred-zero-Fin

{- Exercise 7.8 -}

{- Exercise 7.9 -}

reverse-Fin : {k : ℕ} → Fin k → Fin k
reverse-Fin {succ-ℕ k} (inl x) = skip-zero-Fin (reverse-Fin x)
reverse-Fin {succ-ℕ k} (inr x) = zero-Fin

reverse-skip-zero-Fin :
  {k : ℕ} (x : Fin k) →
  Id (reverse-Fin (skip-zero-Fin x)) (inl-Fin k (reverse-Fin x))
reverse-skip-zero-Fin {succ-ℕ k} (inl x) =
  ap skip-zero-Fin (reverse-skip-zero-Fin x)
reverse-skip-zero-Fin {succ-ℕ k} (inr star) = refl

reverse-neg-one-Fin :
  {k : ℕ} → Id (reverse-Fin (neg-one-Fin {k})) (zero-Fin {k})
reverse-neg-one-Fin {k} = refl

reverse-zero-Fin :
  {k : ℕ} → Id (reverse-Fin (zero-Fin {k})) (neg-one-Fin {k})
reverse-zero-Fin {zero-ℕ} = refl
reverse-zero-Fin {succ-ℕ k} = ap skip-zero-Fin (reverse-zero-Fin {k})

reverse-reverse-Fin :
  {k : ℕ} (x : Fin k) → Id (reverse-Fin (reverse-Fin x)) x
reverse-reverse-Fin {succ-ℕ k} (inl x) =
  ( reverse-skip-zero-Fin (reverse-Fin x)) ∙
  ( ap inl (reverse-reverse-Fin x))
reverse-reverse-Fin {succ-ℕ k} (inr star) = reverse-zero-Fin

{- Exercise 7.10 -}

-- We show that congruence is invariant under scalar multiplication --

scalar-invariant-cong-ℕ :
  (k x y z : ℕ) → cong-ℕ k x y →  cong-ℕ k (mul-ℕ z x) (mul-ℕ z y)
scalar-invariant-cong-ℕ k x y z (pair d p) =
  pair
    ( mul-ℕ z d)
    ( ( associative-mul-ℕ z d k) ∙
      ( ( ap (mul-ℕ z) p) ∙
        ( inv (linear-dist-ℕ x y z))))

scalar-invariant-cong-ℕ' :
  (k x y z : ℕ) → cong-ℕ k x y → cong-ℕ k (mul-ℕ x z) (mul-ℕ y z)
scalar-invariant-cong-ℕ' k x y z H =
  concatenate-eq-cong-eq-ℕ k
    ( commutative-mul-ℕ x z)
    ( scalar-invariant-cong-ℕ k x y z H)
    ( commutative-mul-ℕ z y)

-- We show that multiplication respects the congruence relation --

congruence-mul-ℕ :
  (k : ℕ) {x y x' y' : ℕ} →
  cong-ℕ  k x x' → cong-ℕ k y y' → cong-ℕ k (mul-ℕ x y) (mul-ℕ x' y')
congruence-mul-ℕ k {x} {y} {x'} {y'} H K =
  transitive-cong-ℕ k (mul-ℕ x y) (mul-ℕ x y') (mul-ℕ x' y')
    ( scalar-invariant-cong-ℕ k y y' x K)
    ( scalar-invariant-cong-ℕ' k x x' y' H)

{- We define the multiplication on the types Fin k. -}

mul-Fin :
  {k : ℕ} → Fin k → Fin k → Fin k
mul-Fin {succ-ℕ k} x y = mod-succ-ℕ k (mul-ℕ (nat-Fin x) (nat-Fin y))

ap-mul-Fin :
  {k : ℕ} {x y x' y' : Fin k} →
  Id x x' → Id y y' → Id (mul-Fin x y) (mul-Fin x' y')
ap-mul-Fin refl refl = refl

cong-mul-Fin :
  {k : ℕ} (x y : Fin k) →
  cong-ℕ k (nat-Fin (mul-Fin x y)) (mul-ℕ (nat-Fin x) (nat-Fin y))
cong-mul-Fin {succ-ℕ k} x y =
  cong-nat-mod-succ-ℕ k (mul-ℕ (nat-Fin x) (nat-Fin y))

associative-mul-Fin :
  {k : ℕ} (x y z : Fin k) →
  Id (mul-Fin (mul-Fin x y) z) (mul-Fin x (mul-Fin y z))
associative-mul-Fin {succ-ℕ k} x y z =
  eq-cong-ℕ k
    ( mul-ℕ (nat-Fin (mul-Fin x y)) (nat-Fin z))
    ( mul-ℕ (nat-Fin x) (nat-Fin (mul-Fin y z)))
    ( concatenate-cong-eq-cong-ℕ
      { x1 = mul-ℕ (nat-Fin (mul-Fin x y)) (nat-Fin z)}
      { x2 = mul-ℕ (mul-ℕ (nat-Fin x) (nat-Fin y)) (nat-Fin z)}
      { x3 = mul-ℕ (nat-Fin x) (mul-ℕ (nat-Fin y) (nat-Fin z))}
      { x4 = mul-ℕ (nat-Fin x) (nat-Fin (mul-Fin y z))}
      ( congruence-mul-ℕ
        ( succ-ℕ k)
        { x = nat-Fin (mul-Fin x y)}
        { y = nat-Fin z}
        ( cong-mul-Fin x y)
        ( reflexive-cong-ℕ (succ-ℕ k) (nat-Fin z)))
      ( associative-mul-ℕ (nat-Fin x) (nat-Fin y) (nat-Fin z))
      ( symmetric-cong-ℕ
        ( succ-ℕ k)
        ( mul-ℕ (nat-Fin x) (nat-Fin (mul-Fin y z)))
        ( mul-ℕ (nat-Fin x) (mul-ℕ (nat-Fin y) (nat-Fin z)))
        ( congruence-mul-ℕ
          ( succ-ℕ k)
          { x = nat-Fin x}
          { y = nat-Fin (mul-Fin y z)}
          ( reflexive-cong-ℕ (succ-ℕ k) (nat-Fin x))
          ( cong-mul-Fin y z))))

commutative-mul-Fin :
  {k : ℕ} (x y : Fin k) → Id (mul-Fin x y) (mul-Fin y x)
commutative-mul-Fin {succ-ℕ k} x y =
  eq-cong-ℕ k
    ( mul-ℕ (nat-Fin x) (nat-Fin y))
    ( mul-ℕ (nat-Fin y) (nat-Fin x))
    ( cong-identification-ℕ
      ( succ-ℕ k)
      ( commutative-mul-ℕ (nat-Fin x) (nat-Fin y)))

one-Fin : {k : ℕ} → Fin (succ-ℕ k)
one-Fin {k} = mod-succ-ℕ k one-ℕ

nat-one-Fin : {k : ℕ} → Id (nat-Fin (one-Fin {succ-ℕ k})) one-ℕ
nat-one-Fin {zero-ℕ} = refl
nat-one-Fin {succ-ℕ k} = nat-one-Fin {k}

left-unit-law-mul-Fin :
  {k : ℕ} (x : Fin (succ-ℕ k)) → Id (mul-Fin one-Fin x) x
left-unit-law-mul-Fin {zero-ℕ} (inr star) = refl
left-unit-law-mul-Fin {succ-ℕ k} x =
  ( eq-cong-ℕ (succ-ℕ k)
    ( mul-ℕ (nat-Fin (one-Fin {succ-ℕ k})) (nat-Fin x))
    ( nat-Fin x)
    ( cong-identification-ℕ
      ( succ-ℕ (succ-ℕ k))
      ( ( ap ( mul-ℕ' (nat-Fin x))
             ( nat-one-Fin {k})) ∙
        ( left-unit-law-mul-ℕ (nat-Fin x))))) ∙
  ( issec-nat-Fin (succ-ℕ k) x)

right-unit-law-mul-Fin :
  {k : ℕ} (x : Fin (succ-ℕ k)) → Id (mul-Fin x one-Fin) x
right-unit-law-mul-Fin x =
  ( commutative-mul-Fin x one-Fin) ∙
  ( left-unit-law-mul-Fin x)

left-distributive-mul-add-Fin :
  {k : ℕ} (x y z : Fin k) →
  Id (mul-Fin x (add-Fin y z)) (add-Fin (mul-Fin x y) (mul-Fin x z))
left-distributive-mul-add-Fin {succ-ℕ k} x y z =
  eq-cong-ℕ k
    ( mul-ℕ (nat-Fin x) (nat-Fin (add-Fin y z)))
    ( add-ℕ (nat-Fin (mul-Fin x y)) (nat-Fin (mul-Fin x z)))
    ( concatenate-cong-eq-cong-ℕ
      { k = succ-ℕ k}
      { x1 = mul-ℕ ( nat-Fin x) (nat-Fin (add-Fin y z))}
      { x2 = mul-ℕ ( nat-Fin x) (add-ℕ (nat-Fin y) (nat-Fin z))}
      { x3 = add-ℕ ( mul-ℕ (nat-Fin x) (nat-Fin y))
                   ( mul-ℕ (nat-Fin x) (nat-Fin z))}
      { x4 = add-ℕ (nat-Fin (mul-Fin x y)) (nat-Fin (mul-Fin x z))}
      ( congruence-mul-ℕ
        ( succ-ℕ k)
        { x = nat-Fin x}
        { y = nat-Fin (add-Fin y z)}
        { x' = nat-Fin x}
        { y' = add-ℕ (nat-Fin y) (nat-Fin z)}
        ( reflexive-cong-ℕ (succ-ℕ k) (nat-Fin x))
        ( cong-add-Fin y z))
      ( left-distributive-mul-add-ℕ (nat-Fin x) (nat-Fin y) (nat-Fin z))
      ( symmetric-cong-ℕ (succ-ℕ k)
        ( add-ℕ ( nat-Fin (mul-Fin x y))
                ( nat-Fin (mul-Fin x z)))
        ( add-ℕ ( mul-ℕ (nat-Fin x) (nat-Fin y))
                ( mul-ℕ (nat-Fin x) (nat-Fin z)))
        ( congruence-add-ℕ
          ( succ-ℕ k)
          { x = nat-Fin (mul-Fin x y)}
          { y = nat-Fin (mul-Fin x z)}
          { x' = mul-ℕ (nat-Fin x) (nat-Fin y)}
          { y' = mul-ℕ (nat-Fin x) (nat-Fin z)}
          ( cong-mul-Fin x y)
          ( cong-mul-Fin x z))))

right-distributive-mul-add-Fin :
  {k : ℕ} (x y z : Fin k) →
  Id (mul-Fin (add-Fin x y) z) (add-Fin (mul-Fin x z) (mul-Fin y z))
right-distributive-mul-add-Fin {k} x y z =
  ( commutative-mul-Fin (add-Fin x y) z) ∙
  ( ( left-distributive-mul-add-Fin z x y) ∙
    ( ap-add-Fin (commutative-mul-Fin z x) (commutative-mul-Fin z y)))

{- Exercise 7.11 -}

{- Exercise 7.12 -}

-- We introduce the observational equality on finite sets.

Eq-Fin : (k : ℕ) → Fin k → Fin k → UU lzero
Eq-Fin (succ-ℕ k) (inl x) (inl y) = Eq-Fin k x y
Eq-Fin (succ-ℕ k) (inl x) (inr y) = empty
Eq-Fin (succ-ℕ k) (inr x) (inl y) = empty
Eq-Fin (succ-ℕ k) (inr x) (inr y) = unit

-- Exercise 7.12 (a)

refl-Eq-Fin : {k : ℕ} (x : Fin k) → Eq-Fin k x x
refl-Eq-Fin {succ-ℕ k} (inl x) = refl-Eq-Fin x
refl-Eq-Fin {succ-ℕ k} (inr x) = star

Eq-Fin-eq : {k : ℕ} {x y : Fin k} → Id x y → Eq-Fin k x y
Eq-Fin-eq {k} refl = refl-Eq-Fin {k} _

eq-Eq-Fin :
  {k : ℕ} {x y : Fin k} → Eq-Fin k x y → Id x y
eq-Eq-Fin {succ-ℕ k} {inl x} {inl y} e = ap inl (eq-Eq-Fin e)
eq-Eq-Fin {succ-ℕ k} {inr star} {inr star} star = refl

-- Exercise 7.12 (b)

is-injective-inl-Fin :
  {k : ℕ} {x y : Fin k} → Id (inl-Fin k x) (inl-Fin k y) → Id x y
is-injective-inl-Fin p = eq-Eq-Fin (Eq-Fin-eq p)

-- Exercise 7.12 (c)

neq-zero-succ-Fin :
  {k : ℕ} {x : Fin k} → ¬ (Id (succ-Fin (inl-Fin k x)) zero-Fin)
neq-zero-succ-Fin {succ-ℕ k} {inl x} p =
  neq-zero-succ-Fin (is-injective-inl-Fin p)
neq-zero-succ-Fin {succ-ℕ k} {inr star} p =
  Eq-Fin-eq {succ-ℕ (succ-ℕ k)} {inr star} {zero-Fin} p

-- Exercise 7.12 (d)

is-injective-skip-zero-Fin :
  {k : ℕ} {x y : Fin k} → Id (skip-zero-Fin x) (skip-zero-Fin y) → Id x y
is-injective-skip-zero-Fin {succ-ℕ k} {inl x} {inl y} p =
  ap inl (is-injective-skip-zero-Fin (is-injective-inl-Fin p))
is-injective-skip-zero-Fin {succ-ℕ k} {inl x} {inr star} p =
  ex-falso (Eq-Fin-eq p)
is-injective-skip-zero-Fin {succ-ℕ k} {inr star} {inl y} p =
  ex-falso (Eq-Fin-eq p)
is-injective-skip-zero-Fin {succ-ℕ k} {inr star} {inr star} p = refl

is-injective-succ-Fin :
  {k : ℕ} {x y : Fin k} → Id (succ-Fin x) (succ-Fin y) → Id x y
is-injective-succ-Fin {succ-ℕ k} {inl x} {inl y} p =
  ap inl (is-injective-skip-zero-Fin {k} {x} {y} p)
is-injective-succ-Fin {succ-ℕ k} {inl x} {inr star} p =
  ex-falso (neq-zero-succ-Fin {succ-ℕ k} {inl x} (ap inl p))
is-injective-succ-Fin {succ-ℕ k} {inr star} {inl y} p =
  ex-falso (neq-zero-succ-Fin {succ-ℕ k} {inl y} (ap inl (inv p)))
is-injective-succ-Fin {succ-ℕ k} {inr star} {inr star} p = refl

--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------

{- Section 7.2 Decidability -}

{- Definition 7.2.1 -}

is-decidable : {l : Level} (A : UU l) → UU l
is-decidable A = coprod A (¬ A)

{- Example 7.2.2 -}

is-decidable-unit : is-decidable unit
is-decidable-unit = inl star

is-decidable-empty : is-decidable empty
is-decidable-empty = inr id

{- Definition 7.2.3 -}

{- We say that a type has decidable equality if we can decide whether
   x = y holds for any x, y : A. -}

has-decidable-equality : {l : Level} (A : UU l) → UU l
has-decidable-equality A = (x y : A) → is-decidable (Id x y)

{- Lemma 7.2.5 -}

is-decidable-iff :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  (A → B) → (B → A) → is-decidable A → is-decidable B
is-decidable-iff f g =
  functor-coprod f (functor-neg g)

{- Proposition 7.2.6 -}

{- The type ℕ is an example of a type with decidable equality. -}

is-decidable-Eq-ℕ :
  (m n : ℕ) → is-decidable (Eq-ℕ m n)
is-decidable-Eq-ℕ zero-ℕ zero-ℕ = inl star
is-decidable-Eq-ℕ zero-ℕ (succ-ℕ n) = inr id
is-decidable-Eq-ℕ (succ-ℕ m) zero-ℕ = inr id
is-decidable-Eq-ℕ (succ-ℕ m) (succ-ℕ n) = is-decidable-Eq-ℕ m n

has-decidable-equality-ℕ : has-decidable-equality ℕ
has-decidable-equality-ℕ x y =
  is-decidable-iff (eq-Eq-ℕ x y) Eq-ℕ-eq (is-decidable-Eq-ℕ x y)

{- Proposition 7.2.9 -}

{- We show that Fin k has decidable equality, for each n : ℕ. -}

is-decidable-Eq-Fin :
  (k : ℕ) (x y : Fin k) → is-decidable (Eq-Fin k x y)
is-decidable-Eq-Fin (succ-ℕ k) (inl x) (inl y) = is-decidable-Eq-Fin k x y
is-decidable-Eq-Fin (succ-ℕ k) (inl x) (inr y) = inr id
is-decidable-Eq-Fin (succ-ℕ k) (inr x) (inl y) = inr id
is-decidable-Eq-Fin (succ-ℕ k) (inr x) (inr y) = inl star

is-decidable-eq-Fin :
  (k : ℕ) (x y : Fin k) → is-decidable (Id x y)
is-decidable-eq-Fin k x y =
  functor-coprod eq-Eq-Fin (functor-neg Eq-Fin-eq) (is-decidable-Eq-Fin k x y)

{- Section 7.3 Definitions by case analysis -}

{- We define an alternative definition of the predecessor function with manual
   with-abstraction. -}

cases-pred-Fin-2 :
  {k : ℕ} (x : Fin (succ-ℕ k))
  (d : is-decidable (Eq-Fin (succ-ℕ k) x zero-Fin)) → Fin (succ-ℕ k)
cases-pred-Fin-2 {zero-ℕ} (inr star) d = zero-Fin
cases-pred-Fin-2 {succ-ℕ k} (inl x) (inl e) = neg-one-Fin
cases-pred-Fin-2 {succ-ℕ k} (inl x) (inr f) =
  inl (cases-pred-Fin-2 {k} x (inr f))
cases-pred-Fin-2 {succ-ℕ k} (inr star) (inr f) = inl neg-one-Fin

pred-Fin-2 : {k : ℕ} → Fin k → Fin k
pred-Fin-2 {succ-ℕ k} x =
  cases-pred-Fin-2 {k} x (is-decidable-Eq-Fin (succ-ℕ k) x zero-Fin)

{- We give a solution to the exercise for the alternative definition of the
   predecessor function, using with-abstraction. -}

pred-zero-Fin-2 :
  {k : ℕ} → Id (pred-Fin-2 {succ-ℕ k} zero-Fin) neg-one-Fin
pred-zero-Fin-2 {k} with is-decidable-Eq-Fin (succ-ℕ k) zero-Fin zero-Fin
pred-zero-Fin-2 {zero-ℕ} | d = refl
pred-zero-Fin-2 {succ-ℕ k} | inl e = refl
pred-zero-Fin-2 {succ-ℕ k} | inr f =
  ex-falso (f (refl-Eq-Fin {succ-ℕ k} zero-Fin))

cases-succ-pred-Fin-2 :
  {k : ℕ} (x : Fin (succ-ℕ k))
  (d : is-decidable (Eq-Fin (succ-ℕ k) x zero-Fin)) →
  Id (succ-Fin (cases-pred-Fin-2 x d)) x
cases-succ-pred-Fin-2 {zero-ℕ} (inr star) d =
  refl
cases-succ-pred-Fin-2 {succ-ℕ k} (inl x) (inl e) =
  inv (eq-Eq-Fin e)
cases-succ-pred-Fin-2 {succ-ℕ zero-ℕ} (inl (inr x)) (inr f) =
  ex-falso (f star)
cases-succ-pred-Fin-2 {succ-ℕ (succ-ℕ k)} (inl (inl x)) (inr f) =
  ap inl (cases-succ-pred-Fin-2 (inl x) (inr f))
cases-succ-pred-Fin-2 {succ-ℕ (succ-ℕ k)} (inl (inr star)) (inr f) =
  refl
cases-succ-pred-Fin-2 {succ-ℕ k} (inr star) (inr f) =
  refl

succ-pred-Fin-2 :
  {k : ℕ} (x : Fin k) → Id (succ-Fin (pred-Fin-2 x)) x
succ-pred-Fin-2 {succ-ℕ k} x =
  cases-succ-pred-Fin-2 x (is-decidable-Eq-Fin (succ-ℕ k) x zero-Fin)

pred-inl-Fin-2 :
  {k : ℕ} (x : Fin (succ-ℕ k)) (f : ¬ (Eq-Fin (succ-ℕ k) x zero-Fin)) →
  Id (pred-Fin-2 (inl x)) (inl (pred-Fin-2 x))
pred-inl-Fin-2 {k} x f with is-decidable-Eq-Fin (succ-ℕ k) x zero-Fin
... | inl e = ex-falso (f e)
... | inr f' = refl

nEq-zero-succ-Fin :
  {k : ℕ} (x : Fin (succ-ℕ k)) →
  ¬ (Eq-Fin (succ-ℕ (succ-ℕ k)) (succ-Fin (inl x)) zero-Fin)
nEq-zero-succ-Fin {succ-ℕ k} (inl (inl x)) e = nEq-zero-succ-Fin (inl x) e
nEq-zero-succ-Fin {succ-ℕ k} (inl (inr star)) ()
nEq-zero-succ-Fin {succ-ℕ k} (inr star) ()

pred-succ-Fin-2 :
  {k : ℕ} (x : Fin (succ-ℕ k)) → Id (pred-Fin-2 (succ-Fin x)) x
pred-succ-Fin-2 {zero-ℕ} (inr star) = refl
pred-succ-Fin-2 {succ-ℕ zero-ℕ} (inl (inr star)) = refl
pred-succ-Fin-2 {succ-ℕ zero-ℕ} (inr star) = refl
pred-succ-Fin-2 {succ-ℕ (succ-ℕ k)} (inl (inl (inl x))) =
  ( pred-inl-Fin-2 (inl (succ-Fin (inl x))) (nEq-zero-succ-Fin (inl x))) ∙
  ( ( ap inl (pred-inl-Fin-2 (succ-Fin (inl x)) (nEq-zero-succ-Fin (inl x)))) ∙
    ( ap (inl ∘ inl) (pred-succ-Fin-2 (inl x))))
pred-succ-Fin-2 {succ-ℕ (succ-ℕ k)} (inl (inl (inr star))) = refl
pred-succ-Fin-2 {succ-ℕ (succ-ℕ k)} (inl (inr star)) = refl
pred-succ-Fin-2 {succ-ℕ (succ-ℕ k)} (inr star) = pred-zero-Fin-2

--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------

dist-ℤ : ℤ → ℤ → ℕ
dist-ℤ (inl x) (inl y) = dist-ℕ x y
dist-ℤ (inl x) (inr (inl star)) = succ-ℕ x
dist-ℤ (inl x) (inr (inr y)) = succ-ℕ (succ-ℕ (add-ℕ x y))
dist-ℤ (inr (inl star)) (inl y) = succ-ℕ y
dist-ℤ (inr (inr x)) (inl y) = succ-ℕ (succ-ℕ (add-ℕ x y))
dist-ℤ (inr (inl star)) (inr (inl star)) = zero-ℕ
dist-ℤ (inr (inl star)) (inr (inr y)) = succ-ℕ y
dist-ℤ (inr (inr x)) (inr (inl star)) = succ-ℕ x
dist-ℤ (inr (inr x)) (inr (inr y)) = dist-ℕ x y

dist-ℤ' : ℤ → ℤ → ℕ
dist-ℤ' x y = dist-ℤ y x

ap-dist-ℤ :
  {x y x' y' : ℤ} → Id x x' → Id y y' → Id (dist-ℤ x y) (dist-ℤ x' y')
ap-dist-ℤ refl refl = refl

eq-dist-ℤ :
  (x y : ℤ) → Id zero-ℕ (dist-ℤ x y) → Id x y
eq-dist-ℤ (inl x) (inl y) p = ap inl (eq-dist-ℕ x y p)
eq-dist-ℤ (inl x) (inr (inl star)) p = ex-falso (Peano-8 x p)
eq-dist-ℤ (inr (inl star)) (inl y) p = ex-falso (Peano-8 y p)
eq-dist-ℤ (inr (inl star)) (inr (inl star)) p = refl
eq-dist-ℤ (inr (inl star)) (inr (inr y)) p = ex-falso (Peano-8 y p)
eq-dist-ℤ (inr (inr x)) (inr (inl star)) p = ex-falso (Peano-8 x p)
eq-dist-ℤ (inr (inr x)) (inr (inr y)) p = ap (inr ∘ inr) (eq-dist-ℕ x y p)

dist-eq-ℤ' :
  (x : ℤ) → Id zero-ℕ (dist-ℤ x x)
dist-eq-ℤ' (inl x) = dist-eq-ℕ' x
dist-eq-ℤ' (inr (inl star)) = refl
dist-eq-ℤ' (inr (inr x)) = dist-eq-ℕ' x

dist-eq-ℤ :
  (x y : ℤ) → Id x y → Id zero-ℕ (dist-ℤ x y)
dist-eq-ℤ x .x refl = dist-eq-ℤ' x

{- The distance function on ℤ is symmetric. -}

symmetric-dist-ℤ :
  (x y : ℤ) → Id (dist-ℤ x y) (dist-ℤ y x)
symmetric-dist-ℤ (inl x) (inl y) = symmetric-dist-ℕ x y
symmetric-dist-ℤ (inl x) (inr (inl star)) = refl
symmetric-dist-ℤ (inl x) (inr (inr y)) =
  ap (succ-ℕ ∘ succ-ℕ) (commutative-add-ℕ x y)
symmetric-dist-ℤ (inr (inl star)) (inl y) = refl
symmetric-dist-ℤ (inr (inr x)) (inl y) =
  ap (succ-ℕ ∘ succ-ℕ) (commutative-add-ℕ x y)
symmetric-dist-ℤ (inr (inl star)) (inr (inl star)) = refl
symmetric-dist-ℤ (inr (inl star)) (inr (inr y)) = refl
symmetric-dist-ℤ (inr (inr x)) (inr (inl star)) = refl
symmetric-dist-ℤ (inr (inr x)) (inr (inr y)) = symmetric-dist-ℕ x y

-- We compute the distance from zero --

left-zero-law-dist-ℤ :
  (x : ℤ) → Id (dist-ℤ zero-ℤ x) (abs-ℤ x)
left-zero-law-dist-ℤ (inl x) = refl
left-zero-law-dist-ℤ (inr (inl star)) = refl
left-zero-law-dist-ℤ (inr (inr x)) = refl

right-zero-law-dist-ℤ :
  (x : ℤ) → Id (dist-ℤ x zero-ℤ) (abs-ℤ x)
right-zero-law-dist-ℤ (inl x) = refl
right-zero-law-dist-ℤ (inr (inl star)) = refl
right-zero-law-dist-ℤ (inr (inr x)) = refl

-- We prove the triangle inequality --

{-
triangle-inequality-dist-ℤ :
  (x y z : ℤ) → leq-ℕ (dist-ℤ x y) (add-ℕ (dist-ℤ x z) (dist-ℤ z y))
triangle-inequality-dist-ℤ (inl x) (inl y) (inl z) =
  triangle-inequality-dist-ℕ x y z
triangle-inequality-dist-ℤ (inl x) (inl y) (inr (inl star)) =
  triangle-inequality-dist-ℕ (succ-ℕ x) (succ-ℕ y) zero-ℕ
triangle-inequality-dist-ℤ (inl x) (inl y) (inr (inr z)) = {!!}
triangle-inequality-dist-ℤ (inl x) (inr y) (inl z) = {!!}
triangle-inequality-dist-ℤ (inl x) (inr y) (inr z) = {!!}
triangle-inequality-dist-ℤ (inr x) (inl y) (inl z) = {!!}
triangle-inequality-dist-ℤ (inr x) (inl y) (inr z) = {!!}
triangle-inequality-dist-ℤ (inr x) (inr y) (inl z) = {!!}
triangle-inequality-dist-ℤ (inr x) (inr y) (inr z) = {!!}
-}

{-

triangle-inequality-dist-ℕ :
  (m n k : ℕ) → leq-ℕ (dist-ℕ m n) (add-ℕ (dist-ℕ m k) (dist-ℕ k n))
triangle-inequality-dist-ℕ zero-ℕ zero-ℕ zero-ℕ = star
triangle-inequality-dist-ℕ zero-ℕ zero-ℕ (succ-ℕ k) = star
triangle-inequality-dist-ℕ zero-ℕ (succ-ℕ n) zero-ℕ =
  tr ( leq-ℕ (succ-ℕ n))
     ( inv (left-unit-law-add-ℕ (succ-ℕ n)))
     ( reflexive-leq-ℕ (succ-ℕ n))
triangle-inequality-dist-ℕ zero-ℕ (succ-ℕ n) (succ-ℕ k) =
  concatenate-eq-leq-eq-ℕ
    ( inv (ap succ-ℕ (left-zero-law-dist-ℕ n)))
    ( triangle-inequality-dist-ℕ zero-ℕ n k)
    ( ( ap (succ-ℕ ∘ (add-ℕ' (dist-ℕ k n))) (left-zero-law-dist-ℕ k)) ∙
      ( inv (left-successor-law-add-ℕ k (dist-ℕ k n))))
triangle-inequality-dist-ℕ (succ-ℕ m) zero-ℕ zero-ℕ = reflexive-leq-ℕ (succ-ℕ m)
triangle-inequality-dist-ℕ (succ-ℕ m) zero-ℕ (succ-ℕ k) =
  concatenate-eq-leq-eq-ℕ
    ( inv (ap succ-ℕ (right-zero-law-dist-ℕ m)))
    ( triangle-inequality-dist-ℕ m zero-ℕ k)
    ( ap (succ-ℕ ∘ (add-ℕ (dist-ℕ m k))) (right-zero-law-dist-ℕ k))
triangle-inequality-dist-ℕ (succ-ℕ m) (succ-ℕ n) zero-ℕ =
  concatenate-leq-eq-ℕ
    ( dist-ℕ m n)
    ( transitive-leq-ℕ
      ( dist-ℕ m n)
      ( succ-ℕ (add-ℕ (dist-ℕ m zero-ℕ) (dist-ℕ zero-ℕ n)))
      ( succ-ℕ (succ-ℕ (add-ℕ (dist-ℕ m zero-ℕ) (dist-ℕ zero-ℕ n))))
      ( transitive-leq-ℕ
        ( dist-ℕ m n)
        ( add-ℕ (dist-ℕ m zero-ℕ) (dist-ℕ zero-ℕ n))
        ( succ-ℕ (add-ℕ (dist-ℕ m zero-ℕ) (dist-ℕ zero-ℕ n)))
        ( triangle-inequality-dist-ℕ m n zero-ℕ)
        ( succ-leq-ℕ (add-ℕ (dist-ℕ m zero-ℕ) (dist-ℕ zero-ℕ n))))
      ( succ-leq-ℕ (succ-ℕ (add-ℕ (dist-ℕ m zero-ℕ) (dist-ℕ zero-ℕ n)))))
    ( ( ap (succ-ℕ ∘ succ-ℕ)
           ( ap-add-ℕ (right-zero-law-dist-ℕ m) (left-zero-law-dist-ℕ n))) ∙
      ( inv (left-successor-law-add-ℕ m (succ-ℕ n))))
triangle-inequality-dist-ℕ (succ-ℕ m) (succ-ℕ n) (succ-ℕ k) =
  triangle-inequality-dist-ℕ m n k

-- We show that dist-ℕ x y is a solution to a simple equation.

leq-dist-ℕ :
  (x y : ℕ) → leq-ℕ x y → Id (add-ℕ x (dist-ℕ x y)) y
leq-dist-ℕ zero-ℕ zero-ℕ H = refl
leq-dist-ℕ zero-ℕ (succ-ℕ y) star = left-unit-law-add-ℕ (succ-ℕ y)
leq-dist-ℕ (succ-ℕ x) (succ-ℕ y) H =
  ( left-successor-law-add-ℕ x (dist-ℕ x y)) ∙
  ( ap succ-ℕ (leq-dist-ℕ x y H))

rewrite-left-add-dist-ℕ :
  (x y z : ℕ) → Id (add-ℕ x y) z → Id x (dist-ℕ y z)
rewrite-left-add-dist-ℕ zero-ℕ zero-ℕ .zero-ℕ refl = refl
rewrite-left-add-dist-ℕ zero-ℕ (succ-ℕ y) .(succ-ℕ (add-ℕ zero-ℕ y)) refl =
  ( dist-eq-ℕ' y) ∙
  ( inv (ap (dist-ℕ (succ-ℕ y)) (left-unit-law-add-ℕ (succ-ℕ y))))
rewrite-left-add-dist-ℕ (succ-ℕ x) zero-ℕ .(succ-ℕ x) refl = refl
rewrite-left-add-dist-ℕ
  (succ-ℕ x) (succ-ℕ y) .(succ-ℕ (add-ℕ (succ-ℕ x) y)) refl =
  rewrite-left-add-dist-ℕ (succ-ℕ x) y (add-ℕ (succ-ℕ x) y) refl

rewrite-left-dist-add-ℕ :
  (x y z : ℕ) → leq-ℕ y z → Id x (dist-ℕ y z) → Id (add-ℕ x y) z
rewrite-left-dist-add-ℕ .(dist-ℕ y z) y z H refl =
  ( commutative-add-ℕ (dist-ℕ y z) y) ∙
  ( leq-dist-ℕ y z H)

rewrite-right-add-dist-ℕ :
  (x y z : ℕ) → Id (add-ℕ x y) z → Id y (dist-ℕ x z)
rewrite-right-add-dist-ℕ x y z p =
  rewrite-left-add-dist-ℕ y x z (commutative-add-ℕ y x ∙ p)

rewrite-right-dist-add-ℕ :
  (x y z : ℕ) → leq-ℕ x z → Id y (dist-ℕ x z) → Id (add-ℕ x y) z
rewrite-right-dist-add-ℕ x .(dist-ℕ x z) z H refl =
  leq-dist-ℕ x z H

-- We show that dist-ℕ is translation invariant

translation-invariant-dist-ℕ :
  (k m n : ℕ) → Id (dist-ℕ (add-ℕ k m) (add-ℕ k n)) (dist-ℕ m n)
translation-invariant-dist-ℕ zero-ℕ m n =
  ap-dist-ℕ (left-unit-law-add-ℕ m) (left-unit-law-add-ℕ n)
translation-invariant-dist-ℕ (succ-ℕ k)  m n =
  ( ap-dist-ℕ (left-successor-law-add-ℕ k m) (left-successor-law-add-ℕ k n)) ∙
  ( translation-invariant-dist-ℕ k m n)

-- We show that dist-ℕ is linear with respect to scalar multiplication

linear-dist-ℕ :
  (m n k : ℕ) → Id (dist-ℕ (mul-ℕ k m) (mul-ℕ k n)) (mul-ℕ k (dist-ℕ m n))
linear-dist-ℕ zero-ℕ zero-ℕ zero-ℕ = refl
linear-dist-ℕ zero-ℕ zero-ℕ (succ-ℕ k) = linear-dist-ℕ zero-ℕ zero-ℕ k
linear-dist-ℕ zero-ℕ (succ-ℕ n) zero-ℕ = refl
linear-dist-ℕ zero-ℕ (succ-ℕ n) (succ-ℕ k) =
  ap (dist-ℕ' (mul-ℕ (succ-ℕ k) (succ-ℕ n))) (right-zero-law-mul-ℕ (succ-ℕ k))
linear-dist-ℕ (succ-ℕ m) zero-ℕ zero-ℕ = refl
linear-dist-ℕ (succ-ℕ m) zero-ℕ (succ-ℕ k) =
  ap (dist-ℕ (mul-ℕ (succ-ℕ k) (succ-ℕ m))) (right-zero-law-mul-ℕ (succ-ℕ k))
linear-dist-ℕ (succ-ℕ m) (succ-ℕ n) zero-ℕ = refl
linear-dist-ℕ (succ-ℕ m) (succ-ℕ n) (succ-ℕ k) =
  ( ap-dist-ℕ
    ( right-successor-law-mul-ℕ (succ-ℕ k) m)
    ( right-successor-law-mul-ℕ (succ-ℕ k) n)) ∙
  ( ( translation-invariant-dist-ℕ
      ( succ-ℕ k)
      ( mul-ℕ (succ-ℕ k) m)
      ( mul-ℕ (succ-ℕ k) n)) ∙
    ( linear-dist-ℕ m n (succ-ℕ k)))
-}

max_stars_repo_name: tmoux/HoTT-Intro

max_issues_repo_name: tmoux/HoTT-Intro

max_forks_repo_name: tmoux/HoTT-Intro


text:
-- Andreas, 2019-03-18, AIM XXIX, issue #3631 reported by rrose1
-- Performance regression in 2.5.4 due to new sort handling

{-# OPTIONS --no-universe-polymorphism #-}  -- needed for the performance problem

-- {-# OPTIONS -v 10 -v tc.cc:15 -v tc.cc.type:60 -v tc.cover:100 #-}
-- {-# OPTIONS -v tc.cc.type:80 #-}

module _ where

  module M
    (X : Set)
    (x0  x1  x2  x3  x4  x5  x6  x7  x8  x9  : X)
    (x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 : X)
    (x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 : X)
    where
    f : X
    f = x0

-- Should check quickly.

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Source.Examples where

open import Source.Size
open import Source.Size.Substitution.Theory
open import Source.Term
open import Source.Type
open import Util.Prelude

import Source.Size.Substitution.Canonical as SC

{-
liftℕ : ∀ n < ⋆. ∀ m < n. Nat m → Nat n
liftℕ ≔ Λ n < ⋆. Λ m < n. λ i : Nat m.
  caseNat[Nat n] m i
    zero n
    (Λ k < m. λ i′ : Nat k. suc n k i′)
-}
liftNat : ∀ {Δ} → Term Δ
liftNat = Λₛ ⋆ , Λₛ v0 , Λ (Nat v0) ,
  caseNat (Nat v1) v0 (var 0)
    (zero v1)
    (Λₛ v0 , Λ (Nat v0) , suc v2 v0 (var 0))

liftNat⊢ : ∀ {Δ Γ}
  → Δ , Γ ⊢ liftNat ∶ Π ⋆ , Π v0 , Nat v0 ⇒ Nat v1
liftNat⊢
  = absₛ
      (absₛ
        (abs
          (caseNat (<-trans (var refl) (var refl))
            (var zero)
            (zero (var refl))
            (absₛ
              (abs
                (suc (var refl) (<-trans (var refl) (var refl)) (var zero)))
              refl)
            refl))
        refl)
      refl

{-
half : ∀ n < ⋆. Nat n → Nat n
half ≔ λ n < ⋆. fix[Nat ∙ → Nat ∙]
  (Λ n < ⋆. λ rec : (∀ m < n. Nat m → Nat m). λ i : Nat n.
    caseNat[Nat n] n i
      (zero n)
      (Λ m < n. λ i′ : Nat m. caseNat[Nat n] m i′
        (zero n)
        (Λ k < m. λ i″ : Nat k. suc n k (rec k i″))))
  n
-}
half : ∀ {Δ} → Term Δ
half = Λₛ ⋆ , fix (Nat v0 ⇒ Nat v0)
  (Λₛ ⋆ , Λ (Π v0 , Nat v0 ⇒ Nat v0) ,
    Λ Nat v0 , caseNat (Nat v0) v0 (var 0)
      (zero v0)
      (Λₛ v0 , Λ (Nat v0) , caseNat (Nat v1) v0 (var 0)
        (zero v1)
        (Λₛ v0 , Λ (Nat v0) , suc v2 v0 (var 3 ·ₛ v0 · var 0))))
  v0

half⊢ : ∀ {Δ Γ} → Δ , Γ ⊢ half ∶ Π ⋆ , Nat v0 ⇒ Nat v0
half⊢
  = absₛ
      (fix (var refl)
        (absₛ
          (abs
            (abs
              (caseNat (var refl) (var zero) (zero (var refl))
                (absₛ
                  (abs
                    (caseNat (<-trans (var refl) (var refl))
                      (var zero)
                      (zero (var refl))
                      (absₛ
                        (abs
                          (suc (var refl) (<-trans (var refl) (var refl))
                            (app
                              (appₛ (<-trans (var refl) (var refl))
                                (var (suc (suc (suc zero))))
                                refl)
                              (var zero))))
                        refl)
                      refl))
                  refl)
                refl)))
          refl)
        refl
        refl)
      refl

{-
suc∞ : Nat ∞ → Nat ∞
suc∞ ≔ λ i : Nat ∞. caseNat[Nat ∞] ∞ i
  (suc ∞ 0 (zero 0))
  (Λ m < ∞. λ i′ : Nat m. suc ∞ (↑ m) (suc (↑ m) m i′))
-}
suc∞ : ∀ {Δ} → Term Δ
suc∞ = Λ (Nat ∞) , caseNat (Nat ∞) ∞ (var 0)
  (suc ∞ zero (zero zero))
  (Λₛ ∞ , Λ (Nat v0) , suc ∞ (suc v0) (suc (suc v0) v0 (var 0)))

suc∞⊢ : ∀ {Δ Γ} → Δ , Γ ⊢ suc∞ ∶ Nat ∞ ⇒ Nat ∞
suc∞⊢
  = abs
      (caseNat <suc (var zero) (suc <suc zero<∞ (zero (<-trans zero<∞ <suc)))
        (absₛ
          (abs
            (suc <suc (suc<∞ (var refl))
              (suc (<-trans (suc<∞ (var refl)) <suc) <suc
                (var zero))))
          refl)
        refl)

{-
plus : ∀ n < ⋆. Nat n → Nat ∞ → Nat ∞
plus ≔ Λ n < ⋆. fix[Nat ∙ → Nat ∞ → Nat ∞]
  (Λ n < ⋆. λ rec : (∀ m < n. Nat m → Nat ∞ → Nat ∞).
    λ i : Nat n. λ j : Nat ∞. caseNat[Nat ∞] n i
      j
      (Λ m < n. λ i′ : Nat m. suc∞ (rec m i′ j)))
  n
-}
plus : ∀ {Δ} → Term Δ
plus = Λₛ ⋆ , fix (Nat v0 ⇒ Nat ∞ ⇒ Nat ∞)
  (Λₛ ⋆ , Λ (Π v0 , Nat v0 ⇒ Nat ∞ ⇒ Nat ∞) ,
    Λ (Nat v0) , Λ (Nat ∞) , caseNat (Nat ∞) v0 (var 1)
      (var 0)
      (Λₛ v0 , Λ (Nat v0) , suc∞ · (var 3 ·ₛ v0 · var 0 · var 1)))
  v0

plus⊢ : ∀ {Δ Γ} → Δ , Γ ⊢ plus ∶ Π ⋆ , Nat v0 ⇒ Nat ∞ ⇒ Nat ∞
plus⊢
  = absₛ
      (fix (var refl)
        (absₛ
          (abs
            (abs
              (abs
                (caseNat (var refl) (var (suc zero)) (var zero)
                  (absₛ
                    (abs
                      (app
                        suc∞⊢
                        (app
                          (app
                            (appₛ (var refl)
                              (var (suc (suc (suc zero))))
                              refl)
                            (var zero))
                          (var (suc zero)))))
                    refl)
                  refl))))
          refl)
        refl
        refl)
      refl

{-
zeros : ∀ n < ⋆. Stream n
zeros ≔ Λ n < ⋆. fix[Stream ∙]
  (Λ n < ⋆. λ rec : (∀ m < n. Stream m).
    cons (zero ∞) n rec)
  n
-}
zeros : ∀ {Δ} → Term Δ
zeros = Λₛ ⋆ , fix (Stream v0)
  (Λₛ ⋆ , Λ (Π v0 , Stream v0) , cons (zero ∞) v0 (var 0))
  v0

zeros⊢ : ∀ {Δ Γ} → Δ , Γ ⊢ zeros ∶ Π ⋆ , Stream v0
zeros⊢
  = absₛ
      (fix (var refl)
        (absₛ
          (abs
            (cons (var refl) (zero <suc) (var zero)))
          refl)
        refl
        refl)
      refl

{-
map : (Nat ∞ → Nat ∞) → ∀ n < ⋆. Stream n → Stream n
map ≔ λ f : Nat ∞ → Nat ∞. Λ n < ⋆. fix[Stream ∙ → Stream ∙]
  (Λ n < ⋆. λ rec : (∀ m < n. Stream m → Stream m). λ xs : Stream n.
    cons (f (head n xs)) n (Λ m < n. rec m (tail n xs m)))
  n
-}
map : ∀ {Δ} → Term Δ
map = Λ (Nat ∞ ⇒ Nat ∞) , Λₛ ⋆ , fix (Stream v0 ⇒ Stream v0)
  (Λₛ ⋆ , Λ (Π v0 , Stream v0 ⇒ Stream v0) , Λ Stream v0 ,
    cons (var 2 · head v0 (var 0)) v0
      (Λₛ v0 , var 1 ·ₛ v0 · tail v1 (var 0) v0))
  v0

map⊢ : ∀ {Δ Γ} → Δ , Γ ⊢ map ∶ (Nat ∞ ⇒ Nat ∞) ⇒ (Π ⋆ , Stream v0 ⇒ Stream v0)
map⊢
  = abs
      (absₛ
        (fix (var refl)
          (absₛ
            (abs
              (abs
                (cons
                  (var refl)
                  (app (var (suc (suc zero))) (head (var refl) (var zero)))
                  (absₛ (app (appₛ (var refl) (var (suc zero)) refl)
                      (tail (var refl) (var refl) (var zero)))
                  refl))))
            refl)
          refl
          refl)
        refl)

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
{-# OPTIONS --without-K --safe #-}

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Fundamental.Reducibility {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Typed
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Reducibility
open import Definition.LogicalRelation.Fundamental

open import Tools.Product

-- Well-formed types are reducible.
reducible : ∀ {A Γ} → Γ ⊢ A → Γ ⊩⟨ ¹ ⟩ A
reducible A = let [Γ] , [A] = fundamental A
              in  reducibleᵛ [Γ] [A]

-- Well-formed equality is reducible.
reducibleEq : ∀ {A B Γ} → Γ ⊢ A ≡ B
            → ∃₂ λ [A] ([B] : Γ ⊩⟨ ¹ ⟩ B) → Γ ⊩⟨ ¹ ⟩ A ≡ B / [A]
reducibleEq {A} {B} A≡B =
  let [Γ] , [A] , [B] , [A≡B] = fundamentalEq A≡B
  in  reducibleᵛ [Γ] [A]
  ,   reducibleᵛ [Γ] [B]
  ,   reducibleEqᵛ {A} {B} [Γ] [A] [A≡B]

-- Well-formed terms are reducible.
reducibleTerm : ∀ {t A Γ} → Γ ⊢ t ∷ A → ∃ λ [A] → Γ ⊩⟨ ¹ ⟩ t ∷ A / [A]
reducibleTerm {t} {A} ⊢t =
  let [Γ] , [A] , [t] = fundamentalTerm ⊢t
  in  reducibleᵛ [Γ] [A] , reducibleTermᵛ {t} {A} [Γ] [A] [t]

-- Well-formed term equality is reducible.
reducibleEqTerm : ∀ {t u A Γ} → Γ ⊢ t ≡ u ∷ A → ∃ λ [A] → Γ ⊩⟨ ¹ ⟩ t ≡ u ∷ A / [A]
reducibleEqTerm {t} {u} {A} t≡u =
  let [Γ] , modelsTermEq [A] [t] [u] [t≡u] = fundamentalTermEq t≡u
  in  reducibleᵛ [Γ] [A] , reducibleEqTermᵛ {t} {u} {A} [Γ] [A] [t≡u]


text:
module MLib.Prelude.DFS.ViaNat where

open import MLib.Prelude
open import MLib.Prelude.Finite

open FE using (_⇨_; cong)

open import Data.Digit using (fromDigits; toDigits; Digit)

module _ {c p} (A-finiteSet : FiniteSet c p) where
  module A = FiniteSet A-finiteSet
  open A using () renaming (Carrier to A)

  open LeftInverse
  open Nat using (_^_; _+_; _*_)

  private
    fromBool : Bool → Digit 2
    fromBool false = Fin.zero
    fromBool true = Fin.suc Fin.zero

    toBool : Digit 2 → Bool
    toBool Fin.zero = false
    toBool (Fin.suc Fin.zero) = true
    toBool (Fin.suc (Fin.suc ()))

    toBool-fromBool : ∀ b → toBool (fromBool b) ≡ b
    toBool-fromBool false = ≡.refl
    toBool-fromBool true = ≡.refl
--     fromBinary : (n : ℕ) → List Bool → ℕ
--     fromBinary n [] = 0 -- an empty table represents an empty binary string
--     fromBinary n (x ∷ xs) = Fin.toℕ x + n * from-n-ary n xs

-- --     -- div-rem m i = "i % m" , "i / m"
--     div-rem : ∀ n → ℕ → Fin n × ℕ
--     div-rem n k = {!!}

--     to-n-ary : (n : ℕ) → ℕ → List (Fin n)
--     to-n-ary n k =
--       let r , d = div-rem n k
--           rs = to-n-ary d
--       in {!!}
--         -- r ∷ rs

-- Goal: fromDigits
-- (List.tabulate (λ x → fromBool (.i ⟨$⟩ (from A.ontoFin ⟨$⟩ x))))
-- ≡
-- fromDigits
-- (List.tabulate (λ x → fromBool (.j ⟨$⟩ (from A.ontoFin ⟨$⟩ x))))

    lookupOrElse : ∀ {n} {a} {A : Set a} → A → Fin n → List A → A
    lookupOrElse z _ [] = z
    lookupOrElse _ Fin.zero (x ∷ xs) = x
    lookupOrElse z (Fin.suc n) (x ∷ xs) = lookupOrElse z n xs

    lookupOrElse-toList : ∀ {n} {a} {A : Set a} {z : A} (i : Fin n) (t : Table A n) → lookupOrElse z i (Table.toList t) ≡ Table.lookup t i
    lookupOrElse-toList Fin.zero t = ≡.refl
    lookupOrElse-toList (Fin.suc i) = lookupOrElse-toList i ∘ Table.tail

    *2-absurd : ∀ m n → m * 2 ≡ suc (n * 2) → ⊥
    *2-absurd zero zero ()
    *2-absurd zero (suc n) ()
    *2-absurd (suc m) zero ()
    *2-absurd (suc m) (suc n) = *2-absurd m n ∘ Nat.suc-injective ∘ Nat.suc-injective

    *2-injective : ∀ m n → m * 2 ≡ n * 2 → m ≡ n
    *2-injective zero zero _ = ≡.refl
    *2-injective zero (suc n) ()
    *2-injective (suc m) zero ()
    *2-injective (suc m) (suc n) = ≡.cong suc ∘ *2-injective m n ∘ Nat.suc-injective ∘ Nat.suc-injective

    01-+-*2 : (i j : Fin 2) (m n : ℕ) → Fin.toℕ i + m * 2 ≡ Fin.toℕ j + n * 2 → m ≡ n
    01-+-*2 Fin.zero Fin.zero = *2-injective
    01-+-*2 Fin.zero (Fin.suc Fin.zero) m n = ⊥-elim ∘ *2-absurd m n
    01-+-*2 Fin.zero (Fin.suc (Fin.suc ())) m n
    01-+-*2 (Fin.suc Fin.zero) Fin.zero m n = ⊥-elim ∘ *2-absurd n m ∘ ≡.sym
    01-+-*2 (Fin.suc (Fin.suc ())) Fin.zero m n
    01-+-*2 (Fin.suc Fin.zero) (Fin.suc Fin.zero) m n = *2-injective m n ∘ Nat.suc-injective
    01-+-*2 (Fin.suc Fin.zero) (Fin.suc (Fin.suc ())) m n
    01-+-*2 (Fin.suc (Fin.suc ())) (Fin.suc Fin.zero) m n
    01-+-*2 (Fin.suc (Fin.suc ())) (Fin.suc (Fin.suc j)) m n

    +-injective₂ : ∀ m n o → o + m ≡ o + n → m ≡ n
    +-injective₂ m n zero = id
    +-injective₂ m n (suc o) = +-injective₂ m n o ∘ Nat.suc-injective

    +-injective₁ : ∀ m n o → m + o ≡ n + o → m ≡ n
    +-injective₁ m n o p = +-injective₂ m n o (≡.trans (Nat.+-comm o m) (≡.trans p (Nat.+-comm n o)))

    lookupOrElse-fromDigits : ∀ {n} (i : Fin n) (xs ys : List (Fin 2)) → fromDigits xs ≡ fromDigits ys → lookupOrElse Fin.zero i xs ≡ lookupOrElse Fin.zero i ys
    lookupOrElse-fromDigits i [] [] p = ≡.refl
    lookupOrElse-fromDigits Fin.zero [] (Fin.zero ∷ ys) p = ≡.refl
    lookupOrElse-fromDigits Fin.zero [] (Fin.suc y ∷ ys) ()
    lookupOrElse-fromDigits (Fin.suc i) [] (Fin.zero ∷ ys) p = lookupOrElse-fromDigits i [] ys (*2-injective 0 _ p)
    lookupOrElse-fromDigits (Fin.suc i) [] (Fin.suc y ∷ ys) ()
    lookupOrElse-fromDigits Fin.zero (Fin.zero ∷ xs) [] p = ≡.refl
    lookupOrElse-fromDigits Fin.zero (Fin.suc x ∷ xs) [] ()
    lookupOrElse-fromDigits {Nat.suc n} Fin.zero (x ∷ xs) (y ∷ ys) p =
      let q = 01-+-*2 x y (fromDigits xs) (fromDigits ys) p
          p′ = ≡.subst (λ fdys → Fin.toℕ x + fromDigits xs * 2 ≡ Fin.toℕ y + fdys) (≡.cong₂ _*_ (≡.sym q) ≡.refl) p
          p′′ = +-injective₁ (Fin.toℕ x) (Fin.toℕ y) _ p′
      in Fin.toℕ-injective p′′
    lookupOrElse-fromDigits (Fin.suc i) (Fin.zero ∷ xs) [] p = lookupOrElse-fromDigits i xs [] (*2-injective _ _ p)
    lookupOrElse-fromDigits (Fin.suc i) (Fin.suc x ∷ xs) [] ()
    lookupOrElse-fromDigits (Fin.suc i) (x ∷ xs) (y ∷ ys) p =
      lookupOrElse-fromDigits i xs ys (01-+-*2 x y (fromDigits xs) (fromDigits ys) p)

    toDigits-fromDigits : ∀ {n} (i : Fin n) xs → lookupOrElse Fin.zero i (proj₁ (toDigits 2 (fromDigits xs))) ≡ lookupOrElse Fin.zero i xs
    toDigits-fromDigits i xs with toDigits 2 (fromDigits xs)
    toDigits-fromDigits i xs | ds , p = lookupOrElse-fromDigits i ds xs p

  asNat : LeftInverse (FiniteSet.setoid A-finiteSet ⇨ ≡.setoid Bool) (≡.setoid ℕ)
  _⟨$⟩_ (to asNat) f = fromDigits (Table.toList (Table.map (fromBool ∘ (f ⟨$⟩_)) A.enumₜ))
  cong (to asNat) {f} p = ≡.cong fromDigits {x = Table.toList (Table.map (fromBool ∘ (f ⟨$⟩_)) A.enumₜ)} (List.tabulate-cong λ x → ≡.cong fromBool (p A.refl))
  _⟨$⟩_ (_⟨$⟩_ (from asNat) n) x = toBool (lookupOrElse Fin.zero (A.toIx x) (proj₁ (toDigits 2 n)))
  cong (_⟨$⟩_ (from asNat) n) {x} {y} = ≡.cong (λ i → toBool (lookupOrElse Fin.zero i (proj₁ (toDigits 2 n)))) ∘ cong (to A.ontoFin)
  cong (from asNat) {n} ≡.refl = cong (_⟨$⟩_ (from asNat) n)
  left-inverse-of asNat f {x} {y} p =
    begin
      toBool (lookupOrElse Fin.zero (A.toIx x) (proj₁ (toDigits 2 (fromDigits (Table.toList (Table.map (fromBool ∘ (f ⟨$⟩_)) A.enumₜ))))))
    ≡⟨ ≡.cong toBool (toDigits-fromDigits (A.toIx x) (Table.toList (Table.map (fromBool ∘ (f ⟨$⟩_)) A.enumₜ))) ⟩
      toBool (lookupOrElse Fin.zero (A.toIx x) (Table.toList (Table.map (fromBool ∘ (f ⟨$⟩_)) A.enumₜ)))
    ≡⟨ ≡.cong toBool (lookupOrElse-toList (A.toIx x) _) ⟩
      toBool (Table.lookup (Table.map (fromBool ∘ (f ⟨$⟩_)) A.enumₜ) (A.toIx x))
    ≡⟨⟩
      toBool (fromBool (f ⟨$⟩ (from A.ontoFin ⟨$⟩ (to A.ontoFin ⟨$⟩ x))))
    ≡⟨ toBool-fromBool _ ⟩
      f ⟨$⟩ (from A.ontoFin ⟨$⟩ (to A.ontoFin ⟨$⟩ x))
    ≡⟨ cong f (left-inverse-of A.ontoFin x) ⟩
      f ⟨$⟩ x
    ≡⟨ cong f p ⟩
      f ⟨$⟩ y
    ∎
    where open ≡.Reasoning


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Implications of nullary relations
------------------------------------------------------------------------

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

module Relation.Nullary.Implication where

open import Data.Bool.Base
open import Data.Empty
open import Function.Base
open import Relation.Nullary
open import Level

private
  variable
    p q : Level
    P : Set p
    Q : Set q

------------------------------------------------------------------------
-- Some properties which are preserved by _→_.

infixr 2 _→-reflects_ _→-dec_

_→-reflects_ : ∀ {bp bq} → Reflects P bp → Reflects Q bq →
                           Reflects (P → Q) (not bp ∨ bq)
ofʸ  p →-reflects ofʸ  q = ofʸ (const q)
ofʸ  p →-reflects ofⁿ ¬q = ofⁿ (¬q ∘ (_$ p))
ofⁿ ¬p →-reflects _      = ofʸ (⊥-elim ∘ ¬p)

_→-dec_ : Dec P → Dec Q → Dec (P → Q)
does  (p? →-dec q?) = not (does p?) ∨ does q?
proof (p? →-dec q?) = proof p? →-reflects proof q?


text:
{-# OPTIONS --cubical --safe #-}

module Data.Binary.PerformanceTests.Subtraction where

open import Prelude
open import Data.Binary.Definition
open import Data.Binary.Addition using (_+_)
open import Data.Binary.Subtraction using (_-_)
open import Data.Binary.Multiplication using (_*_)

sub-r  : 𝔹 → 𝔹 → ℕ → 𝔹
sub-r a x zero = a
sub-r a x (suc n) = sub-r a x n - x

sub-l  : 𝔹 → 𝔹 → ℕ → 𝔹
sub-l a x zero = a
sub-l a x (suc n) = sub-r (a - x) x n

one-thousand : 𝔹
one-thousand = 2ᵇ 1ᵇ 1ᵇ 2ᵇ 1ᵇ 2ᵇ 2ᵇ 2ᵇ 2ᵇ 0ᵇ

f : 𝔹
f = one-thousand * one-thousand * one-thousand

n : ℕ
n = 99999

-- The actual performance test (uncomment and time how long it takes to type-check)
-- _ : sub-l f one-thousand n ≡ sub-r f one-thousand n
-- _ = refl

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------------
-- Common definitions
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module Common.DefinitionsATP where

open import Common.FOL.FOL using ( ¬_ ; D )
open import Common.FOL.Relation.Binary.PropositionalEquality using ( _≡_ )

infix 4 _≢_

------------------------------------------------------------------------------
-- Inequality.
_≢_ : D → D → Set
x ≢ y = ¬ x ≡ y
{-# ATP definition _≢_ #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- Convenient syntax for "equational reasoning" using a indexed preorder
------------------------------------------------------------------------

open import Relation.Binary.Indexed.Extra

module Relation.Binary.Indexed.PreorderReasoning {𝒾} {I : Set 𝒾} {𝒸 ℓ₁ ℓ₂} (P : Preorder I 𝒸 ℓ₁ ℓ₂) where

open Preorder P

infix  4 _IsRelatedTo_
infix  1 begin_
infix  3 _∎
infixr 2 _∼⟨_⟩_ _≈⟨_⟩_ _≈⟨⟩_

data _IsRelatedTo_ {i j : I} (x : Carrier i) (y : Carrier j) : Set ℓ₂ where
    relTo : (x∼y : x ∼ y) → x IsRelatedTo y

begin_ : ∀ {i j : I} {x : Carrier i} {y : Carrier j} →  x IsRelatedTo y → x ∼ y
begin relTo x∼y = x∼y

_∼⟨_⟩_ : ∀ {i j k : I} → (x : Carrier i)
    → {y : Carrier j} {z : Carrier k}
    → x ∼ y → y IsRelatedTo z → x IsRelatedTo z
_ ∼⟨ x∼y ⟩ relTo y∼z = relTo (trans x∼y y∼z)

_≈⟨_⟩_ : ∀ {i j k : I} → (x : Carrier i)
    → {y : Carrier j} {z : Carrier k}
    → x ≈ y → y IsRelatedTo z → x IsRelatedTo z
_ ≈⟨ x≈y ⟩ relTo y∼z = relTo (trans (reflexive x≈y) y∼z)

_≈⟨⟩_ : ∀ {i j : I} → (x : Carrier i) → {y : Carrier j}
    → x IsRelatedTo y → x IsRelatedTo y
_ ≈⟨⟩ x∼y = x∼y

_∎ : ∀ {i : I} (x : Carrier i) → x IsRelatedTo x
_∎ _ = relTo refl

max_stars_repo_name: banacorn/categories

max_issues_repo_name: banacorn/categories

max_forks_repo_name: banacorn/categories


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Rings.Definition
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Rings.IntegralDomains.Definition
open import Rings.IntegralDomains.Lemmas

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Fields.FieldOfFractions.Setoid {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (I : IntegralDomain R) where

record fieldOfFractionsSet : Set (a ⊔ b) where
  field
    num : A
    denom : A
    .denomNonzero : (Setoid._∼_ S denom (Ring.0R R) → False)

fieldOfFractionsSetoid : Setoid fieldOfFractionsSet
Setoid._∼_ fieldOfFractionsSetoid (record { num = a ; denom = b ; denomNonzero = b!=0 }) (record { num = c ; denom = d ; denomNonzero = d!=0 }) = Setoid._∼_ S (a * d) (b * c)
Equivalence.reflexive (Setoid.eq fieldOfFractionsSetoid) {record { num = a ; denom = b ; denomNonzero = b!=0 }} = Ring.*Commutative R
Equivalence.symmetric (Setoid.eq fieldOfFractionsSetoid) {record { num = a ; denom = b ; denomNonzero = b!=0 }} {record { num = c ; denom = d ; denomNonzero = d!=0 }} ad=bc = transitive (Ring.*Commutative R) (transitive (symmetric ad=bc) (Ring.*Commutative R))
  where
    open Equivalence (Setoid.eq S)
Equivalence.transitive (Setoid.eq fieldOfFractionsSetoid) {record { num = a ; denom = b ; denomNonzero = b!=0 }} {record { num = c ; denom = d ; denomNonzero = d!=0 }} {record { num = e ; denom = f ; denomNonzero = f!=0 }} ad=bc cf=de = p5
  where
    open Setoid S
    open Ring R
    open Equivalence eq
    p : (a * d) * f ∼ (b * c) * f
    p = Ring.*WellDefined R ad=bc reflexive
    p2 : (a * f) * d ∼ b * (d * e)
    p2 = transitive (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) (transitive p (transitive (symmetric *Associative) (*WellDefined reflexive cf=de)))
    p3 : (a * f) * d ∼ (b * e) * d
    p3 = transitive p2 (transitive (*WellDefined reflexive *Commutative) *Associative)
    p4 : ((d ∼ 0R) → False) → ((a * f) ∼ (b * e))
    p4 = cancelIntDom I (transitive *Commutative (transitive p3 *Commutative))
    p5 : (a * f) ∼ (b * e)
    p5 = p4 λ t → exFalso (d!=0 t)


text:
open import Mockingbird.Forest using (Forest)

-- Curry’s Lively Bird Forest
module Mockingbird.Problems.Chapter14 {b ℓ} (forest : Forest {b} {ℓ}) where

open import Data.Product using (_×_; _,_; ∃-syntax; proj₁; proj₂)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function using (_$_; _⇔_; Equivalence; mk⇔)
open import Level using (_⊔_)
open import Relation.Binary using (_Respects_)
open import Relation.Nullary using (¬_)
open import Relation.Unary using (Pred)

open import Mockingbird.Forest.Birds forest
import Mockingbird.Problems.Chapter09 forest as Chapter₉

open Forest forest

module _ {s} (Sings : Pred Bird s)
         (respects : Sings Respects _≈_)
         -- This law of excluded middle is not stated in the problem as one of
         -- the laws, but in the solution given in the book, it is used.
         (LEM : ∀ x → Sings x ⊎ ¬ Sings x)
         (P : Bird) where

  module _ (law₁ : ∀ {x y} → Sings y → Sings (P ∙ x ∙ y))
           (law₂ : ∀ {x y} → ¬ (Sings x) → Sings (P ∙ x ∙ y))
           (law₃ : ∀ {x y} → Sings x → Sings (P ∙ x ∙ y) → Sings y)
           (law₄ : ∀ x → ∃[ y ] Sings y ⇔ Sings (P ∙ y ∙ x)) where

    problem₁ : ∀ x → Sings x
    problem₁ x = law₃ (proj₂ (law₄-⇐ x) Pyx-sings) Pyx-sings
      where
        -- If y sings on all days on which x sings, then Pxy sings on all days.
        lemma-Pxy : ∀ y x → (Sings y → Sings x) → Sings (P ∙ y ∙ x)
        lemma-Pxy y x y-sings⇒x-sings with LEM y
        ... | inj₁ y-sings = law₁ (y-sings⇒x-sings y-sings)
        ... | inj₂ ¬y-sings = law₂ ¬y-sings

        law₄-⇒ : ∀ x → ∃[ y ] (Sings y → Sings (P ∙ y ∙ x))
        law₄-⇒ x =
          let (y , p) = law₄ x
          in (y , Equivalence.f p)

        law₄-⇐ : ∀ x → ∃[ y ] (Sings (P ∙ y ∙ x) → Sings y)
        law₄-⇐ x =
          let (y , p) = law₄ x
          in (y , Equivalence.g p)

        y = proj₁ $ law₄ x

        y-sings⇒x-sings : Sings y → Sings x
        y-sings⇒x-sings y-sings = law₃ y-sings $ proj₂ (law₄-⇒ x) y-sings

        Pyx-sings : Sings (P ∙ y ∙ x)
        Pyx-sings = lemma-Pxy y x y-sings⇒x-sings

  module _ (law₁ : ∀ {x y} → Sings y → Sings (P ∙ x ∙ y))
           (law₂ : ∀ {x y} → ¬ Sings (x) → Sings (P ∙ x ∙ y))
           (law₃ : ∀ {x y} → Sings x → Sings (P ∙ x ∙ y) → Sings y)
           ⦃ _ : HasCardinal ⦄ ⦃ _ : HasLark ⦄ where

    problem₂ : ∀ x → Sings x
    problem₂ = problem₁ law₁ law₂ law₃ $ λ x →
      let -- There exists a bird of which CPx is fond.
          (y , isFond) = Chapter₉.problem₂₅ (C ∙ P ∙ x)

          Pyx≈y : P ∙ y ∙ x ≈ y
          Pyx≈y = begin
            P ∙ y ∙ x      ≈˘⟨ isCardinal P x y ⟩
            C ∙ P ∙ x ∙ y  ≈⟨ isFond ⟩
            y              ∎

          law₄ : Sings y ⇔ Sings (P ∙ y ∙ x)
          law₄ = mk⇔ (respects (sym Pyx≈y)) (respects Pyx≈y)
      in (y , law₄)

  module _ (law₁ : ∀ {x y} → Sings y → Sings (P ∙ x ∙ y))
           (law₂ : ∀ {x y} → ¬ Sings (x) → Sings (P ∙ x ∙ y))
           (law₃ : ∀ {x y} → Sings x → Sings (P ∙ x ∙ y) → Sings y) where

    problem₃ : ∃[ A ] (∀ x y z → A ∙ x ∙ y ∙ z ≈ x ∙ (z ∙ z) ∙ y) → ∀ x → Sings x
    problem₃ (A , Axyz≈x[zz]y) = problem₁ law₁ law₂ law₃ $ λ x →
      let y = A ∙ P ∙ x ∙ (A ∙ P ∙ x)

          y≈Pyx : y ≈ P ∙ y ∙ x
          y≈Pyx = begin
            y                                  ≈⟨⟩
            A ∙ P ∙ x ∙ (A ∙ P ∙ x)            ≈⟨ Axyz≈x[zz]y P x (A ∙ P ∙ x) ⟩
            P ∙ (A ∙ P ∙ x ∙ (A ∙ P ∙ x)) ∙ x  ≈⟨⟩
            (P ∙ y ∙ x                         ∎)

          law₄ : Sings y ⇔ Sings (P ∙ y ∙ x)
          law₄ = mk⇔ (respects y≈Pyx) (respects (sym y≈Pyx))
      in (y , law₄)

-- -- TODO: bonus exercises

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


text:
open import Nat
open import Prelude
open import core

open import lemmas-gcomplete

module lemmas-complete where
  lem-comp-pair1 : ∀{d1 d2} → ⟨ d1 , d2 ⟩ dcomplete → d1 dcomplete
  lem-comp-pair1 (DCPair h _) = h

  lem-comp-pair2 : ∀{d1 d2} → ⟨ d1 , d2 ⟩ dcomplete → d2 dcomplete
  lem-comp-pair2 (DCPair _ h) = h

  lem-comp-prod1 : ∀{τ1 τ2} → τ1 ⊗ τ2 tcomplete → τ1 tcomplete
  lem-comp-prod1 (TCProd h _) = h

  lem-comp-prod2 : ∀{τ1 τ2} → τ1 ⊗ τ2 tcomplete → τ2 tcomplete
  lem-comp-prod2 (TCProd _ h) = h

  -- no term is both complete and indeterminate
  lem-ind-comp : ∀{d} → d dcomplete → d indet → ⊥
  lem-ind-comp DCVar ()
  lem-ind-comp DCConst ()
  lem-ind-comp (DCLam comp x₁) ()
  lem-ind-comp (DCAp comp comp₁) (IAp x ind x₁) = lem-ind-comp comp ind
  lem-ind-comp (DCCast comp x x₁) (ICastArr x₂ ind) = lem-ind-comp comp ind
  lem-ind-comp (DCCast comp x x₁) (ICastGroundHole x₂ ind) = lem-ind-comp comp ind
  lem-ind-comp (DCCast comp x x₁) (ICastHoleGround x₂ ind x₃) = lem-ind-comp comp ind
  lem-ind-comp (DCCast dc x x₁) (ICastProd x₂ ind) = lem-ind-comp dc ind
  lem-ind-comp (DCFst d) (IFst ind x x₁) = lem-ind-comp d ind
  lem-ind-comp (DCSnd d) (ISnd ind x x₁) = lem-ind-comp d ind
  lem-ind-comp (DCPair d d₁) (IPair1 ind x) = lem-ind-comp d ind
  lem-ind-comp (DCPair d d₁) (IPair2 x ind) = lem-ind-comp d₁ ind

  -- complete types that are consistent are equal
  complete-consistency : ∀{τ1 τ2} → τ1 ~ τ2 → τ1 tcomplete → τ2 tcomplete → τ1 == τ2
  complete-consistency TCRefl TCBase comp2 = refl
  complete-consistency TCRefl (TCArr comp1 comp2) comp3 = refl
  complete-consistency TCHole1 comp1 ()
  complete-consistency TCHole2 () comp2
  complete-consistency (TCArr consis consis₁) (TCArr comp1 comp2) (TCArr comp3 comp4)
   with complete-consistency consis comp1 comp3 | complete-consistency consis₁ comp2 comp4
  ... | refl | refl = refl
  complete-consistency TCRefl (TCProd tc' tc'') = λ _ → refl
  complete-consistency (TCProd tc tc') (TCProd tc1 tc2) (TCProd tc3 tc4)
    with complete-consistency tc tc1 tc3 | complete-consistency tc' tc2 tc4
  ... | refl | refl = refl

  -- a well typed complete term is assigned a complete type
  complete-ta : ∀{Γ Δ d τ} → (Γ gcomplete) →
                             (Δ , Γ ⊢ d :: τ) →
                             d dcomplete →
                             τ tcomplete
  complete-ta gc TAConst comp = TCBase
  complete-ta gc (TAVar x₁) DCVar = gc _ _ x₁
  complete-ta gc (TALam a wt) (DCLam comp x₁) = TCArr x₁ (complete-ta (gcomp-extend gc x₁ a ) wt comp)
  complete-ta gc (TAAp wt wt₁) (DCAp comp comp₁) with complete-ta gc wt comp
  complete-ta gc (TAAp wt wt₁) (DCAp comp comp₁) | TCArr qq qq₁ = qq₁
  complete-ta gc (TAEHole x x₁) ()
  complete-ta gc (TANEHole x wt x₁) ()
  complete-ta gc (TACast wt x) (DCCast comp x₁ x₂) = x₂
  complete-ta gc (TAFailedCast wt x x₁ x₂) ()
  complete-ta gc (TAFst wt) (DCFst comp) = lem-comp-prod1 (complete-ta gc wt comp)
  complete-ta gc (TASnd wt) (DCSnd comp) = lem-comp-prod2 (complete-ta gc wt comp)
  complete-ta gc (TAPair ta ta₁) (DCPair comp comp₁) = TCProd (complete-ta gc ta comp) (complete-ta gc ta₁ comp₁)

  -- a well typed term synthesizes a complete type
  comp-synth : ∀{Γ e τ} →
                   Γ gcomplete →
                   e ecomplete →
                   Γ ⊢ e => τ →
                   τ tcomplete
  comp-synth gc ec SConst = TCBase
  comp-synth gc (ECAsc x ec) (SAsc x₁) = x
  comp-synth gc ec (SVar x) = gc _ _ x
  comp-synth gc (ECAp ec ec₁) (SAp _ wt MAHole x₁) with comp-synth gc ec wt
  ... | ()
  comp-synth gc (ECAp ec ec₁) (SAp _ wt MAArr x₁) with comp-synth gc ec wt
  comp-synth gc (ECAp ec ec₁) (SAp _ wt MAArr x₁) | TCArr qq qq₁ = qq₁
  comp-synth gc () SEHole
  comp-synth gc () (SNEHole _ wt)
  comp-synth gc (ECLam2 ec x₁) (SLam x₂ wt) = TCArr x₁ (comp-synth (gcomp-extend gc x₁ x₂) ec wt)
  comp-synth gc (ECFst ec) (SFst wt MPHole) = comp-synth gc ec wt
  comp-synth gc (ECFst ec) (SFst wt MPProd) = lem-comp-prod1 (comp-synth gc ec wt)
  comp-synth gc (ECSnd ec) (SSnd wt MPHole) = comp-synth gc ec wt
  comp-synth gc (ECSnd ec) (SSnd wt MPProd) = lem-comp-prod2 (comp-synth gc ec wt)
  comp-synth gc (ECPair ec ec₁) (SPair x wt wt₁) = TCProd (comp-synth gc ec wt) (comp-synth gc ec₁ wt₁)

  -- complete boxed values are just values
  lem-comp-boxed-val : {Δ : hctx} {d : iexp} {τ : typ} {Γ : tctx} →
                           Δ , Γ ⊢ d :: τ →
                           d dcomplete →
                           d boxedval →
                           d val
  lem-comp-boxed-val wt comp (BVVal VConst) = VConst
  lem-comp-boxed-val wt comp (BVVal VLam) = VLam
  lem-comp-boxed-val wt comp (BVVal (VPair x x₁)) = VPair x x₁
  lem-comp-boxed-val (TAPair wt wt₁) (DCPair comp comp₁) (BVPair bv bv₁) = VPair (lem-comp-boxed-val wt comp bv)
                                                                                (lem-comp-boxed-val wt₁ comp₁ bv₁)
  lem-comp-boxed-val (TACast wt x₃) (DCCast comp x₁ x₂) (BVArrCast x bv) = abort (x (complete-consistency x₃ x₁ x₂))
  lem-comp-boxed-val (TACast wt x₁) (DCCast comp x₂ x₃) (BVProdCast x bv) = abort (x (complete-consistency x₁ x₂ x₃))
  lem-comp-boxed-val (TACast wt x₁) (DCCast comp x₂ ()) (BVHoleCast x bv)

max_stars_repo_name: hazelgrove/hazel-palette-agda

max_issues_repo_name: hazelgrove/hazel-palette-agda

max_forks_repo_name: hazelgrove/hazelnut-livelits-agda


text:
-- Andreas, 2015-12-12, report by Ulf, 2015-12-09

{-# OPTIONS -v tc.with.40 #-}

open import Common.Equality
open import Common.Bool

T : Bool → Set
T true  = Bool
T false = true ≡ false

foo : (a b : Bool) → a ≡ b → T a → T b
foo a b eq x rewrite eq = x

data _≅_ {A : Set} (x : A) : {B : Set} → B → Set where
  refl : x ≅ x

-- Intended new rewrite
refl-rewrite : ∀ a (eq : a ≡ a) (t : T a) → foo a a eq t ≡ t
refl-rewrite a eq t with eq
refl-rewrite a eq t | refl = refl

test : ∀ a (eq : a ≡ a) (t : T a) → foo a a eq t ≡ t
test a eq t rewrite eq = refl  -- FAILS, this is the original issue report
-- Error:
-- foo a a eq t | a | eq != t of type T a
-- when checking that the expression refl has type foo a a eq t ≡ t
-- test a refl t = refl  -- WORKS, of course

-- Non-reflexive rewrite
works : ∀ a b (eq : a ≡ b) (t : T a) → foo a b eq t ≅ t
works a b eq t rewrite eq = refl

-- Manual desugaring of old-style rewrite works as well
old-rewrite : ∀ a (eq : a ≡ a) (t : T a) → foo a a eq t ≡ t
old-rewrite a eq t with a | eq
old-rewrite a eq t | _ | refl = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Cubical.Core.Everything
open import Cubical.Relation.Binary
open import Cubical.Algebra.Magma

module Cubical.Algebra.Magma.Construct.Quotient {c ℓ} (M : Magma c) {R : Rel ⟨ M ⟩ ℓ} (isEq : IsEquivalence R)
                                                    (closed : Congruent₂ R (Magma._•_ M)) where

open import Cubical.Algebra.Properties
open import Cubical.HITs.SetQuotients

open Magma M
open IsEquivalence isEq

Carrier/R = Carrier / R

_•ᴿ_ : Op₂ Carrier/R
_•ᴿ_ = rec2 squash/ (λ x y → [ x • y ]) (λ _ _ _ eq → eq/ _ _ (cong₂⇒rcong R reflexive _•_ closed eq))
                                        (λ _ _ _ eq → eq/ _ _ (cong₂⇒lcong R reflexive _•_ closed eq))

M/R-isMagma : IsMagma Carrier/R _•ᴿ_
M/R-isMagma = record { is-set = squash/ }

M/R : Magma (ℓ-max c ℓ)
M/R = record { isMagma = M/R-isMagma }


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Rationals.QuoQ.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv

open import Cubical.Data.Nat as ℕ using (discreteℕ)
open import Cubical.Data.NatPlusOne
open import Cubical.Data.Sigma

open import Cubical.HITs.Ints.QuoInt
open import Cubical.HITs.SetQuotients as SetQuotient
  using ([_]; eq/; discreteSetQuotients) renaming (_/_ to _//_) public

open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary.Base

ℕ₊₁→ℤ : ℕ₊₁ → ℤ
ℕ₊₁→ℤ n = pos (ℕ₊₁→ℕ n)

private
  ℕ₊₁→ℤ-hom : ∀ m n → ℕ₊₁→ℤ (m ·₊₁ n) ≡ ℕ₊₁→ℤ m · ℕ₊₁→ℤ n
  ℕ₊₁→ℤ-hom _ _ = refl

-- ℚ as a set quotient of ℤ × ℕ₊₁ (as in the HoTT book)

_∼_ : ℤ × ℕ₊₁ → ℤ × ℕ₊₁ → Type₀
(a , b) ∼ (c , d) = a · ℕ₊₁→ℤ d ≡ c · ℕ₊₁→ℤ b

ℚ : Type₀
ℚ = (ℤ × ℕ₊₁) // _∼_

isSetℚ : isSet ℚ
isSetℚ = SetQuotient.squash/

[_/_] : ℤ → ℕ₊₁ → ℚ
[ a / b ] = [ a , b ]

isEquivRel∼ : isEquivRel _∼_
isEquivRel.reflexive isEquivRel∼ (a , b) = refl
isEquivRel.symmetric isEquivRel∼ (a , b) (c , d) = sym
isEquivRel.transitive isEquivRel∼ (a , b) (c , d) (e , f) p q = ·-injʳ _ _ _ r
  where r = (a · ℕ₊₁→ℤ f) · ℕ₊₁→ℤ d ≡[ i ]⟨ ·-comm a (ℕ₊₁→ℤ f) i · ℕ₊₁→ℤ d ⟩
            (ℕ₊₁→ℤ f · a) · ℕ₊₁→ℤ d ≡⟨ sym (·-assoc (ℕ₊₁→ℤ f) a (ℕ₊₁→ℤ d)) ⟩
            ℕ₊₁→ℤ f · (a · ℕ₊₁→ℤ d) ≡[ i ]⟨ ℕ₊₁→ℤ f · p i ⟩
            ℕ₊₁→ℤ f · (c · ℕ₊₁→ℤ b) ≡⟨ ·-assoc (ℕ₊₁→ℤ f) c (ℕ₊₁→ℤ b) ⟩
            (ℕ₊₁→ℤ f · c) · ℕ₊₁→ℤ b ≡[ i ]⟨ ·-comm (ℕ₊₁→ℤ f) c i · ℕ₊₁→ℤ b ⟩
            (c · ℕ₊₁→ℤ f) · ℕ₊₁→ℤ b ≡[ i ]⟨ q i · ℕ₊₁→ℤ b ⟩
            (e · ℕ₊₁→ℤ d) · ℕ₊₁→ℤ b ≡⟨ sym (·-assoc e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ⟩
            e · (ℕ₊₁→ℤ d · ℕ₊₁→ℤ b) ≡[ i ]⟨ e · ·-comm (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b) i ⟩
            e · (ℕ₊₁→ℤ b · ℕ₊₁→ℤ d) ≡⟨ ·-assoc e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d) ⟩
            (e · ℕ₊₁→ℤ b) · ℕ₊₁→ℤ d ∎

eq/⁻¹ : ∀ x y → Path ℚ [ x ] [ y ] → x ∼ y
eq/⁻¹ = SetQuotient.effective (λ _ _ → isSetℤ _ _) isEquivRel∼

discreteℚ : Discrete ℚ
discreteℚ = discreteSetQuotients (discreteΣ discreteℤ (λ _ → subst Discrete 1+Path discreteℕ))
                                 (λ _ _ → isSetℤ _ _) isEquivRel∼ (λ _ _ → discreteℤ _ _)

-- Natural number and negative integer literals for ℚ

open import Cubical.Data.Nat.Literals public

instance
  fromNatℚ : HasFromNat ℚ
  fromNatℚ = record { Constraint = λ _ → Unit ; fromNat = λ n → [ pos n / 1 ] }

instance
  fromNegℚ : HasFromNeg ℚ
  fromNegℚ = record { Constraint = λ _ → Unit ; fromNeg = λ n → [ neg n / 1 ] }

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
module Functors.FullyFaithful where

open import Library
open import Categories
open import Functors
open import Naturals hiding (Iso)
open import Isomorphism

open Cat
open Fun

FullyFaithful : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}
                (F : Fun C D) → Set (a ⊔ b ⊔ d)
FullyFaithful {C = C}{D = D} F =
  ∀ (X Y : Obj C) → Iso (Hom D (OMap F X) (OMap F Y)) (Hom C X Y)

Full : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}
                (F : Fun C D) → Set _
Full {C = C}{D = D} F = ∀ {X Y}(h : Hom D (OMap F X) (OMap F Y)) →
  Σ (Hom C X Y) \ f -> HMap F f ≅ h

Faithful : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}
                (F : Fun C D) → Set _
Faithful {C = C}{D = D} F = ∀{X Y}{f g : Hom C X Y} → HMap F f ≅ HMap F g → f ≅ g

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
-- WARNING: This file was generated automatically by Vehicle
-- and should not be modified manually!
-- Metadata
--  - Agda version: 2.6.2
--  - AISEC version: 0.1.0.1
--  - Time generated: ???

{-# OPTIONS --allow-exec #-}

open import Vehicle
open import Vehicle.Data.Tensor
open import Data.Rational as ℚ using (ℚ)
open import Data.Fin as Fin using (Fin; #_)
open import Data.List

module increasing-temp-output where

postulate f : Tensor ℚ (1 ∷ []) → Tensor ℚ (1 ∷ [])

abstract
  increasing : ∀ (x : ℚ) → x ℚ.≤ f (x ∷ []) (# 0)
  increasing = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

max_stars_repo_name: vehicle-lang/vehicle

max_issues_repo_name: vehicle-lang/vehicle

max_forks_repo_name: vehicle-lang/vehicle


text:
module AgdaCheatSheet where

open import Level using (Level)
open import Data.Nat
open import Data.Bool hiding (_<?_)
open import Data.List using (List; []; _∷_; length)

-- https://alhassy.github.io/AgdaCheatSheet/CheatSheet.pdf

{-
------------------------------------------------------------------------------
-- dependent function

A function whose RESULT type depends on the VALUE of the argument.
  -- given  value  of type A
  -- return result of type B a
  (a : A) → B a

E.g., generic identity
-- input
--  the type of X
--  value of type X
-- output a function X → X
-}
id0 : (X : Set) → X → X
id0 X x = x

id1 id2 id3 : (X : Set) → X → X
id1 X = λ x → x

id2 = λ X x → x
id3 = λ (X : Set) (x : X) → x

-- call it
sad : ℕ
sad = id0 ℕ 3

{-
------------------------------------------------------------------------------
-- implicits

In above, type arg can be inferred.
Use curly braces to mark arg as implicit.
-}

id : {X : Set} → X → X
id x = x

-- call it
nice : ℕ
nice = id 3

-- call with explicit implicit
explicit : ℕ
explicit = id {ℕ} 3

-- call with explicit inferred implicit
explicit’ : ℕ
explicit’ = id0 _ 3

{-
------------------------------------------------------------------------------
-- specifying arguments

{x : _} {y : _} (z : _) → · · ·        ≈ ∀ {x y} z → · · ·

(a1 : A) → (a2 : A) → (b : B) → · · ·  ≈ (a1 a2 : A) (b : B) → · · ·

------------------------------------------------------------------------------
-- dependent datatypes

-- data
-- name
-- arguments
-- type of the datatype
-- constructors and their types
-}

data Vec {ℓ : Level} (A : Set ℓ) : ℕ → Set ℓ where
  []   :                         Vec A  0
  _::_ : {n : ℕ} → A → Vec A n → Vec A (1 + n)

{-
For a given A, type of Vec A is N → Set.
Means Vec A is a FAMILY of types indexed by natural numbers:
- For each n, there is a TYPE Vec A n.

Vec is
- parametrised by A (and ℓ)
- indexed by n

A is type of elements
n is length

only way to Vec A 0 is via []
only way to Vec A (1 + n) is via _::_

enables safe head (since empty impossible)
-}

head : {A : Set} {n : ℕ} → Vec A (1 + n) → A
head (x :: xs) = x

{-
------------------------------------------------------------------------------
-- universes

ℓ arg says Vec is universe polymorphic
- can vectors of numbers and also vectors of types

Levels are essentially natural numbers:
- constructurs
  - lzero
  - lsuc
- _t_ : max of two levels

NO UNIVERSE OF ALL UNIVERSES:
- Set n has type Set n+1 for any n
- the type (n : Level) → Set n
  - is not itself typeable
  — i.e., is not in Set ℓ for any ℓ
  — Agda errors saying it is a value of Set ω

------------------------------------------------------------------------------
-- functions defined by pattern matching ALL cases

must terminate : so recursive calls must be made on structurally smaller arg
-}

infixr 40 _++_

_++_ : {A : Set} {n m : ℕ} → Vec A n → Vec A m → Vec A (n + m)
[]        ++ ys =             ys
(x :: xs) ++ ys = x :: (xs ++ ys)
{-
Append type encodes property : length of catenation is sum of args lengths

- Different types can have the same constructor names.
- Mixifx operators can be written prefix by having all underscores mentioned; e.g.,
- In def, if an arg is not needed, use _ (wildcard pattern)

------------------------------------------------------------------------------
-- Curry-Howard Correspondence — Propositions as Types

Logic                     Programming                 Example Use in Programming
================================================================================
proof / proposition       element / type              “p is a proof of P” ≈ “p is of type P”

true                      singleton type              return type of side-effect only methods
false                     empty type                  return type for non-terminating methods

⇒                         function type           →   methods with an input and output type
∧                         product type            ×   simple records of data and methods
∨                         sum type                +   enumerations or tagged unions

∀                         dependent function type Π   return type varies according to input value
∃                         dependent product  type Σ   record fields depend on each other’s values

natural deduction         type system                 ensuring only “meaningful” programs
hypothesis                free variable               global variables, closures

modus ponens              function application        executing methods on arguments
⇒ -introduction           λ-abstraction               parameters acting as local variables
                                                    to method definitions

induction;
elimination rules         Structural recursion        for-loops are precisely N-induction

Signature, term           Syntax; interface, record type, class
Algebra, Interpretation   Semantics; implementation, instance, object
Free Theory               Data structure
Inference rule            Algebraic datatype constructor
Monoid                    Untyped programming / composition
Category                  Typed programming / composition

------------------------------------------------------------------------------
-- equality

example of propositions-as-types : definition of identity relation (the least reflexive relation)
-}
data _≡_ {A : Set} : A → A → Set where
  refl : {x : A} → x ≡ x
  {-

states that refl {x}
- is a proof of l ≡ r
- whenever l and r simplify to x
  - by definition chasing only

Use it to prove Leibniz’s substitutivity rule, “equals for equals”:
-}
subst : {A : Set} {P : A → Set} {l r : A}
      → l ≡ r  -- must be of the form refl {x} for some canonical form x
      → P l    -- if l and r are both x, then P l and P r are the same type
      → P r    -- matching on proof l ≡ r gave infor about the rest of the program’s type
subst refl it = it

------------------------------------------------------------------------------
-- modules - namespace management

--------------------------------------------------
-- SIMPLE MODULES
module M where
  N : Set
  N = ℕ
  private
    x : ℕ
    x = 3
  y : N
  y = x + 1

-- using it - public names accessible by qualification or by opening them locally or globally
use0 : M.N
use0 = M.y

use1 : ℕ
use1 = y where open M
{- if open, then causes y in M' to duplicate
open M
use2 : ℕ
use2 = y
-}

--------------------------------------------------
-- PARAMETERISED MODULES : by arbitrarily many values and types (but not by other modules)
module M’ (x : ℕ) where
  y : ℕ
  y = x + 1

  -- names are functions
  --exposed : (x : ℕ) → ℕ
  --exposed = M’.y -- TODO compile error

-- using it
use’0 : ℕ
use’0 = M’.y 3

module M” = M’ 3
use” : ℕ
use” = M”.y

use’1 : ℕ
use’1 = y where open M’ 3

{-

“Using Them”:
- names in parameterised modules are are treated as functions
- can instantiate some parameters and name the resulting module
- can still open them as usual

--------------------------------------------------
-- ANONYMOUS MODULES
-- named-then-immediately-opened modules

module _ {A : Set} {a : A} · · ·
  ≈
module T {A : Set} {a : A} · · ·
open T

-- use-case : to  approximate the informal phrase
--   “for any A : Set and a : A, we have · · · ”

-- so common that variable keyword was introduced
--  Names in · · · are functions of only those variable-s they actually mention.

variable
  A : Set
  a : A

--------------------------------------------------
-- opening, using, hiding, renaming

open M hiding (n0; ...; nk)               : treat ni as private

open M using  (n0; ...; nk)               : treat only ni as public

open M renaming (n0 to m0; ...; nk to mk) : use names mi instead of ni

import X.Y.Z       : Use the definitions of module Z which lives in file ./X/Y/Z.agda.
open M public      : Treat the contents of M as if it is the public contents of the current module

Splitting a program over several files improves type checking performance,
since only need to type check files influenced by the change.

------------------------------------------------------------------------------
-- records : record ≈ module + data with one constructor
-}

record PointedSet : Set1 where
  constructor MkIt {- optional -}
  field
    Carrier : Set
    point   : Carrier

  {- like a module, so can add derived definitions -}
  blind : {A : Set} → A → Carrier
  blind = λ a → point

-- construct without named constructor
ex0 : PointedSet
ex0 = record {Carrier = ℕ; point = 3}

-- construct with named constructor
ex1 : PointedSet
ex1 = MkIt ℕ 3

open PointedSet
ex2 : PointedSet
Carrier ex2 = ℕ
point ex2 = 3

{-
Start with ex2 = ?, then in the hole enter C-c C-c RET to obtain the co-pattern setup.

Two tuples are the same when they have the same components.
Likewise a record is defined by its projections, whence co-patterns.
If you’re using many local definitions, you likely want to use co-patterns.

To enable projection of the fields from a record,
each record type comes with a module of the same name.
This module is parameterised by an element of the record type and
contains projection functions for the fields.
-}

useR0 : ℕ
useR0 = PointedSet.point ex0
{-
use¹ : ℕ
use¹ = point where open PointedSet ex0 -- TODO compile error
-}
open PointedSet
use² : ℕ
use² = blind ex0 true

-- pattern match on records

use³ : (P : PointedSet) → Carrier P
use³ record {Carrier = C; point = x} = x

use4 : (P : PointedSet) → Carrier P
use4 (MkIt C x) = x

{-
------------------------------------------------------------------------------
-- TODO Interacting with the real world —Compilation, Haskell, and IO

------------------------------------------------------------------------------
-- absurd patterns

When no constructor are matchable
- match the pattern ()
- provide no right hand side (since no way to could provide an arg to the function)

E.g., numbers smaller than a given natural number
-}

{- Fin n ∼= numbers i with i < n -}
data Fin : ℕ → Set where
  fzero : {n : ℕ} →         Fin (suc n) -- smaller than suc n for any n
  fsuc  : {n : ℕ} → Fin n → Fin (suc n) -- if i smaller than n then fsuc i is smaller than suc n.

{-
for each n, the type Fin n contains n elements
- Fin 2 has elements fsuc fzero and fzero
- Fin 0 has no elements

safe indexing function
-}
_!!_ : {A : Set} {n : ℕ} → Vec A n → Fin n → A
[]        !! ()               -- n is necessarily 0, but no way to make an element of type Fin 0
                              -- so use absurd pattern
(x :: xs) !! fzero  = x
(x :: xs) !! fsuc i = xs !! i

-- Logically “anything follows from false” becomes the following program:

data False : Set where

magic : {Anything-you-want : Set} → False → Anything-you-want
magic ()

{-
do
  magic x = ?
then case split on x
yields the program

------------------------------------------------------------------------------
-- isTrue pattern : passing around explicit proof objects
-- when not possible/easy to capture a desired precondition in types
-}

-- An empty record has only one value: record {} -}
record True : Set where

isTrue : Bool → Set
isTrue true  = True
isTrue false = False

_<0_ : ℕ → ℕ → Bool
_     <0  zero = false
zero  <0 suc y = true
suc x <0 suc y = x <0 y

find : {A : Set} (xs : List A) (i : ℕ) → isTrue (i <0 length xs) → A
find       []       i  ()
find (x ∷ xs)   zero  pf = x
find (x ∷ xs) (suc i) pf = find xs i pf

head’ : {A : Set} (xs : List A) → isTrue (0 <0 length xs) → A
head’       []  ()
head’ (x ∷ xs) _ = x

-- Unlike the _!!_ definition
-- rather than there being no index into the empty list
-- there is no proof that a natural number i is smaller than 0

{-
------------------------------------------------------------------------------
Mechanically Moving from Bool to Set —Avoiding “Boolean Blindness”

proposition represented as type whose elements denote proofs

Why use?
- awkward to request an index be “in bounds” in the find method,
- easier to encode this using Fin
- likewise, head’ is more elegant type when the non-empty precondition
  is part of the datatype definition, as in head.

recipe : from Boolean functions to inductive datatype families

1. Write the Boolean function.
2. Throw away all the cases with right side false.
3. Every case that has right side true corresponds to a new nullary constructor.
4. Every case that has n recursive calls corresponds to an n-ary constructor.

following these steps for _<0_:
-}

data _<1_ : ℕ → ℕ → Set where
  z< :   {y : ℕ} →          zero  <1     y
  s< : {x y : ℕ} → x <1 y → suc x <1 suc y

{-
then prove
- soundness    : constructed values correspond to Boolean-true statements
                 ensured by the second step in recipe
- completeness : true things correspond to terms formed from constructors.
-}

completeness : {x y : ℕ} → isTrue (x <0 y) → x <1 y
completeness     {x}  {zero} ()
completeness  {zero} {suc y} p = z<
completeness {suc x} {suc y} p = s< (completeness p)

{-
begin with
  completeness {x} {y} p = ?
then want case on p
but that requires evaluating x <0 y
which requires we know the shapes of x and y.

shape of proofs usually mimics the shape of definitions they use

------------------------------------------------------------------------------
record Payload (A : Set) : Set
  field
   pPayload  : [a]

record BlockType (A : Set) : Set
  = Proposal (Payload a) Author
  | NilBlock
  | Genesis

record LastVoteInfo
  fields
    lviLiDigest  :: HashValue
    lviRound     :: Round
    lviIsTimeout :: Bool
-}

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:
module Issue1486 where

open import Common.Prelude

postulate
  QName : Set
{-# BUILTIN QNAME QName #-}

primitive
  primShowQName : QName -> String

main : IO Unit
main = putStrLn (primShowQName (quote main))


text:
-- Andreas, 2014-10-05, issue reported by Stevan Andjelkovic

{-# OPTIONS --cubical-compatible #-}

postulate
  IO : Set → Set

record ⊤ : Set where
  constructor tt

record Container : Set₁ where
  field
    Shape    : Set
    Position : Shape → Set

open Container public

data W (A : Set) (B : A → Set) : Set where
  sup : (x : A) (f : B x → W A B) → W A B

postulate
  Ω : Container
  p : ∀ {s} → Position Ω s

mutual
  bad : W (Shape Ω) (Position Ω) → IO ⊤
  bad (sup c k) = helper c k

  helper : (s : Shape Ω) → (Position Ω s → W (Shape Ω) (Position Ω)) → IO ⊤
  helper _ k = bad (k p)

-- should pass termination check


text:
open import Coinduction using ( ∞ )
open import Data.ByteString using ( ByteString ; strict ; lazy )
open import Data.String using ( String )

module System.IO.Primitive where

infixl 1 _>>=_

-- The Unit type and its sole inhabitant

postulate
  Unit : Set
  unit : Unit

{-# COMPILED_TYPE Unit () #-}
{-# COMPILED unit () #-}

-- The IO type and its primitives
-- TODO: Make these universe-polymorphic once the compiler supports it

postulate
  IO : Set → Set
  return : {A : Set} → A → (IO A)
  _>>=_  : {A B : Set} → (IO A) → (A → (IO B)) → (IO B)
  inf : {A : Set} → ∞(IO A) → (IO A)

{-# BUILTIN IO IO #-}
{-# COMPILED_TYPE IO IO #-}
{-# COMPILED return (\ _ a -> return a) #-}
{-# COMPILED _>>=_ (\ _ _ a f -> a >>= f) #-}
-- {-# COMPILED inf (\ _ a -> a) #-}

-- The commitment primitives
postulate
  commit : IO Unit
  onCommit : (IO Unit) → (IO Unit)

{-# IMPORT System.IO.AgdaFFI #-}
{-# COMPILED commit System.IO.AgdaFFI.commit #-}
{-# COMPILED onCommit System.IO.AgdaFFI.onCommit #-}

-- The low-level binary handle primitives.
-- TODO: Should the string etc. functions be built on top of
-- the binary functions, or should we link directly to the Haskell
-- string functions?
-- TODO: Think about append and read-write modes.

postulate
  HandleR : Set
  stdin : HandleR
  hOpenR : String → (IO HandleR)
  hGetLazy : HandleR → (IO (ByteString lazy))
  hGetStrict : HandleR → (IO (ByteString strict))
  hCloseR : HandleR → (IO Unit)

{-# IMPORT System.IO #-}
{-# COMPILED_TYPE HandleR System.IO.Handle #-}
{-# COMPILED stdin System.IO.stdin #-}
{-# COMPILED hOpenR System.IO.AgdaFFI.hOpen System.IO.ReadMode #-}
{-# COMPILED hGetStrict System.IO.AgdaFFI.hGetStrict #-}
{-# COMPILED hGetLazy System.IO.AgdaFFI.hGetLazy #-}
{-# COMPILED hCloseR System.IO.AgdaFFI.hClose #-}

postulate
  HandleW : Set
  stdout : HandleW
  stderr : HandleW
  hOpenW : String → (IO HandleW)
  hPutLazy : HandleW → (ByteString lazy) → (IO Unit)
  hPutStrict : HandleW → (ByteString strict) → (IO Unit)
  hCloseW : HandleW → (IO Unit)

{-# COMPILED_TYPE HandleW System.IO.Handle #-}
{-# COMPILED stdout System.IO.stdout #-}
{-# COMPILED stderr System.IO.stderr #-}
{-# COMPILED hOpenW System.IO.AgdaFFI.hOpen System.IO.WriteMode #-}
{-# COMPILED hPutStrict System.IO.AgdaFFI.hPutStrict #-}
{-# COMPILED hPutLazy System.IO.AgdaFFI.hPutLazy #-}
{-# COMPILED hCloseW System.IO.AgdaFFI.hClose #-}

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io