text:
{-# OPTIONS --without-K --exact-split --allow-unsolved-metas #-}

module 10-number-theory where

import 09-truncation-levels
open 09-truncation-levels public

two-ℕ : ℕ
two-ℕ = succ-ℕ one-ℕ

three-ℕ : ℕ
three-ℕ = succ-ℕ two-ℕ

four-ℕ : ℕ
four-ℕ = succ-ℕ three-ℕ

five-ℕ : ℕ
five-ℕ = succ-ℕ four-ℕ

six-ℕ : ℕ
six-ℕ = succ-ℕ five-ℕ

seven-ℕ : ℕ
seven-ℕ = succ-ℕ six-ℕ

eight-ℕ : ℕ
eight-ℕ = succ-ℕ seven-ℕ

nine-ℕ : ℕ
nine-ℕ = succ-ℕ eight-ℕ

ten-ℕ : ℕ
ten-ℕ = succ-ℕ nine-ℕ

-- Section 10.1 Decidability.

{- Recall that a proposition P is decidable if P + (¬ P) holds. -}

classical-Prop :
  (l : Level) → UU (lsuc l)
classical-Prop l = Σ (UU-Prop l) (λ P → is-decidable (pr1 P))

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

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

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

{- 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)

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

Eq-ℕ-eq : (x y : ℕ) → Id x y → Eq-ℕ x y
Eq-ℕ-eq x .x refl = refl-Eq-ℕ x

is-injective-succ-ℕ : (x y : ℕ) → Id (succ-ℕ x) (succ-ℕ y) → Id x y
is-injective-succ-ℕ zero-ℕ zero-ℕ p = refl
is-injective-succ-ℕ zero-ℕ (succ-ℕ y) p =
  ind-empty
    { P = λ t → Id zero-ℕ (succ-ℕ y)}
    ( Eq-ℕ-eq one-ℕ (succ-ℕ (succ-ℕ y)) p)
is-injective-succ-ℕ (succ-ℕ x) zero-ℕ p =
  ind-empty
    { P = λ t → Id (succ-ℕ x) zero-ℕ}
    ( Eq-ℕ-eq (succ-ℕ (succ-ℕ x)) one-ℕ p)
is-injective-succ-ℕ (succ-ℕ x) (succ-ℕ y) p =
  ap succ-ℕ (eq-Eq-ℕ x y (Eq-ℕ-eq (succ-ℕ (succ-ℕ x)) (succ-ℕ (succ-ℕ y)) p))

has-decidable-equality-ℕ : has-decidable-equality ℕ
has-decidable-equality-ℕ zero-ℕ zero-ℕ = inl refl
has-decidable-equality-ℕ zero-ℕ (succ-ℕ y) = inr (Eq-ℕ-eq zero-ℕ (succ-ℕ y))
has-decidable-equality-ℕ (succ-ℕ x) zero-ℕ = inr (Eq-ℕ-eq (succ-ℕ x) zero-ℕ)
has-decidable-equality-ℕ (succ-ℕ x) (succ-ℕ y) =
  functor-coprod
    ( ap succ-ℕ)
    ( λ (f : ¬ (Id x y)) p → f (is-injective-succ-ℕ x y p))
    ( has-decidable-equality-ℕ x y)

{- Types with decidable equality are closed under coproducts. -}

has-decidable-equality-coprod : {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  has-decidable-equality A → has-decidable-equality B →
  has-decidable-equality (coprod A B)
has-decidable-equality-coprod dec-A dec-B (inl x) (inl y) =
  functor-coprod
    ( ap inl)
    ( λ f p → f (inv-is-equiv (is-emb-inl _ _ x y) p))
    ( dec-A x y)
has-decidable-equality-coprod {A = A} {B = B} dec-A dec-B (inl x) (inr y) =
  inr
    ( λ p →
      inv-is-equiv
        ( is-equiv-map-raise _ empty)
        ( Eq-coprod-eq A B (inl x) (inr y) p))
has-decidable-equality-coprod {A = A} {B = B} dec-A dec-B (inr x) (inl y) =
  inr
    ( λ p →
      inv-is-equiv
        ( is-equiv-map-raise _ empty)
        ( Eq-coprod-eq A B (inr x) (inl y) p))
has-decidable-equality-coprod dec-A dec-B (inr x) (inr y) =
  functor-coprod
    ( ap inr)
    ( λ f p → f (inv-is-equiv (is-emb-inr _ _ x y) p))
    ( dec-B x y)

{- Decidable equality of Fin n. -}

has-decidable-equality-empty : has-decidable-equality empty
has-decidable-equality-empty ()

has-decidable-equality-unit :
  has-decidable-equality unit
has-decidable-equality-unit star star = inl refl

has-decidable-equality-Fin :
  (n : ℕ) → has-decidable-equality (Fin n)
has-decidable-equality-Fin zero-ℕ = has-decidable-equality-empty
has-decidable-equality-Fin (succ-ℕ n) =
  has-decidable-equality-coprod
    ( has-decidable-equality-Fin n)
    ( has-decidable-equality-unit)

{- Decidable equality of ℤ. -}

has-decidable-equality-ℤ : has-decidable-equality ℤ
has-decidable-equality-ℤ =
  has-decidable-equality-coprod
    has-decidable-equality-ℕ
    ( has-decidable-equality-coprod
      has-decidable-equality-unit
      has-decidable-equality-ℕ)

{- Next, we show that types with decidable equality are sets. To see this, we
   will construct a fiberwise equivalence with the binary relation R that is
   defined by R x y := unit if (x = y), and empty otherwise. In order to define
   this relation, we first define a type family over ((x = y) + ¬(x = y)) that
   returns unit on the left and empty on the right. -}

splitting-decidable-equality : {l : Level} (A : UU l) (x y : A) →
  is-decidable (Id x y) → UU lzero
splitting-decidable-equality A x y (inl p) = unit
splitting-decidable-equality A x y (inr f) = empty

is-prop-splitting-decidable-equality : {l : Level} (A : UU l) (x y : A) →
  (t : is-decidable (Id x y)) →
  is-prop (splitting-decidable-equality A x y t)
is-prop-splitting-decidable-equality A x y (inl p) = is-prop-unit
is-prop-splitting-decidable-equality A x y (inr f) = is-prop-empty

reflexive-splitting-decidable-equality : {l : Level} (A : UU l) (x : A) →
  (t : is-decidable (Id x x)) → splitting-decidable-equality A x x t
reflexive-splitting-decidable-equality A x (inl p) = star
reflexive-splitting-decidable-equality A x (inr f) =
  ind-empty {P = λ t → splitting-decidable-equality A x x (inr f)} (f refl)

eq-splitting-decidable-equality : {l : Level} (A : UU l) (x y : A) →
  (t : is-decidable (Id x y)) →
  splitting-decidable-equality A x y t → Id x y
eq-splitting-decidable-equality A x y (inl p) t = p
eq-splitting-decidable-equality A x y (inr f) t =
  ind-empty {P = λ s → Id x y} t

is-set-has-decidable-equality : {l : Level} (A : UU l) →
  has-decidable-equality A → is-set A
is-set-has-decidable-equality A d =
  is-set-prop-in-id
    ( λ x y → splitting-decidable-equality A x y (d x y))
    ( λ x y → is-prop-splitting-decidable-equality A x y (d x y))
    ( λ x → reflexive-splitting-decidable-equality A x (d x x))
    ( λ x y → eq-splitting-decidable-equality A x y (d x y))

{- Closure of decidable types under retracts and equivalences. -}

is-decidable-retract-of :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  A retract-of B → is-decidable B → is-decidable A
is-decidable-retract-of (pair i (pair r H)) (inl b) = inl (r b)
is-decidable-retract-of (pair i (pair r H)) (inr f) = inr (f ∘ i)

is-decidable-is-equiv :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B}
  (is-equiv-f : is-equiv f) → is-decidable B → is-decidable A
is-decidable-is-equiv {f = f} (pair (pair g G) (pair h H)) =
  is-decidable-retract-of (pair f (pair h H))

is-decidable-equiv :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B) →
  is-decidable B → is-decidable A
is-decidable-equiv e = is-decidable-is-equiv (is-equiv-map-equiv e)

is-decidable-equiv' :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B) →
  is-decidable A → is-decidable B
is-decidable-equiv' e = is-decidable-equiv (inv-equiv e)

has-decidable-equality-retract-of :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  A retract-of B → has-decidable-equality B → has-decidable-equality A
has-decidable-equality-retract-of (pair i (pair r H)) d x y =
  is-decidable-retract-of
    ( Id-retract-of-Id (pair i (pair r H)) x y)
    ( d (i x) (i y))

{- The well-ordering principle. -}

is-minimal-element-ℕ :
  {l : Level} (P : ℕ → UU l) (n : ℕ) (p : P n) → UU l
is-minimal-element-ℕ P n p =
  (m : ℕ) → P m → (leq-ℕ n m)

minimal-element-ℕ :
  {l : Level} (P : ℕ → UU l) → UU l
minimal-element-ℕ P = Σ ℕ (λ n → Σ (P n) (is-minimal-element-ℕ P n))

is-minimal-element-succ-ℕ :
  {l : Level} (P : ℕ → UU l) (d : (n : ℕ) → is-decidable (P n))
  (m : ℕ) (pm : P (succ-ℕ m))
  (is-min-m : is-minimal-element-ℕ (λ x → P (succ-ℕ x)) m pm) →
  ¬ (P zero-ℕ) → is-minimal-element-ℕ P (succ-ℕ m) pm
is-minimal-element-succ-ℕ P d m pm is-min-m neg-p0 zero-ℕ p0 =
  ind-empty (neg-p0 p0)
is-minimal-element-succ-ℕ P d zero-ℕ pm is-min-m neg-p0 (succ-ℕ n) psuccn =
  leq-zero-ℕ n
is-minimal-element-succ-ℕ P d (succ-ℕ m) pm is-min-m neg-p0 (succ-ℕ n) psuccn =
  is-minimal-element-succ-ℕ (λ x → P (succ-ℕ x)) (λ x → d (succ-ℕ x)) m pm
    ( λ m → is-min-m (succ-ℕ m))
    ( is-min-m zero-ℕ)
    ( n)
    ( psuccn)

well-ordering-principle-succ-ℕ :
  {l : Level} (P : ℕ → UU l) (d : (n : ℕ) → is-decidable (P n))
  (n : ℕ) (p : P (succ-ℕ n)) →
  is-decidable (P zero-ℕ) →
  minimal-element-ℕ (λ m → P (succ-ℕ m)) → minimal-element-ℕ P
well-ordering-principle-succ-ℕ P d n p (inl p0) _ =
  pair zero-ℕ (pair p0 (λ m q → leq-zero-ℕ m))
well-ordering-principle-succ-ℕ P d n p
  (inr neg-p0) (pair m (pair pm is-min-m)) =
  pair
    ( succ-ℕ m)
    ( pair pm
      ( is-minimal-element-succ-ℕ P d m pm is-min-m neg-p0))

well-ordering-principle-ℕ :
  {l : Level} (P : ℕ → UU l) (d : (n : ℕ) → is-decidable (P n)) →
  Σ ℕ P → minimal-element-ℕ P
well-ordering-principle-ℕ P d (pair zero-ℕ p) =
  pair zero-ℕ (pair p (λ m q → leq-zero-ℕ m))
well-ordering-principle-ℕ P d (pair (succ-ℕ n) p) =
  well-ordering-principle-succ-ℕ P d n p (d zero-ℕ)
    ( well-ordering-principle-ℕ
      ( λ m → P (succ-ℕ m))
      ( λ m → d (succ-ℕ m))
      ( pair n p))

{- The Pigeon hole principle. -}

{- First we write a function that counts the number of elements in a decidable
   subset of a finite set. -}

count-Fin-succ-ℕ :
  {l : Level} (n : ℕ) (P : Fin (succ-ℕ n) → classical-Prop l) →
  ℕ → is-decidable (pr1 (pr1 (P (inr star)))) → ℕ
count-Fin-succ-ℕ n P m (inl x) = succ-ℕ m
count-Fin-succ-ℕ n P m (inr x) = m

count-Fin :
  (l : Level) (n : ℕ) (P : Fin n → classical-Prop l) → ℕ
count-Fin l zero-ℕ P = zero-ℕ
count-Fin l (succ-ℕ n) P =
  count-Fin-succ-ℕ n P
    ( count-Fin l n (P ∘ inl))
    ( pr2 (P (inr star)))

{- Next we prove the pigeonhole principle. -}

decidable-Eq-Fin :
  (n : ℕ) (i j : Fin n) → classical-Prop lzero
decidable-Eq-Fin n i j =
  pair
    ( pair (Id i j) (is-set-Fin n i j))
    ( has-decidable-equality-Fin n i j)

skip :
  (n : ℕ) → Fin (succ-ℕ n) → Fin n → Fin (succ-ℕ n)
skip (succ-ℕ n) (inl i) (inl j) = inl (skip n i j)
skip (succ-ℕ n) (inl i) (inr star) = inr star
skip (succ-ℕ n) (inr star) j = inl j

double :
  (n : ℕ) → Fin n → Fin (succ-ℕ n) → Fin n
double (succ-ℕ n) (inl i) (inl j) = inl (double n i j)
double (succ-ℕ n) (inl j) (inr star) = inr star
double (succ-ℕ n) (inr star) (inl j) = j
double (succ-ℕ n) (inr star) (inr star) = inr star

{-
skip-skip :
  (n : ℕ) (i : Fin (succ-ℕ (succ-ℕ n))) (j : Fin (succ-ℕ n)) →
    ( ( skip (succ-ℕ n) i) ∘ (skip n j)) ~
    ( ( skip (succ-ℕ n) (skip (succ-ℕ n) i j)) ∘
      ( skip n (double (succ-ℕ n) j i)))
skip-skip zero-ℕ (inl x) (inl x₁) ()
skip-skip zero-ℕ (inl x) (inr x₁) ()
skip-skip zero-ℕ (inr x) (inl x₁) ()
skip-skip zero-ℕ (inr x) (inr x₁) ()
skip-skip (succ-ℕ n) (inl i) (inl j) (inl k) = {!!}
skip-skip (succ-ℕ n) (inl x) (inl x₁) (inr x₂) = {!!}
skip-skip (succ-ℕ n) (inl x) (inr x₁) (inl x₂) = {!!}
skip-skip (succ-ℕ n) (inl x) (inr x₁) (inr x₂) = {!!}
skip-skip (succ-ℕ n) (inr x) (inl x₁) (inl x₂) = {!!}
skip-skip (succ-ℕ n) (inr x) (inl x₁) (inr x₂) = {!!}
skip-skip (succ-ℕ n) (inr x) (inr x₁) (inl x₂) = {!!}
skip-skip (succ-ℕ n) (inr x) (inr x₁) (inr x₂) = {!!}
-}

{-
pigeonhole-principle :
  (m n : ℕ) (f : Fin n → Fin m) (H : le-ℕ m n) →
  Σ ( Fin m) (λ i →
    le-ℕ one-ℕ
      ( count-Fin lzero n
        ( λ j → decidable-Eq-Fin m (f j) i)))
pigeonhole-principle zero-ℕ (succ-ℕ n) f H = {!!}
pigeonhole-principle (succ-ℕ m) n f H = {!!}
-}

-- The greatest common divisor

{- First we show that mul-ℕ n is an embedding whenever n > 0. In order to do
   this, we have to show that add-ℕ n is injective. -}

is-injective-add-ℕ :
  (n : ℕ) → is-injective is-set-ℕ is-set-ℕ (add-ℕ n)
is-injective-add-ℕ zero-ℕ k l p = p
is-injective-add-ℕ (succ-ℕ n) k l p =
  is-injective-add-ℕ n k l (is-injective-succ-ℕ (add-ℕ n k) (add-ℕ n l) p)

is-emb-add-ℕ :
  (n : ℕ) → is-emb (add-ℕ n)
is-emb-add-ℕ n =
  is-emb-is-injective is-set-ℕ is-set-ℕ (add-ℕ n) (is-injective-add-ℕ n)

leq-fib-add-ℕ :
  (m n : ℕ) → fib (add-ℕ m) n → (leq-ℕ m n)
leq-fib-add-ℕ zero-ℕ n (pair k p) = leq-zero-ℕ n
leq-fib-add-ℕ (succ-ℕ m) (succ-ℕ n) (pair k p) =
  leq-fib-add-ℕ m n (pair k (is-injective-succ-ℕ (add-ℕ m k) n p))

fib-add-leq-ℕ :
  (m n : ℕ) → (leq-ℕ m n) → fib (add-ℕ m) n
fib-add-leq-ℕ zero-ℕ zero-ℕ H = pair zero-ℕ refl
fib-add-leq-ℕ zero-ℕ (succ-ℕ n) H = pair (succ-ℕ n) refl
fib-add-leq-ℕ (succ-ℕ m) (succ-ℕ n) H =
  pair
    ( pr1 (fib-add-leq-ℕ m n H))
    ( ap succ-ℕ (pr2 (fib-add-leq-ℕ m n H)))

is-prop-leq-ℕ :
  (m n : ℕ) → is-prop (leq-ℕ m n)
is-prop-leq-ℕ zero-ℕ zero-ℕ = is-prop-unit
is-prop-leq-ℕ zero-ℕ (succ-ℕ n) = is-prop-unit
is-prop-leq-ℕ (succ-ℕ m) zero-ℕ = is-prop-empty
is-prop-leq-ℕ (succ-ℕ m) (succ-ℕ n) = is-prop-leq-ℕ m n

is-equiv-leq-fib-add-ℕ :
  (m n : ℕ) → is-equiv (leq-fib-add-ℕ m n)
is-equiv-leq-fib-add-ℕ m n =
  is-equiv-is-prop
    ( is-prop-map-is-emb _ (is-emb-add-ℕ m) n)
    ( is-prop-leq-ℕ m n)
    ( fib-add-leq-ℕ m n)

is-equiv-fib-add-leq-ℕ :
  (m n : ℕ) → is-equiv (fib-add-leq-ℕ m n)
is-equiv-fib-add-leq-ℕ m n =
  is-equiv-is-prop
    ( is-prop-leq-ℕ m n)
    ( is-prop-map-is-emb _ (is-emb-add-ℕ m) n)
    ( leq-fib-add-ℕ m n)

is-injective-add-ℕ' :
  (n : ℕ) → is-injective is-set-ℕ is-set-ℕ (λ m → add-ℕ m n)
is-injective-add-ℕ' n k l p =
  is-injective-add-ℕ n k l
    (((commutative-add-ℕ n k) ∙ p) ∙ (commutative-add-ℕ l n))

is-injective-mul-ℕ :
  (n : ℕ) → (le-ℕ zero-ℕ n) → is-injective is-set-ℕ is-set-ℕ (mul-ℕ n)
is-injective-mul-ℕ (succ-ℕ n) star zero-ℕ zero-ℕ p = refl
is-injective-mul-ℕ (succ-ℕ n) star zero-ℕ (succ-ℕ l) p =
  ind-empty
    ( Eq-ℕ-eq
      ( zero-ℕ)
      ( succ-ℕ (add-ℕ (mul-ℕ n (succ-ℕ l)) l))
      ( ( inv (right-zero-law-mul-ℕ n)) ∙
        ( ( inv (right-unit-law-add-ℕ (mul-ℕ n zero-ℕ))) ∙
          ( p ∙ (right-successor-law-add-ℕ (mul-ℕ n (succ-ℕ l)) l)))))
is-injective-mul-ℕ (succ-ℕ n) star (succ-ℕ k) zero-ℕ p =
  ind-empty
    ( Eq-ℕ-eq
      ( succ-ℕ (add-ℕ (mul-ℕ n (succ-ℕ k)) k))
      ( zero-ℕ)
      ( ( inv (right-successor-law-add-ℕ (mul-ℕ n (succ-ℕ k)) k)) ∙
        ( p ∙ ( right-zero-law-mul-ℕ (succ-ℕ n)))))
is-injective-mul-ℕ (succ-ℕ n) star (succ-ℕ k) (succ-ℕ l) p =
  ap succ-ℕ
    ( is-injective-mul-ℕ (succ-ℕ n) star k l
      ( is-injective-add-ℕ (succ-ℕ n)
        ( mul-ℕ (succ-ℕ n) k)
        ( mul-ℕ (succ-ℕ n) l)
        ( ( inv (right-successor-law-mul-ℕ (succ-ℕ n) k) ∙ p) ∙
          ( right-successor-law-mul-ℕ (succ-ℕ n) l))))

is-emb-mul-ℕ :
  (n : ℕ) → (le-ℕ zero-ℕ n) → is-emb (mul-ℕ n)
is-emb-mul-ℕ n le =
  is-emb-is-injective is-set-ℕ is-set-ℕ
    ( mul-ℕ n)
    ( is-injective-mul-ℕ n le)

is-emb-mul-ℕ' :
  (n : ℕ) → (le-ℕ zero-ℕ n) → is-emb (λ m → mul-ℕ m n)
is-emb-mul-ℕ' n t =
  is-emb-htpy'
    ( mul-ℕ n)
    ( λ m → mul-ℕ m n)
    ( commutative-mul-ℕ n)
    ( is-emb-mul-ℕ n t)

{- We conclude that the division relation is a property. -}

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

is-prop-div-ℕ :
  (m n : ℕ) → (le-ℕ zero-ℕ m) → is-prop (div-ℕ m n)
is-prop-div-ℕ (succ-ℕ m) n star =
  is-prop-map-is-emb
    ( λ z → mul-ℕ z (succ-ℕ m))
    ( is-emb-mul-ℕ' (succ-ℕ m) star)
    n

{- We now construct the division with remainder. -}

le-mul-ℕ :
  (d n k : ℕ) → UU lzero
le-mul-ℕ d n k = le-ℕ n (mul-ℕ k d)

is-decidable-le-mul-ℕ :
  (d n k : ℕ) → is-decidable (le-mul-ℕ d n k)
is-decidable-le-mul-ℕ d n k =
  is-decidable-le-ℕ n (mul-ℕ k d)

order-preserving-succ-ℕ :
  (n n' : ℕ) → (leq-ℕ n n') → (leq-ℕ (succ-ℕ n) (succ-ℕ n'))
order-preserving-succ-ℕ n n' H = H

leq-eq-left-ℕ :
  {m m' : ℕ} → Id m m' → (n : ℕ) → leq-ℕ m n → leq-ℕ m' n
leq-eq-left-ℕ refl n = id

leq-eq-right-ℕ :
  (m : ℕ) {n n' : ℕ} → Id n n' → leq-ℕ m n → leq-ℕ m n'
leq-eq-right-ℕ m refl = id

order-preserving-add-ℕ :
  (m n m' n' : ℕ) →
  (leq-ℕ m m') → (leq-ℕ n n') → (leq-ℕ (add-ℕ m n) (add-ℕ m' n'))
order-preserving-add-ℕ zero-ℕ zero-ℕ m' n' Hm Hn = star
order-preserving-add-ℕ zero-ℕ (succ-ℕ n) zero-ℕ (succ-ℕ n') Hm Hn = Hn
order-preserving-add-ℕ zero-ℕ (succ-ℕ n) (succ-ℕ m') (succ-ℕ n') Hm Hn =
  leq-eq-right-ℕ n
    ( inv (right-successor-law-add-ℕ m' n'))
    ( order-preserving-add-ℕ zero-ℕ n (succ-ℕ m') n' Hm Hn)
order-preserving-add-ℕ (succ-ℕ m) n (succ-ℕ m') n' Hm Hn =
  order-preserving-add-ℕ m n m' n' Hm Hn

le-eq-right-ℕ :
  (m : ℕ) {n n' : ℕ} → Id n n' → le-ℕ m n' → le-ℕ m n
le-eq-right-ℕ m refl = id

le-add-ℕ :
  (m n : ℕ) → (leq-ℕ one-ℕ n) → le-ℕ m (add-ℕ m n)
le-add-ℕ zero-ℕ (succ-ℕ n) star = star
le-add-ℕ (succ-ℕ m) (succ-ℕ n) star = le-add-ℕ m (succ-ℕ n) star

le-mul-self-ℕ :
  (d n : ℕ) → (leq-ℕ one-ℕ d) → (leq-ℕ one-ℕ n) → le-mul-ℕ d n n
le-mul-self-ℕ (succ-ℕ d) (succ-ℕ n) star star =
  le-eq-right-ℕ
    ( succ-ℕ n)
    ( right-successor-law-mul-ℕ (succ-ℕ n) d)
    ( le-add-ℕ (succ-ℕ n) (mul-ℕ (succ-ℕ n) d) {!leq-eq-right-ℕ !})

leq-multiple-ℕ :
  (n m : ℕ) → (leq-ℕ one-ℕ m) → leq-ℕ n (mul-ℕ n m)
leq-multiple-ℕ n (succ-ℕ m) H =
  leq-eq-right-ℕ n
    ( inv (right-successor-law-mul-ℕ n m))
    ( leq-fib-add-ℕ n (add-ℕ n (mul-ℕ n m)) (pair (mul-ℕ n m) refl))

least-factor-least-larger-multiple-ℕ :
  (d n : ℕ) → (leq-ℕ one-ℕ d) →
  minimal-element-ℕ (λ k → leq-ℕ n (mul-ℕ k d))
least-factor-least-larger-multiple-ℕ d n H =
  well-ordering-principle-ℕ
    ( λ k → leq-ℕ n (mul-ℕ k d))
    ( λ k → is-decidable-leq-ℕ n (mul-ℕ k d))
    ( pair n (leq-multiple-ℕ n d H))

factor-least-larger-multiple-ℕ :
  (d n : ℕ) → (leq-ℕ one-ℕ d) → ℕ
factor-least-larger-multiple-ℕ d n H =
  pr1 (least-factor-least-larger-multiple-ℕ d n H)

least-larger-multiple-ℕ :
  (d n : ℕ) → (leq-ℕ one-ℕ d) → ℕ
least-larger-multiple-ℕ d n H =
  mul-ℕ (factor-least-larger-multiple-ℕ d n H) d

leq-least-larger-multiple-ℕ :
  (d n : ℕ) (H : leq-ℕ one-ℕ d) →
  leq-ℕ n (least-larger-multiple-ℕ d n H)
leq-least-larger-multiple-ℕ d n H =
  pr1 (pr2 (least-factor-least-larger-multiple-ℕ d n H))

is-minimal-least-larger-multiple-ℕ :
  (d n : ℕ) (H : leq-ℕ one-ℕ d) (k : ℕ) (K : leq-ℕ n (mul-ℕ k d)) →
  leq-ℕ (factor-least-larger-multiple-ℕ d n H) k
is-minimal-least-larger-multiple-ℕ d n H =
  pr2 (pr2 (least-factor-least-larger-multiple-ℕ d n H))

is-decidable-div-is-decidable-eq-least-larger-multiple-ℕ :
  (d n : ℕ) (H : leq-ℕ one-ℕ d) →
  is-decidable (Id (least-larger-multiple-ℕ d n H) n) → is-decidable (div-ℕ d n)
is-decidable-div-is-decidable-eq-least-larger-multiple-ℕ d n H (inl p) =
  inl (pair (factor-least-larger-multiple-ℕ d n H) p)
is-decidable-div-is-decidable-eq-least-larger-multiple-ℕ d n H (inr f) =
  inr (λ x → {!!})

is-decidable-div-ℕ' :
  (d n : ℕ) → (leq-ℕ one-ℕ d) → is-decidable (div-ℕ d n)
is-decidable-div-ℕ' d n H = {!!}

is-decidable-div-ℕ :
  (d n : ℕ) → is-decidable (div-ℕ d n)
is-decidable-div-ℕ zero-ℕ zero-ℕ = inl (pair zero-ℕ refl)
is-decidable-div-ℕ zero-ℕ (succ-ℕ n) =
  inr ( λ p →
    Eq-ℕ-eq zero-ℕ (succ-ℕ n) ((inv (right-zero-law-mul-ℕ (pr1 p))) ∙ (pr2 p)))
is-decidable-div-ℕ (succ-ℕ d) n =
  is-decidable-div-ℕ' (succ-ℕ d) n (leq-zero-ℕ d)

-- Operations on decidable bounded subsets of ℕ

iterated-operation-ℕ :
  (strict-upper-bound : ℕ) (operation : ℕ → ℕ → ℕ) (base-value : ℕ) → ℕ
iterated-operation-ℕ zero-ℕ μ e = e
iterated-operation-ℕ (succ-ℕ b) μ e = μ (iterated-operation-ℕ b μ e) b

iterated-sum-ℕ :
  (summand : ℕ → ℕ) (b : ℕ) → ℕ
iterated-sum-ℕ f zero-ℕ = zero-ℕ
iterated-sum-ℕ f (succ-ℕ b) = add-ℕ (iterated-sum-ℕ f b) (f (succ-ℕ b))

ranged-sum-ℕ :
  (summand : ℕ → ℕ) (l u : ℕ) → ℕ
ranged-sum-ℕ f zero-ℕ u = iterated-sum-ℕ f u
ranged-sum-ℕ f (succ-ℕ l) zero-ℕ = zero-ℕ
ranged-sum-ℕ f (succ-ℕ l) (succ-ℕ u) =
  ranged-sum-ℕ (f ∘ succ-ℕ) l u

succ-iterated-operation-fam-ℕ :
  { l : Level}
  ( P : ℕ → UU l) (is-decidable-P : (n : ℕ) → is-decidable (P n)) →
  ( predecessor-strict-upper-bound : ℕ) (operation : ℕ → ℕ → ℕ) →
  is-decidable (P predecessor-strict-upper-bound) → ℕ → ℕ
succ-iterated-operation-fam-ℕ
  P is-decidable-P b μ (inl p) m = μ m b
succ-iterated-operation-fam-ℕ
  P is-decidable-P b μ (inr f) m = m

iterated-operation-fam-ℕ :
  { l : Level} (P : ℕ → UU l) (is-decidable-P : (n : ℕ) → is-decidable (P n)) →
  ( strict-upper-bound : ℕ) (operation : ℕ → ℕ → ℕ) (base-value : ℕ) → ℕ
iterated-operation-fam-ℕ P d zero-ℕ μ e = e
iterated-operation-fam-ℕ P d (succ-ℕ b) μ e =
  succ-iterated-operation-fam-ℕ P d b μ (d b)
    ( iterated-operation-fam-ℕ P d b μ e)

Sum-fam-ℕ :
  { l : Level} (P : ℕ → UU l) (is-decidable-P : (n : ℕ) → is-decidable (P n)) →
  ( upper-bound : ℕ) ( summand : ℕ → ℕ) → ℕ
Sum-fam-ℕ P d b f = iterated-operation-fam-ℕ P d (succ-ℕ b) (λ x y → add-ℕ x (f y)) zero-ℕ

{-
iterated-operation-fam-ℕ
  P is-decidable-P zero-ℕ is-bounded-P μ base-value =
  base-value
iterated-operation-fam-ℕ
  P is-decidable-P (succ-ℕ b) is-bounded-P μ base-value =
  succ-iterated-operation-ℕ P is-decidable-P b is-bounded-P μ
    ( is-decidable-P b)
    ( iterated-operation-ℕ
      ( introduce-bound-on-fam-ℕ b P)
      ( is-decidable-introduce-bound-on-fam-ℕ b P is-decidable-P)
      ( b)
      ( is-bounded-introduce-bound-on-fam-ℕ b P)
      ( μ)
      ( base-value))

product-decidable-bounded-fam-ℕ :
  { l : Level} (P : ℕ → UU l) →
  ( is-decidable-P : (n : ℕ) → is-decidable (P n))
  ( b : ℕ) ( is-bounded-P : is-bounded-fam-ℕ b P) → ℕ
product-decidable-bounded-fam-ℕ P is-decidable-P b is-bounded-P =
  iterated-operation-ℕ P is-decidable-P b is-bounded-P mul-ℕ one-ℕ

twenty-four-ℕ : ℕ
twenty-four-ℕ =
  product-decidable-bounded-fam-ℕ
    ( λ x → le-ℕ x five-ℕ)
    ( λ x → is-decidable-le-ℕ x five-ℕ)
    ( five-ℕ)
    ( λ x → id)
-}

{-
test-zero-twenty-four-ℕ : Id twenty-four-ℕ zero-ℕ
test-zero-twenty-four-ℕ = refl

test-twenty-four-ℕ : Id twenty-four-ℕ (factorial four-ℕ)
test-twenty-four-ℕ = refl
-}

-- Exercises

-- Exercise 10.?

Eq-𝟚-eq : (x y : bool) → Id x y → Eq-𝟚 x y
Eq-𝟚-eq x .x refl = reflexive-Eq-𝟚 x

abstract
  has-decidable-equality-𝟚 : has-decidable-equality bool
  has-decidable-equality-𝟚 true true = inl refl
  has-decidable-equality-𝟚 true false = inr (Eq-𝟚-eq true false)
  has-decidable-equality-𝟚 false true = inr (Eq-𝟚-eq false true)
  has-decidable-equality-𝟚 false false = inl refl

-- Exercise 10.?

abstract
  has-decidable-equality-prod' : {l1 l2 : Level} {A : UU l1} {B : UU l2} →
    (x x' : A) (y y' : B) → is-decidable (Id x x') → is-decidable (Id y y') →
    is-decidable (Id (pair x y) (pair x' y'))
  has-decidable-equality-prod' x x' y y' (inl p) (inl q) =
    inl (eq-pair-triv (pair p q))
  has-decidable-equality-prod' x x' y y' (inl p) (inr g) =
    inr (λ h → g (ap pr2 h))
  has-decidable-equality-prod' x x' y y' (inr f) (inl q) =
    inr (λ h → f (ap pr1 h))
  has-decidable-equality-prod' x x' y y' (inr f) (inr g) =
    inr (λ h → f (ap pr1 h))

abstract
  has-decidable-equality-prod : {l1 l2 : Level} {A : UU l1} {B : UU l2} →
    has-decidable-equality A → has-decidable-equality B →
    has-decidable-equality (A × B)
  has-decidable-equality-prod dec-A dec-B (pair x y) (pair x' y') =
    has-decidable-equality-prod' x x' y y' (dec-A x x') (dec-B y y')

{-

bounds-fam-ℕ :
  {l : Level} (P : ℕ → UU l) → UU l
bounds-fam-ℕ P = Σ ℕ (λ n → is-bounded-fam-ℕ n P)

is-minimal-ℕ :
  {l : Level} (P : ℕ → UU l) → Σ ℕ P → UU l
is-minimal-ℕ P (pair n p) = (t : Σ ℕ P) → leq-ℕ n (pr1 t)

eq-zero-leq-zero-ℕ :
  (n : ℕ) → leq-ℕ n zero-ℕ → Id n zero-ℕ
eq-zero-leq-zero-ℕ zero-ℕ star = refl
eq-zero-leq-zero-ℕ (succ-ℕ n) ()

fam-succ-ℕ :
  {l : Level} → (ℕ → UU l) → (ℕ → UU l)
fam-succ-ℕ P n = P (succ-ℕ n)

is-decidable-fam-succ-ℕ :
  {l : Level} (P : ℕ → UU l) →
  ((n : ℕ) → is-decidable (P n)) → ((n : ℕ) → is-decidable (P (succ-ℕ n)))
is-decidable-fam-succ-ℕ P d n = d (succ-ℕ n)

min-is-bounded-not-zero-ℕ :
  {l : Level} (P : ℕ → UU l) → ((n : ℕ) → is-decidable (P n)) →
  Σ ℕ (λ n → is-bounded-fam-ℕ n P) →
  ¬ (P zero-ℕ) →
  Σ (Σ ℕ (fam-succ-ℕ P)) (is-minimal-ℕ (fam-succ-ℕ P)) →
  Σ (Σ ℕ P) (is-minimal-ℕ P)
min-is-bounded-not-zero-ℕ P d b np0 t = {!!}

min-is-bounded-ℕ :
  {l : Level} (P : ℕ → UU l) → ((n : ℕ) → is-decidable (P n)) →
  Σ ℕ (λ n → is-bounded-fam-ℕ n P) →
  Σ ℕ P → Σ (Σ ℕ P) (is-minimal-ℕ P)
min-is-bounded-ℕ P d (pair zero-ℕ b) t =
  pair
    ( pair
      ( zero-ℕ)
      ( tr P (eq-zero-leq-zero-ℕ (pr1 t) (b (pr1 t) (pr2 t))) (pr2 t)))
    ( λ p → leq-zero-ℕ (pr1 p))
min-is-bounded-ℕ P d (pair (succ-ℕ n) b) t =
  ind-coprod
    ( λ (t : is-decidable (P zero-ℕ)) → Σ (Σ ℕ P) (is-minimal-ℕ P))
    ( λ p0 → pair (pair zero-ℕ p0) (λ p → leq-zero-ℕ (pr1 p)))
    ( λ y → min-is-bounded-not-zero-ℕ P d (pair (succ-ℕ n) b) y
      ( min-is-bounded-ℕ
        ( fam-succ-ℕ P)
        ( is-decidable-fam-succ-ℕ P d)
        {!!}
        {!!}))
    ( d zero-ℕ)

{- We show that every non-empty decidable subset of ℕ has a least element. -}

least-ℕ :
  {l : Level} (P : ℕ → UU l) → Σ ℕ P → UU l
least-ℕ P (pair n p) = (m : ℕ) → P m → leq-ℕ n m

least-element-non-empty-decidable-subset-ℕ :
  {l : Level} (P : ℕ → UU l) (d : (n : ℕ) → is-decidable (P n)) →
  Σ ℕ P → Σ (Σ ℕ P) (least-ℕ P)
least-element-non-empty-decidable-subset-ℕ P d (pair zero-ℕ p) =
  pair (pair zero-ℕ p) {!!}
least-element-non-empty-decidable-subset-ℕ P d (pair (succ-ℕ n) p) = {!!}
-}

zero-Fin :
  (n : ℕ) → Fin (succ-ℕ n)
zero-Fin zero-ℕ = inr star
zero-Fin (succ-ℕ n) = inl (zero-Fin n)

succ-Fin :
  (n : ℕ) → Fin n → Fin n
succ-Fin (succ-ℕ n) (inr star) = zero-Fin n
succ-Fin (succ-ℕ (succ-ℕ n)) (inl (inl x)) = inl (succ-Fin (succ-ℕ n) (inl x))
succ-Fin (succ-ℕ (succ-ℕ n)) (inl (inr star)) = inr star

iterated-succ-Fin :
  (k : ℕ) → (n : ℕ) → Fin n → Fin n
iterated-succ-Fin zero-ℕ n = id
iterated-succ-Fin (succ-ℕ k) n = (succ-Fin n) ∘ (iterated-succ-Fin k n)

quotient-ℕ-Fin :
  (n : ℕ) → Fin (succ-ℕ n)
quotient-ℕ-Fin n = iterated-succ-Fin n (succ-ℕ n) (zero-Fin n)

pred-Fin :
  (n : ℕ) → Fin n → Fin n
pred-Fin (succ-ℕ zero-ℕ) (inr star) = inr star
pred-Fin (succ-ℕ (succ-ℕ n)) (inl x) = {!!}
pred-Fin (succ-ℕ (succ-ℕ n)) (inr star) = inl (inr star)

add-Fin :
  (n : ℕ) → Fin n → Fin n → Fin n
add-Fin (succ-ℕ n) (inl x) j = {!!}
add-Fin (succ-ℕ n) (inr x) j = {!!}

idempotent-succ-Fin :
  (n : ℕ) (i : Fin n) → Id (iterated-succ-Fin n n i) i
idempotent-succ-Fin (succ-ℕ zero-ℕ) (inr star) = refl
idempotent-succ-Fin (succ-ℕ (succ-ℕ n)) (inl x) = {!!}
idempotent-succ-Fin (succ-ℕ (succ-ℕ n)) (inr x) = {!!}

in-nat-ℤ : ℕ → ℤ
in-nat-ℤ zero-ℕ = zero-ℤ
in-nat-ℤ (succ-ℕ n) = in-pos n

div-ℤ :
  (k l : ℤ) → UU lzero
div-ℤ k l = Σ ℤ (λ x → Id (mul-ℤ x k) l)

_≡_mod_ :
  (k l : ℤ) (n : ℕ) → UU lzero
k ≡ l mod n = div-ℤ (in-nat-ℤ n) (add-ℤ k (neg-ℤ l))

-- From before

is-even-ℕ : ℕ → UU lzero
is-even-ℕ n = div-ℕ two-ℕ n

is-prime : ℕ → UU lzero
is-prime n = (one-ℕ < n) × ((m : ℕ) → (one-ℕ < m) → (div-ℕ m n) → Id m n)

{- The Goldbach conjecture asserts that every even number above 2 is the sum
   of two primes. -}

Goldbach-conjecture : UU lzero
Goldbach-conjecture =
  ( n : ℕ) → (two-ℕ < n) → (is-even-ℕ n) →
    Σ ℕ (λ p → (is-prime p) × (Σ ℕ (λ q → (is-prime q) × Id (add-ℕ p q) n)))

is-twin-prime : ℕ → UU lzero
is-twin-prime n = (is-prime n) × (is-prime (succ-ℕ (succ-ℕ n)))

{- The twin prime conjecture asserts that there are infinitely many twin
   primes. We assert that there are infinitely twin primes by asserting that
   for every n : ℕ there is a twin prime that is larger than n. -}

Twin-prime-conjecture : UU lzero
Twin-prime-conjecture = (n : ℕ) → Σ ℕ (λ p → (is-twin-prime p) × (leq-ℕ n p))

max_stars_repo_name: tadejpetric/HoTT-Intro

max_issues_repo_name: tadejpetric/HoTT-Intro

max_forks_repo_name: tadejpetric/HoTT-Intro


text:
-- We apply the theory of quasi equivalence relations (QERs) to finite multisets and association lists.
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Relation.ZigZag.Applications.MultiSet where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.RelationalStructure
open import Cubical.Foundations.Structure
open import Cubical.Foundations.SIP
open import Cubical.Foundations.Univalence
open import Cubical.Data.Unit
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Nat
open import Cubical.Data.List hiding ([_])
open import Cubical.Data.Sigma
open import Cubical.HITs.SetQuotients
open import Cubical.HITs.FiniteMultiset as FMS hiding ([_] ; _++_)
open import Cubical.HITs.FiniteMultiset.CountExtensionality
open import Cubical.HITs.PropositionalTruncation
open import Cubical.Relation.Nullary
open import Cubical.Relation.ZigZag.Base

open import Cubical.Structures.MultiSet
open import Cubical.Structures.Relational.Auto
open import Cubical.Structures.Relational.Macro

-- we define simple association lists without any higher constructors
data AList {ℓ} (A : Type ℓ) : Type ℓ where
  ⟨⟩ : AList A
  ⟨_,_⟩∷_ : A → ℕ → AList A → AList A

infixr 5 ⟨_,_⟩∷_

private
  variable
    ℓ : Level

-- We have a CountStructure on List and AList and use these to get a QER between the two
module Lists&ALists {A : Type ℓ} (discA : Discrete A) where

  multisetShape : Type ℓ → Type ℓ
  multisetShape X = X × (A → X → X) × (X → X → X) × (A → X → Const[ ℕ , isSetℕ ])

  module S = RelMacro ℓ (autoRelDesc multisetShape)

  addIfEq : (a x : A) → ℕ → ℕ → ℕ
  addIfEq a x m n with discA a x
  ... | yes _ = m + n
  ... | no _ = n

  module _ {a x : A} {n : ℕ} where

    addIfEq≡ : {m : ℕ} → a ≡ x → addIfEq a x m n ≡ m + n
    addIfEq≡ a≡x with discA a x
    ... | yes _ = refl
    ... | no a≢x = ⊥.rec (a≢x a≡x)

    addIfEq≢ : {m : ℕ} → ¬ (a ≡ x) → addIfEq a x m n ≡ n
    addIfEq≢ a≢x with discA a x
    ... | yes a≡x = ⊥.rec (a≢x a≡x)
    ... | no _ = refl

    addIfEq0 : addIfEq a x 0 n ≡ n
    addIfEq0 with discA a x
    ... | yes _ = refl
    ... | no _ = refl

    addIfEq+ : {m : ℕ} (n' : ℕ) → addIfEq a x m (n + n') ≡ addIfEq a x m n + n'
    addIfEq+ n' with discA a x
    ... | yes _ = +-assoc _ n n'
    ... | no _ = refl

  module L where
    emp : List A
    emp = []

    insert : A → List A → List A
    insert x xs = x ∷ xs

    union : List A → List A → List A
    union xs ys = xs ++ ys

    count : A → List A → ℕ
    count a [] = zero
    count a (x ∷ xs) = addIfEq a x 1 (count a xs)

    structure : S.structure (List A)
    structure = emp , insert , union , count

    countUnion : ∀ a xs ys → count a (union xs ys) ≡ count a xs + count a ys
    countUnion a [] ys = refl
    countUnion a (x ∷ xs) ys =
      cong (addIfEq a x 1) (countUnion a xs ys)
      ∙ addIfEq+ (count a ys)

  module AL where
    emp : AList A
    emp = ⟨⟩

    insert* : ℕ → A → AList A → AList A
    insert* m a ⟨⟩ = ⟨ a , m ⟩∷ ⟨⟩
    insert* m a (⟨ y , n ⟩∷ ys) with (discA a y)
    ... | yes _ = ⟨ y , m + n ⟩∷ ys
    ... | no _ = ⟨ y , n ⟩∷ insert* m a ys

    insert : A → AList A → AList A
    insert = insert* 1

    union : AList A → AList A → AList A
    union ⟨⟩ ys = ys
    union (⟨ x , n ⟩∷ xs) ys = insert* n x (union xs ys)

    count : A → AList A → ℕ
    count a ⟨⟩ = zero
    count a (⟨ y , n ⟩∷ ys) = addIfEq a y n (count a ys)

    structure : S.structure (AList A)
    structure = emp , insert , union , count

    countInsert* : ∀ m a x ys → count a (insert* m x ys) ≡ addIfEq a x m (count a ys)
    countInsert* m a x ⟨⟩ = refl
    countInsert* m a x (⟨ y , n ⟩∷ ys) with discA a x | discA a y | discA x y
    ... | yes a≡x | yes a≡y | yes x≡y = addIfEq≡ a≡y ∙ sym (+-assoc m n _)
    ... | yes a≡x | yes a≡y | no x≢y = ⊥.rec (x≢y (sym a≡x ∙ a≡y))
    ... | yes a≡x | no a≢y | yes x≡y = ⊥.rec (a≢y (a≡x ∙ x≡y))
    ... | yes a≡x | no a≢y | no x≢y =  addIfEq≢ a≢y ∙ countInsert* m a x ys ∙ addIfEq≡ a≡x
    ... | no a≢x | yes a≡y | yes x≡y = ⊥.rec (a≢x (a≡y ∙ sym x≡y))
    ... | no a≢x | yes a≡y | no x≢y = addIfEq≡ a≡y ∙ cong (n +_) (countInsert* m a x ys ∙ addIfEq≢ a≢x)
    ... | no a≢x | no a≢y | yes x≡y = addIfEq≢ a≢y
    ... | no a≢x | no a≢y | no x≢y = addIfEq≢ a≢y ∙ countInsert* m a x ys ∙ addIfEq≢ a≢x

    countInsert = countInsert* 1

    countUnion : ∀ a xs ys → count a (union xs ys) ≡ count a xs + count a ys
    countUnion a ⟨⟩ ys = refl
    countUnion a (⟨ x , n ⟩∷ xs) ys =
      countInsert* n a x (union xs ys)
      ∙ cong (addIfEq a x n) (countUnion a xs ys)
      ∙ addIfEq+ (count a ys)

  -- now for the QER between List and Alist

  R : List A → AList A → Type ℓ
  R xs ys = ∀ a → L.count a xs ≡ AL.count a ys

  φ : List A → AList A
  φ [] = ⟨⟩
  φ (x ∷ xs) = AL.insert x (φ xs)

  ψ : AList A → List A
  ψ ⟨⟩ = []
  ψ (⟨ x , zero ⟩∷ xs) = ψ xs
  ψ (⟨ x , suc n ⟩∷ xs) = x ∷ ψ (⟨ x , n ⟩∷ xs)

  η : ∀ xs → R xs (φ xs)
  η [] a = refl
  η (x ∷ xs) a = cong (addIfEq a x 1) (η xs a) ∙ sym (AL.countInsert a x (φ xs))

  -- for the other direction we need a little helper function
  ε : ∀ y → R (ψ y) y
  ε' : (x : A) (n : ℕ) (xs : AList A) (a : A)
    → L.count a (ψ (⟨ x , n ⟩∷ xs)) ≡ AL.count a (⟨ x , n ⟩∷ xs)

  ε ⟨⟩ a = refl
  ε (⟨ x , n ⟩∷ xs) a = ε' x n xs a

  ε' x zero xs a = ε xs a ∙ sym addIfEq0
  ε' x (suc n) xs a with discA a x
  ... | yes a≡x = cong suc (ε' x n xs a ∙ addIfEq≡ a≡x)
  ... | no  a≢x = ε' x n xs a ∙ addIfEq≢ a≢x

  -- Induced quotients and equivalence

  open isQuasiEquivRel

  -- R is a QER
  QuasiR : QuasiEquivRel _ _ ℓ
  QuasiR .fst .fst = R
  QuasiR .fst .snd _ _ = isPropΠ λ _ → isSetℕ _ _
  QuasiR .snd .zigzag r r' r'' a = (r a) ∙∙ sym (r' a) ∙∙ (r'' a)
  QuasiR .snd .fwd a = ∣ φ a , η a ∣
  QuasiR .snd .bwd b = ∣ ψ b , ε b ∣

  isStructuredInsert : (x : A) {xs : List A} {ys : AList A}
    → R xs ys → R (L.insert x xs) (AL.insert x ys)
  isStructuredInsert x {xs} {ys} r a =
    cong (addIfEq a x 1) (r a) ∙ sym (AL.countInsert a x ys)

  isStructuredUnion :
    {xs : List A} {ys : AList A} (r : R xs ys)
    {xs' : List A} {ys' : AList A} (r' : R xs' ys')
    → R (L.union xs xs') (AL.union ys ys')
  isStructuredUnion {xs} {ys} r {xs'} {ys'} r' a =
    L.countUnion a xs xs' ∙ cong₂ _+_ (r a) (r' a) ∙ sym (AL.countUnion a ys ys')

  -- R is structured
  isStructuredR : S.relation R L.structure AL.structure
  isStructuredR .fst a = refl
  isStructuredR .snd .fst = isStructuredInsert
  isStructuredR .snd .snd .fst {xs} {ys} = isStructuredUnion {xs} {ys}
  isStructuredR .snd .snd .snd a r = r a

  module E = QER→Equiv QuasiR
  open E renaming (Rᴸ to Rᴸ; Rᴿ to Rᴬᴸ)

  List/Rᴸ = (List A) / Rᴸ
  AList/Rᴬᴸ = (AList A) / Rᴬᴸ

  List/Rᴸ≃AList/Rᴬᴸ : List/Rᴸ ≃ AList/Rᴬᴸ
  List/Rᴸ≃AList/Rᴬᴸ = E.Thm

  main : QERDescends _ S.relation (List A , L.structure) (AList A , AL.structure) QuasiR
  main = structuredQER→structuredEquiv S.suitable _ _ QuasiR isStructuredR

  open QERDescends

  LQstructure : S.structure List/Rᴸ
  LQstructure = main .quoᴸ .fst

  ALQstructure : S.structure AList/Rᴬᴸ
  ALQstructure = main .quoᴿ .fst

  -- We get a path between structure over the equivalence from the fact that the QER is structured
  List/Rᴸ≡AList/Rᴬᴸ :
    Path (TypeWithStr ℓ S.structure) (List/Rᴸ , LQstructure) (AList/Rᴬᴸ , ALQstructure)
  List/Rᴸ≡AList/Rᴬᴸ =
    sip S.univalent _ _
      (E.Thm , S.matches (List/Rᴸ , LQstructure) (AList/Rᴬᴸ , ALQstructure) E.Thm .fst (main .rel))

  -- Deriving associativity of union for association list multisets

  LQunion = LQstructure .snd .snd .fst
  ALQunion = ALQstructure .snd .snd .fst

  hasAssociativeUnion : TypeWithStr ℓ S.structure → Type ℓ
  hasAssociativeUnion (_ , _ , _ , _⊔_ , _) =
    ∀ xs ys zs → (xs ⊔ ys) ⊔ zs ≡ xs ⊔ (ys ⊔ zs)

  LQassoc : hasAssociativeUnion (List/Rᴸ , LQstructure)
  LQassoc = elimProp3 (λ _ _ _ → squash/ _ _) (λ xs ys zs i → [ ++-assoc xs ys zs i ])

  ALQassoc : hasAssociativeUnion (AList/Rᴬᴸ , ALQstructure)
  ALQassoc = subst hasAssociativeUnion List/Rᴸ≡AList/Rᴬᴸ LQassoc

  -- We now show that List/Rᴸ≃FMSet

  _∷/_ : A → List/Rᴸ → List/Rᴸ
  _∷/_ = LQstructure .snd .fst

  multisetShape' : Type ℓ → Type ℓ
  multisetShape' X = X × (A → X → X) × (A → X → Const[ ℕ , isSetℕ ])

  FMSstructure : S.structure (FMSet A)
  FMSstructure = [] , _∷_ , FMS._++_ , FMScount discA

  infixr 5 _∷/_

  FMSet→List/Rᴸ : FMSet A → List/Rᴸ
  FMSet→List/Rᴸ = FMS.Rec.f squash/ [ [] ] _∷/_ β
    where
    δ : ∀ c a b xs → L.count c (a ∷ b ∷ xs) ≡ L.count c (b ∷ a ∷ xs)
    δ c a b xs with discA c a | discA c b
    δ c a b xs | yes _        | yes _ = refl
    δ c a b xs | yes _        | no  _ = refl
    δ c a b xs | no  _        | yes _ = refl
    δ c a b xs | no  _        | no  _ = refl

    γ : ∀ a b xs → Rᴸ (a ∷ b ∷ xs) (b ∷ a ∷ xs)
    γ a b xs =
      ∣ φ (a ∷ b ∷ xs) , η (a ∷ b ∷ xs) , (λ c → δ c b a xs ∙ η (a ∷ b ∷ xs) c) ∣

    β : ∀ a b [xs] → a ∷/ b ∷/ [xs] ≡ b ∷/ a ∷/ [xs]
    β a b = elimProp (λ _ → squash/ _ _) (λ xs → eq/ _ _ (γ a b xs))

  -- The inverse is induced by the standard projection of lists into finite multisets,
  -- which is a morphism of CountStructures
  -- Moreover, we need 'count-extensionality' for finite multisets
  List→FMSet : List A → FMSet A
  List→FMSet [] = []
  List→FMSet (x ∷ xs) = x ∷ List→FMSet xs

  List→FMSet-count : ∀ a xs → L.count a xs ≡ FMScount discA a (List→FMSet xs)
  List→FMSet-count a [] = refl
  List→FMSet-count a (x ∷ xs) with discA a x
  ...                         | yes _ = cong suc (List→FMSet-count a xs)
  ...                         | no  _ = List→FMSet-count a xs

  List/Rᴸ→FMSet : List/Rᴸ → FMSet A
  List/Rᴸ→FMSet [ xs ] = List→FMSet xs
  List/Rᴸ→FMSet (eq/ xs ys r i) = path i
    where
    countsAgree : ∀ a → L.count a xs ≡ L.count a ys
    countsAgree a = cong (LQstructure .snd .snd .snd a) (eq/ xs ys r)

    θ : ∀ a → FMScount discA a (List→FMSet xs) ≡ FMScount discA a (List→FMSet ys)
    θ a = sym (List→FMSet-count a xs) ∙∙ countsAgree a ∙∙ List→FMSet-count a ys

    path : List→FMSet xs ≡ List→FMSet ys
    path = FMScountExt.Thm discA _ _ θ
  List/Rᴸ→FMSet (squash/ xs/ xs/' p q i j) =
    trunc (List/Rᴸ→FMSet xs/) (List/Rᴸ→FMSet xs/') (cong List/Rᴸ→FMSet p) (cong List/Rᴸ→FMSet q) i j

  List/Rᴸ→FMSet-insert : (x : A) (ys : List/Rᴸ) → List/Rᴸ→FMSet (x ∷/ ys) ≡ x ∷ List/Rᴸ→FMSet ys
  List/Rᴸ→FMSet-insert x = elimProp (λ _ → FMS.trunc _ _) λ xs → refl

  List→FMSet-union : (xs ys : List A)
    → List→FMSet (xs ++ ys) ≡ FMS._++_ (List→FMSet xs) (List→FMSet ys)
  List→FMSet-union [] ys = refl
  List→FMSet-union (x ∷ xs) ys = cong (x ∷_) (List→FMSet-union xs ys)

  List/Rᴸ≃FMSet : List/Rᴸ ≃ FMSet A
  List/Rᴸ≃FMSet = isoToEquiv (iso List/Rᴸ→FMSet FMSet→List/Rᴸ τ σ)
    where
    σ' : (xs : List A) → FMSet→List/Rᴸ (List/Rᴸ→FMSet [ xs ]) ≡ [ xs ]
    σ' [] = refl
    σ' (x ∷ xs) = cong (x ∷/_) (σ' xs)

    σ : section FMSet→List/Rᴸ List/Rᴸ→FMSet
    σ = elimProp (λ _ → squash/ _ _) σ'

    τ' : ∀ x {xs} → List/Rᴸ→FMSet (FMSet→List/Rᴸ xs) ≡ xs → List/Rᴸ→FMSet (FMSet→List/Rᴸ (x ∷ xs)) ≡ x ∷ xs
    τ' x {xs} p = List/Rᴸ→FMSet-insert x (FMSet→List/Rᴸ xs) ∙ cong (x ∷_) p

    τ : retract FMSet→List/Rᴸ List/Rᴸ→FMSet
    τ = FMS.ElimProp.f (FMS.trunc _ _) refl τ'

  List/Rᴸ≃FMSet-EquivStr : S.equiv (List/Rᴸ , LQstructure) (FMSet A , FMSstructure) List/Rᴸ≃FMSet
  List/Rᴸ≃FMSet-EquivStr .fst = refl
  List/Rᴸ≃FMSet-EquivStr .snd .fst a xs = List/Rᴸ→FMSet-insert a xs
  List/Rᴸ≃FMSet-EquivStr .snd .snd .fst = elimProp2 (λ _ _ → trunc _ _) List→FMSet-union
  List/Rᴸ≃FMSet-EquivStr .snd .snd .snd a =
    elimProp (λ _ → isSetℕ _ _) (List→FMSet-count a)

  {-
  Putting everything together we get:
                ≃
  List/Rᴸ ------------> AList/Rᴬᴸ
    |
    |≃
    |
    ∨
                ≃
  FMSet A ------------> AssocList A
  We thus get that AList/Rᴬᴸ≃AssocList.
  Constructing such an equivalence directly requires count extensionality for association lists,
  which should be even harder to prove than for finite multisets.
  This strategy should work for all implementations of multisets with HITs.
  We just have to show that:
   ∙ The HIT is equivalent to FMSet (like AssocList)
   ∙ There is a QER between lists and the basic data type of the HIT
     with the higher constructors removed (like AList)
  Then we get that this HIT is equivalent to the corresponding set quotient that identifies elements
  that give the same count on each a : A.
  TODO: Show that all the equivalences are indeed isomorphisms of multisets not only of CountStructures!
  -}

ext: agda

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
{-# OPTIONS --sized-types #-}
open import Relation.Binary.Core

module BubbleSort.Correctness.Order  {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)
                  (trans≤ : Transitive _≤_) where

open import BubbleSort _≤_ tot≤
open import Data.Product
open import Data.List
open import Data.Sum
open import Function using (_∘_)
open import List.Sorted _≤_
open import Order.Total _≤_ tot≤
open import Size
open import SList
open import SList.Order _≤_
open import SList.Order.Properties _≤_

lemma-swap*-≤*-≤ : {ι : Size}{x t : A}{xs : SList A {ι}} → x ≤ t → xs ≤* t → proj₁ (swap* x xs) ≤* t × proj₂ (swap* x xs) ≤ t
lemma-swap*-≤*-≤ x≤t lenx = lenx , x≤t
lemma-swap*-≤*-≤ {x = x} x≤t (lecx {x = y} y≤t ys≤*t)
    with tot≤ x y
... | inj₁ x≤y = lecx x≤t (proj₁ (lemma-swap*-≤*-≤ y≤t ys≤*t)), proj₂ (lemma-swap*-≤*-≤ y≤t ys≤*t)
... | inj₂ y≤x = lecx y≤t (proj₁ (lemma-swap*-≤*-≤ x≤t ys≤*t)), proj₂ (lemma-swap*-≤*-≤ x≤t ys≤*t)

lemma-bubbleSort-≤* : {ι : Size}{t : A}{xs : SList A {ι}} → xs ≤* t → bubbleSort xs ≤* t
lemma-bubbleSort-≤* lenx = lenx
lemma-bubbleSort-≤* (lecx x≤t xs≤*t)
    with lemma-swap*-≤*-≤ x≤t xs≤*t
... | (zs≤*t , z≤t) = lemma-⊕≤* z≤t (lemma-bubbleSort-≤* zs≤*t)

lemma-swap*-≤ : {ι : Size}(x : A) → (xs : SList A {ι}) → x ≤ proj₂ (swap* x xs)
lemma-swap*-≤ x snil = refl≤
lemma-swap*-≤ x (y ∙ ys)
    with tot≤ x y
... | inj₁ x≤y = trans≤ x≤y (lemma-swap*-≤ y ys)
... | inj₂ y≤x = lemma-swap*-≤ x ys

lemma-swap*-≤* : {ι : Size}(x : A) → (xs : SList A {ι}) → proj₁ (swap* x xs) ≤* proj₂ (swap* x xs)
lemma-swap*-≤* x snil = lenx
lemma-swap*-≤* x (y ∙ ys)
    with tot≤ x y
... | inj₁ x≤y = lecx (trans≤ x≤y (lemma-swap*-≤ y ys)) (lemma-swap*-≤* y ys)
... | inj₂ y≤x = lecx (trans≤ y≤x (lemma-swap*-≤ x ys)) (lemma-swap*-≤* x ys)

lemma-bubbleSort-sorted : {ι : Size}(xs : SList A {ι}) → Sorted (unsize A (bubbleSort xs))
lemma-bubbleSort-sorted snil = nils
lemma-bubbleSort-sorted (x ∙ xs) = lemma-sorted⊕ (lemma-bubbleSort-≤* (lemma-swap*-≤* x xs)) (lemma-bubbleSort-sorted (proj₁ (swap* x xs)))

theorem-bubbleSort-sorted : (xs : List A) → Sorted (unsize A (bubbleSort (size A xs)))
theorem-bubbleSort-sorted = lemma-bubbleSort-sorted ∘ (size A)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text: module nix-emacs-agda where


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

open import lib.Base
open import lib.PathGroupoid
open import lib.PathFunctor
open import lib.Equivalences

module lib.Univalence where

{-
The map [coe-equiv] is the map which is supposed to be an equivalence according
to the univalence axiom. We do not define it directly by path induction because
it may be helpful to know definitionally what are the components.
-}
coe-equiv : ∀ {i} {A B : Type i} → A == B → A ≃ B
coe-equiv p = equiv (coe p) (coe! p) (coe!-inv-r p) (coe!-inv-l p)

{- We postulate the univalence axiom as three separate axioms because it’s more
natural this way. But it doesn’t change anything in practice. -}

postulate  -- Univalence axiom
  ua : ∀ {i} {A B : Type i} → (A ≃ B) → A == B
  coe-equiv-β : ∀ {i} {A B : Type i} (e : A ≃ B) → coe-equiv (ua e) == e
  ua-η : ∀ {i} {A B : Type i} (p : A == B) → ua (coe-equiv p) == p

ua-equiv : ∀ {i} {A B : Type i} → (A ≃ B) ≃ (A == B)
ua-equiv = equiv ua coe-equiv ua-η coe-equiv-β

{- Reductions for coercions along a path constructed with the univalence axiom -}

coe-β : ∀ {i} {A B : Type i} (e : A ≃ B) (a : A)
  → coe (ua e) a == –> e a
coe-β e a = ap (λ e → –> e a) (coe-equiv-β e)

coe!-β : ∀ {i} {A B : Type i} (e : A ≃ B) (b : B)
  → coe! (ua e) b == <– e b
coe!-β e a = ap (λ e → <– e a) (coe-equiv-β e)

{- Paths over a path in a universe in the identity fibration reduces -}

↓-idf-ua-out : ∀ {i} {A B : Type i} (e : A ≃ B) {u : A} {v : B}
  → u == v [ (λ x → x) ↓ (ua e) ]
  → –> e u == v
↓-idf-ua-out e p = ! (coe-β e _) ∙ aux (ua e) p  where

  aux : ∀ {i} {A B : Type i} (p : A == B) {u : A} {v : B}
    → u == v [ (λ x → x) ↓ p ]
    → coe p u == v
  aux idp = idf _

↓-idf-ua-in : ∀ {i} {A B : Type i} (e : A ≃ B) {u : A} {v : B}
  → –> e u == v
  → u == v [ (λ x → x) ↓ (ua e) ]
↓-idf-ua-in e p = aux (ua e) (coe-β e _ ∙ p)  where

  aux : ∀ {i} {A B : Type i} (p : A == B) {u : A} {v : B}
    → coe p u == v
    → u == v [ (λ x → x) ↓ p ]
  aux idp = idf _

{- Induction along equivalences

If [P] is a predicate over all equivalences in a universe [Type i] and [d] is a
proof of [P] over all [ide A], then we get a section of [P]
-}

equiv-induction : ∀ {i j} (P : {A B : Type i} (f : A ≃ B) → Type j)
  (d : (A : Type i) → P (ide A)) {A B : Type i} (f : A ≃ B)
  → P f
equiv-induction {i} {j} P d f =
  transport P (coe-equiv-β f)
    (aux P d (ua f)) where

  aux : ∀ {j} (P : {A : Type i} {B : Type i} (f : A ≃ B) → Type j)
    (d : (A : Type i) → P (ide A)) {A B : Type i} (p : A == B)
    → P (coe-equiv p)
  aux P d idp = d _

max_stars_repo_name: sattlerc/HoTT-Agda

max_issues_repo_name: sattlerc/HoTT-Agda

max_forks_repo_name: sattlerc/HoTT-Agda


text:
module Data.List.Relation.Binary.Subset.Propositional.Instances where

open import Data.List using (List; _∷_; [])
open import Data.List.Relation.Unary.Any using (here; there)
open import Data.List.Membership.Propositional using (_∈_; _∉_)
open import Data.List.Membership.Setoid.Properties using (∈-resp-≈)
open import Data.List.Relation.Binary.Subset.Propositional using (_⊆_)

open import Relation.Nullary.Negation using (contradiction)

open import Relation.Binary.PropositionalEquality using (sym; setoid)

open import Level using (Level)

private
  variable
    a : Level
    A : Set a
    x y : A
    xs ys : List A

-- ----------------------------------------------------------------------
-- Wrapped subset. Could use Data.Wrap but required curried arguments
-- Easier to define specific data type.

infix 4 ⦅_⊆_⦆
data ⦅_⊆_⦆ {a} {A : Set a} : List A → List A → Set a where
  [_] : xs ⊆ ys → ⦅ xs ⊆ ys ⦆

proj : ⦅ xs ⊆ ys ⦆ → xs ⊆ ys
proj [ xs⊆ys ] = xs⊆ys

-- ----------------------------------------------------------------------
-- Lemmas used for instance searching

x∉[] : x ∉ []
x∉[] = λ ()

[]⊆xs : [] ⊆ xs
[]⊆xs = λ x∈[] → contradiction x∈[] x∉[]

xs⊆x∷xs : xs ⊆ x ∷ xs
xs⊆x∷xs = there

xs⊆ys⇒x∷xs⊆x∷ys : xs ⊆ ys → x ∷ xs ⊆ x ∷ ys
xs⊆ys⇒x∷xs⊆x∷ys xs⊆ys (here y≡x) = here y≡x
xs⊆ys⇒x∷xs⊆x∷ys xs⊆ys (there y∈x∷xs) = there (xs⊆ys y∈x∷xs)

x∈ys-xs⊆ys⇒x∷xs⊆ys : x ∈ ys → xs ⊆ ys → x ∷ xs ⊆ ys
x∈ys-xs⊆ys⇒x∷xs⊆ys x∈ys xs⊆ys (here y≡x) = ∈-resp-≈ (setoid _) (sym y≡x) x∈ys
x∈ys-xs⊆ys⇒x∷xs⊆ys x∈ys xs⊆ys (there y∈x∷xs) = xs⊆ys y∈x∷xs

-- ----------------------------------------------------------------------
-- Instances

instance
  ⦃[]⊆xs⦄ : ⦅ [] ⊆ xs ⦆
  ⦃[]⊆xs⦄ = [ []⊆xs ]

  -- Removed to improve instance search, syntax directed.

  -- ⦃xs⊆x∷xs⦄ : ⦅ xs ⊆ x ∷ xs ⦆
  -- ⦃xs⊆x∷xs⦄ = [ xs⊆x∷xs ]

  -- ⦃xs⊆ys⇒x∷xs⊆x∷ys⦄ : ⦃ ⦅ xs ⊆ ys ⦆ ⦄ → ⦅ x ∷ xs ⊆ x ∷ ys ⦆
  -- ⦃xs⊆ys⇒x∷xs⊆x∷ys⦄ ⦃ [ xs⊆ys ] ⦄ = [ xs⊆ys⇒x∷xs⊆x∷ys xs⊆ys ]

  ⦃x∈ys-xs⊆ys⇒x∷xs⊆ys⦄ : ⦃ x ∈ ys ⦄ → ⦃ ⦅ xs ⊆ ys ⦆ ⦄ → ⦅ x ∷ xs ⊆ ys ⦆
  ⦃x∈ys-xs⊆ys⇒x∷xs⊆ys⦄ ⦃ x∈ys ⦄ ⦃ [ xs⊆ys ] ⦄ = [ x∈ys-xs⊆ys⇒x∷xs⊆ys x∈ys xs⊆ys ]

max_stars_repo_name: johnyob/agda-union

max_issues_repo_name: johnyob/agda-union

max_forks_repo_name: johnyob/agda-union


text:
module Pin where

-- N-dimensional version of Pi

-- open import Data.Fin
open import Data.Nat
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Function renaming (_∘_ to _○_)
open import Relation.Binary.PropositionalEquality using (module ≡-Reasoning)
open ≡-Reasoning
open import Algebra
open import Data.Nat.Properties
open CommutativeSemiring commutativeSemiring using (+-commutativeMonoid)
open CommutativeMonoid +-commutativeMonoid using ()
     renaming (comm to +-comm)

--infix  4  _≡_   -- propositional equality
--infixr 8  _∘_   -- path composition
infixr 10 _◎_
infixr 30 _⟷_
infixr 9 _>>>_
-- infixr 30 _⟺_

------------------------------------------------------------------------------
-- base types (or 0d types) are the usual finite types

data T : Set where
  Zero  : T
  One   : T
  Plus  : T → T → T
  Times : T → T → T

-- Combinators on 0d types

data _⟷_ : T → T → Set where
  unite₊  : { t : T } → Plus Zero t ⟷ t
  uniti₊  : { t : T } → t ⟷ Plus Zero t
  swap₊   : { t₁ t₂ : T } → Plus t₁ t₂ ⟷ Plus t₂ t₁
  assocl₊ : { t₁ t₂ t₃ : T } → Plus t₁ (Plus t₂ t₃) ⟷ Plus (Plus t₁ t₂) t₃
  assocr₊ : { t₁ t₂ t₃ : T } → Plus (Plus t₁ t₂) t₃ ⟷ Plus t₁ (Plus t₂ t₃)
  unite⋆  : { t : T } → Times One t ⟷ t
  uniti⋆  : { t : T } → t ⟷ Times One t
  swap⋆   : { t₁ t₂ : T } → Times t₁ t₂ ⟷ Times t₂ t₁
  assocl⋆ : { t₁ t₂ t₃ : T } → Times t₁ (Times t₂ t₃) ⟷ Times (Times t₁ t₂) t₃
  assocr⋆ : { t₁ t₂ t₃ : T } → Times (Times t₁ t₂) t₃ ⟷ Times t₁ (Times t₂ t₃)
  distz    : { t : T } → Times Zero t ⟷ Zero
  factorz  : { t : T } → Zero ⟷ Times Zero t
  dist    : { t₁ t₂ t₃ : T } →
            Times (Plus t₁ t₂) t₃ ⟷ Plus (Times t₁ t₃) (Times t₂ t₃)
  factor  : { t₁ t₂ t₃ : T } →
            Plus (Times t₁ t₃) (Times t₂ t₃) ⟷ Times (Plus t₁ t₂) t₃
  id⟷   : { t : T } → t ⟷ t
  sym⟷    : { t₁ t₂ : T } → (t₁ ⟷ t₂) → (t₂ ⟷ t₁)
  _◎_    : { t₁ t₂ t₃ : T } → (t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)
  _⊕_    : { t₁ t₂ t₃ t₄ : T } →
           (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (Plus t₁ t₂ ⟷ Plus t₃ t₄)
  _⊗_    : { t₁ t₂ t₃ t₄ : T } →
           (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (Times t₁ t₂ ⟷ Times t₃ t₄)

-- Semantics

⟦_⟧ : T → Set
⟦ Zero ⟧         = ⊥
⟦ One ⟧          = ⊤
⟦ Plus t1 t2 ⟧   = ⟦ t1 ⟧ ⊎ ⟦ t2 ⟧
⟦ Times t1 t2 ⟧  = ⟦ t1 ⟧ × ⟦ t2 ⟧

mutual

  eval : {t₁ t₂ : T} → (t₁ ⟷ t₂) → ⟦ t₁ ⟧ → ⟦ t₂ ⟧
  eval unite₊ (inj₁ ())
  eval unite₊ (inj₂ v) = v
  eval uniti₊ v = inj₂ v
  eval swap₊ (inj₁ v) = inj₂ v
  eval swap₊ (inj₂ v) = inj₁ v
  eval assocl₊ (inj₁ v) = inj₁ (inj₁ v)
  eval assocl₊ (inj₂ (inj₁ v)) = inj₁ (inj₂ v)
  eval assocl₊ (inj₂ (inj₂ v)) = inj₂ v
  eval assocr₊ (inj₁ (inj₁ v)) = inj₁ v
  eval assocr₊ (inj₁ (inj₂ v)) = inj₂ (inj₁ v)
  eval assocr₊ (inj₂ v) = inj₂ (inj₂ v)
  eval unite⋆ (tt , v) = v
  eval uniti⋆ v = (tt , v)
  eval swap⋆ (v1 , v2) = (v2 , v1)
  eval assocl⋆ (v1 , (v2 , v3)) = ((v1 , v2) , v3)
  eval assocr⋆ ((v1 , v2) , v3) = (v1 , (v2 , v3))
  eval distz (() , v)
  eval factorz ()
  eval dist (inj₁ v1 , v3) = inj₁ (v1 , v3)
  eval dist (inj₂ v2 , v3) = inj₂ (v2 , v3)
  eval factor (inj₁ (v1 , v3)) = (inj₁ v1 , v3)
  eval factor (inj₂ (v2 , v3)) = (inj₂ v2 , v3)
  eval id⟷ v = v
  eval (sym⟷ c) v = evalB c v
  eval (c₁ ◎ c₂) v = eval c₂ (eval c₁ v)
  eval (c₁ ⊕ c₂) (inj₁ v) = inj₁ (eval c₁ v)
  eval (c₁ ⊕ c₂) (inj₂ v) = inj₂ (eval c₂ v)
  eval (c₁ ⊗ c₂) (v₁ , v₂) = (eval c₁ v₁ , eval c₂ v₂)

  evalB : {t₁ t₂ : T} → (t₁ ⟷ t₂) → ⟦ t₂ ⟧ → ⟦ t₁ ⟧
  evalB unite₊ v = inj₂ v
  evalB uniti₊ (inj₁ ())
  evalB uniti₊ (inj₂ v) = v
  evalB swap₊ (inj₁ v) = inj₂ v
  evalB swap₊ (inj₂ v) = inj₁ v
  evalB assocl₊ (inj₁ (inj₁ v)) = inj₁ v
  evalB assocl₊ (inj₁ (inj₂ v)) = inj₂ (inj₁ v)
  evalB assocl₊ (inj₂ v) = inj₂ (inj₂ v)
  evalB assocr₊ (inj₁ v) = inj₁ (inj₁ v)
  evalB assocr₊ (inj₂ (inj₁ v)) = inj₁ (inj₂ v)
  evalB assocr₊ (inj₂ (inj₂ v)) = inj₂ v
  evalB unite⋆ v = (tt , v)
  evalB uniti⋆ (tt , v) = v
  evalB swap⋆ (v1 , v2) = (v2 , v1)
  evalB assocl⋆ ((v1 , v2) , v3) = (v1 , (v2 , v3))
  evalB assocr⋆ (v1 , (v2 , v3)) = ((v1 , v2) , v3)
  evalB distz ()
  evalB factorz (() , v)
  evalB dist (inj₁ (v1 , v3)) = (inj₁ v1 , v3)
  evalB dist (inj₂ (v2 , v3)) = (inj₂ v2 , v3)
  evalB factor (inj₁ v1 , v3) = inj₁ (v1 , v3)
  evalB factor (inj₂ v2 , v3) = inj₂ (v2 , v3)
  evalB id⟷ v = v
  evalB (sym⟷ c) v = eval c v
  evalB (c₁ ◎ c₂) v = evalB c₁ (evalB c₂ v)
  evalB (c₁ ⊕ c₂) (inj₁ v) = inj₁ (evalB c₁ v)
  evalB (c₁ ⊕ c₂) (inj₂ v) = inj₂ (evalB c₂ v)
  evalB (c₁ ⊗ c₂) (v₁ , v₂) = (evalB c₁ v₁ , evalB c₂ v₂)

------------------------------------------------------------------------------
-- N dimensional version

data C : ℕ → Set where
  ZD   : T → C 0
  Node : {n : ℕ} → C n → C n → C (suc n)

liftN : (n : ℕ) → (t : T) → C n
liftN 0 t = ZD t
liftN (suc n) t = Node (liftN n t) (liftN n Zero)

zeroN : (n : ℕ) → C n
zeroN n = liftN n Zero

oneN : (n : ℕ) → C n
oneN n = liftN n One

plus : {n : ℕ} → C n → C n → C n
plus (ZD t₁) (ZD t₂) = ZD (Plus t₁ t₂)
plus (Node c₁ c₂) (Node c₁' c₂') = Node (plus c₁ c₁') (plus c₂ c₂')

times : {m n : ℕ} → C m → C n → C (m + n)
times (ZD t1) (ZD t2) = ZD (Times t1 t2)
times (ZD t) (Node c1 c2) = Node (times (ZD t) c1) (times (ZD t) c2)
times (Node c1 c2) c = Node (times c1 c) (times c2 c)

-- Combinators on nd types

data _⟺_ : {n : ℕ} → C n → C n → Set where
  baseC : {t₁ t₂ : T} → (t₁ ⟷ t₂) → ((ZD t₁) ⟺ (ZD t₂))
  nodeC : {n : ℕ} {c₁ : C n} {c₂ : C n} {c₃ : C n} {c₄ : C n} →
          (c₁ ⟺ c₂) → (c₃ ⟺ c₄) → ((Node c₁ c₃) ⟺ (Node c₂ c₄))
  zerolC : {n : ℕ} {c : C n} → ((Node c c) ⟺ (zeroN (suc n)))
  zerorC : {n : ℕ} {c : C n} → ((zeroN (suc n)) ⟺ (Node c c))

-- Def. 2.1 lists the conditions for J-graded bipermutative category

mutual

  _>>>_ = seqF

  idN⟷ : {n : ℕ} {c : C n} → c ⟺ c
  idN⟷ {0} {ZD t} = baseC (id⟷ {t})
  idN⟷ {suc n} {Node c₁ c₂} = nodeC (idN⟷ {n} {c₁}) (idN⟷ {n} {c₂})

  symN⟷ : {n : ℕ} {c₁ c₂ : C n} → (c₁ ⟺ c₂) → (c₂ ⟺ c₁)
  symN⟷ (baseC f) = baseC (sym⟷ f)
  symN⟷ (nodeC f g) = nodeC (symN⟷ f) (symN⟷ g)
  symN⟷ (zerolC {n} {c}) = zerorC {n} {c}
  symN⟷ (zerorC {n} {c}) = zerolC {n} {c}

  seqF : {n : ℕ} {c₁ c₂ c₃ : C n} →
         (c₁ ⟺ c₂) → (c₂ ⟺ c₃) → (c₁ ⟺ c₃)
  seqF {0} (baseC f) (baseC g) = baseC (f ◎ g)
  seqF {suc n} (nodeC f g) (nodeC f' g') = nodeC (seqF f f') (seqF g g')
  seqF {suc n} (nodeC f g) zerolC = nodeC (seqF f {!!}) (seqF g {!!})
  seqF {suc n} (nodeC f g) zerorC = {!!}
  seqF {suc n} zerolC (nodeC f g) = {!!}
  seqF {suc n} zerolC zerolC = {!!}
  seqF {suc n} zerolC zerorC = {!!}
  seqF {suc n} zerorC (nodeC f g) = {!!}
  seqF {suc n} zerorC zerolC = {!!}
  seqF {suc n} zerorC zerorC = {!!}

{--

  plusF : {n : ℕ} {c₁ c₂ c₃ c₄ : C n} →
          (c₁ ⟺ c₂) → (c₃ ⟺ c₄) → (plus c₁ c₃ ⟺ plus c₂ c₄)
  plusF (baseC f) (baseC g) = baseC (f ⊕ g)
  plusF (nodeC f) (nodeC g) = nodeC {!!}

  timesF : {m n : ℕ} {c₁ c₂ : C m} {c₃ c₄ : C n} →
           (c₁ ⟺ c₂) → (c₃ ⟺ c₄) → (times c₁ c₃ ⟺ times c₂ c₄)
  timesF (baseC f) (baseC g) = baseC (f ⊗ g)
  timesF (baseC f) (nodeC g) = nodeC {!!}
{--
    nodeC (
    seqF (plusF (timesF (baseC f) idN⟷) idN⟷) (
    seqF (seqF (plusF swapN⋆ swapN⋆) factorN) (
    seqF (timesF idN⟷ g) (
    seqF (seqF distN (plusF swapN⋆ swapN⋆))
    ((plusF (timesF (baseC (sym⟷ f)) idN⟷) idN⟷))))))
--}
  timesF (nodeC f) (baseC g) = {!!}
  timesF (nodeC f) (nodeC g) = nodeC {!!}
  -- nodeC (timesF f₁ g) (timesF f₂ g)
  -- f : t1 <-> t2
  -- g : c1 + c4 <=> c3 + c2
  --?24 : plus (times (ZD t₁) c₁) (times (ZD t₂) c₄) ⟺
  --      plus (times (ZD t₁) c₃) (times (ZD t₂) c₂)
  {--
  plus (times (ZD t₁) c₁) (times (ZD t₂) c₄) ⟺
  -> s1
  plus (times (ZD t2) c₁) (times (ZD t₂) c₄) ⟺
  -> s2
  times (ZD t2) (plus c1 c4)
  -> s3
  times (ZD t2) (plus c3 c2)
  -> s4
  plus (times (ZD t2) c3) (times (ZD t2) c2)
  -> s5
  plus (times (ZD t1) c3) (times (ZD t2) c2)
  --}

  uniteN₊ : {n : ℕ} {c : C n} → (plus (zeroN n) c) ⟺ c
  uniteN₊ {0} {ZD t} = baseC (unite₊ {t})
  uniteN₊ {suc n} {Node c₁ c₂} =
    nodeC (seqF assocrN₊ (seqF (plusF idN⟷ swapN₊) assoclN₊))

  unitiN₊ : {n : ℕ} {c : C n} → c ⟺ (plus (zeroN n) c)
  unitiN₊ {0} {ZD t} = baseC (uniti₊ {t})
  unitiN₊ {suc n} {Node c₁ c₂} =
    nodeC (assoclN₊ >>> swapN₊ >>> (plusF idN⟷ swapN₊))

  swapN₊ : { n : ℕ } { c₁ c₂ : C n } → plus c₁ c₂ ⟺ plus c₂ c₁
  swapN₊ {0} {ZD t₁} {ZD t₂} = baseC (swap₊ {t₁} {t₂})
  swapN₊ {suc n} {Node c₁ c₂} {Node c₁' c₂'} =
    nodeC (swapN₊ >>> (plusF swapN₊ swapN₊))

  assoclN₊ : { n : ℕ } { c₁ c₂ c₃ : C n } →
             plus c₁ (plus c₂ c₃) ⟺ plus (plus c₁ c₂) c₃
  assoclN₊ {0} {ZD t₁} {ZD t₂} {ZD t₃} = baseC (assocl₊ {t₁} {t₂} {t₃})
  assoclN₊ {suc n} {Node c₁ c₂} {Node c₃ c₄} {Node c₅ c₆} =
      nodeC (swapN₊ >>> (plusF assocrN₊ assoclN₊))

  assocrN₊ : { n : ℕ } { c₁ c₂ c₃ : C n } →
             plus (plus c₁ c₂) c₃ ⟺ plus c₁ (plus c₂ c₃)
  assocrN₊ {0} {ZD t₁} {ZD t₂} {ZD t₃} = baseC (assocr₊ {t₁} {t₂} {t₃})
  assocrN₊ {suc n} {Node c₁ c₂} {Node c₃ c₄} {Node c₅ c₆} =
    nodeC (swapN₊ >>> (plusF assoclN₊ assocrN₊))

  uniteN⋆ : {n : ℕ} {c : C n} → times (ZD One) c ⟺ c
  uniteN⋆ {0} {ZD t} = baseC (unite⋆ {t})
  uniteN⋆ {suc n} {Node c₁ c₂} = nodeC {!!}

  unitiN⋆ : {n : ℕ} {c : C n} → c ⟺ times (ZD One) c
  unitiN⋆ {0} {ZD t} = baseC (uniti⋆ {t})
  unitiN⋆ {suc n} {Node c₁ c₂} = nodeC {!!}

  -- Ugly hack or feature ???

  times' : {m n : ℕ} → C n → C m → C (m + n)
  times' {m} {n} c₁ c₂ rewrite +-comm m n = times c₁ c₂

  swapN⋆ : {m n : ℕ} {c₁ : C m} {c₂ : C n} → times c₁ c₂ ⟺ times' c₂ c₁
  swapN⋆ {0} {0} {ZD t₁} {ZD t₂} = baseC (swap⋆ {t₁} {t₂})
  swapN⋆ {0} {suc n} {ZD t} {Node c₁ c₂} = {!!}
  --nodeC (swapN⋆ {0} {n} {ZD t} {c₁}) (swapN⋆ {0} {n} {ZD t} {c₂})
  swapN⋆ {suc m} {0} {Node c₁ c₂} {ZD t} = {!!}
  --nodeC (swapN⋆ {0} {n} {c₁} {ZD t}) (swapN⋆ {0} {n} {c₂} {ZD t})
  swapN⋆ {suc m} {n} {Node c₁ c₂} {c} = {!!}
  --nodeC (swapN⋆ {m} {n} {c₁} {c}) (swapN⋆ {m} {n} {c₂} {c})

  TODO : Set
  TODO = {!!}

  assoclN⋆ : {m n k : ℕ} {c₁ : C m} {c₂ : C n} {c₃ : C k} → TODO
  --           times c₁ (times c₂ c₃) ⟺ times (times c₁ c₂) c₃
  assoclN⋆ = {!!}

  assocrN⋆ : { m n k : ℕ } { c₁ : C m } { c₂ : C n } { c₃ : C k } → TODO
  --            times (times c₁ c₂) c₃ ⟺ times c₁ (times c₂ c₃)
  assocrN⋆ = {!!}

  distzN : {m n : ℕ} {c : C n} → times (zeroN m) c ⟺ zeroN (m + n)
  distzN {0} {0} {ZD t} = baseC (distz {t})
  distzN {0} {suc n} {Node c₁ c₂} = nodeC {!!}
  --  nodeC (distzN {0} {n} {c₁}) (distzN {0} {n} {c₂})
  distzN {suc m} {n} {c} = nodeC {!!}
  --  nodeC (distzN {m} {n} {c}) (distzN {m} {n} {c})

  factorzN : { m n : ℕ } { c : C n } → zeroN (m + n) ⟺ times (zeroN m) c
  factorzN {0} {0} {ZD t} = baseC (factorz {t})
  factorzN {0} {suc n} {Node c₁ c₂} = nodeC {!!}
  --  nodeC (factorzN {0} {n} {c₁}) (factorzN {0} {n} {c₂})
  factorzN {suc m} {n} {c} = nodeC {!!}
  --  nodeC (factorzN {m} {n} {c}) (factorzN {m} {n} {c})

  distN : {m n : ℕ} {c₁ c₂ : C m} {c₃ : C n} →
          times (plus c₁ c₂) c₃ ⟺ plus (times c₁ c₃) (times c₂ c₃)
  distN {0} {0} {ZD t₁} {ZD t₂} {ZD t₃} = baseC (dist {t₁} {t₂} {t₃})
  distN {0} {suc n} {ZD t₁} {ZD t₂} {Node c₁ c₂} = nodeC {!!}
  --  nodeC
  --    (distN {0} {n} {ZD t₁} {ZD t₂} {c₁})
  --    (distN {0} {n} {ZD t₁} {ZD t₂} {c₂})
  distN {suc m} {n} {Node c₁ c₂} {Node c₃ c₄} {c} = nodeC {!!}
  --  nodeC
  --    ((distN {m} {n} {c₁} {c₃} {c}))
  --    ((distN {m} {n} {c₂} {c₄} {c}))

  factorN : {m n : ℕ} {c₁ c₂ : C m} {c₃ : C n} →
            plus (times c₁ c₃) (times c₂ c₃) ⟺ times (plus c₁ c₂) c₃
  factorN {0} {0} {ZD t₁} {ZD t₂} {ZD t₃} = baseC (factor {t₁} {t₂} {t₃})
  factorN {0} {suc n} {ZD t₁} {ZD t₂} {Node c₁ c₂} = nodeC {!!}
  --  nodeC
  --    (factorN {0} {n} {ZD t₁} {ZD t₂} {c₁})
  --    (factorN {0} {n} {ZD t₁} {ZD t₂} {c₂})
  factorN {suc m} {n} {Node c₁ c₂} {Node c₃ c₄} {c} = nodeC {!!}
  --  nodeC
  --    ((factorN {m} {n} {c₁} {c₃} {c}))
  --    ((factorN {m} {n} {c₂} {c₄} {c}))

  --?25 : plus (times .c₁ .c₃) (times .c₆ .c₄) ⟺
  --      plus (times .c₅ .c₃) (times .c₂ .c₄)

  {--
  data _⟺_ : {n : ℕ} → C n → C n → Set where
    baseC : {t₁ t₂ : T} → (t₁ ⟷ t₂) → ((ZD t₁) ⟺ (ZD t₂))
    nodeC : {n : ℕ} {c₁ : C n} {c₂ : C n} {c₃ : C n} {c₄ : C n} →
          (plus c₁ c₄ ⟺ plus c₃ c₂) →
          ((Node c₁ c₃) ⟺ (Node c₂ c₄))

--}

-- eta/epsilon/trace

------------------------------------------------------------------------------
-- Semantics

⟦_⟧C : {n : ℕ} → C n → Set
⟦_⟧C (ZD t) = ⟦ t ⟧
⟦_⟧C (Node c₁ c₂) = ⟦ c₁ ⟧C ⊎ ⟦ c₂ ⟧C

evalC : {n : ℕ} {c₁ c₂ : C n} → (c₁ ⟺ c₂) → ⟦ c₁ ⟧C → ⟦ c₂ ⟧C
evalC (baseC iso) v = eval iso v
evalC (nodeC iso) (inj₁ v) = {!!} -- inj₁ (evalC iso v)
evalC (nodeC iso) (inj₂ v) = {!!} -- inj₂ (evalC iso v)

------------------------------------------------------------------------------
-- Example

-- Let's try a 3d program

Bool : T
Bool = Plus One One

vtrue : ⟦ Bool ⟧
vtrue = inj₁ tt

vfalse : ⟦ Bool ⟧
vfalse = inj₂ tt

Bool² : T
Bool² = Times Bool Bool

Bool³ : T
Bool³ = Times Bool² Bool

cond : {t₁ t₂ : T} → (t₁ ⟷ t₂) → (t₁ ⟷ t₂) →
       ((Times Bool t₁) ⟷ (Times Bool t₂))
cond f g = dist ◎ ((id⟷ ⊗ f) ⊕ (id⟷ ⊗ g)) ◎ factor

controlled : {t : T} → (t ⟷ t) → ((Times Bool t) ⟷ (Times Bool t))
controlled f = cond f id⟷

cnot : Bool² ⟷ Bool²
cnot = controlled swap₊

toffoli : Bool³ ⟷ Bool³
toffoli = assocr⋆ ◎ controlled cnot ◎ assocl⋆

test₁ : ⟦ Bool³ ⟧
test₁ = eval toffoli ((vtrue , vtrue) , vfalse)

--

condN : {n : ℕ} {c₁ c₂ : C n} → (c₁ ⟺ c₂) → (c₁ ⟺ c₂) →
        ((times (ZD Bool) c₁) ⟺ (times (ZD Bool) c₂))
condN {n} {c₁} {c₂} f g =
  (seqF (distN {0} {n} {ZD One} {ZD One} {c₁})
  (seqF (plusF {n}
          (timesF {0} {n} (idN⟷ {0} {ZD One}) f)
          (timesF {0} {n} (idN⟷ {0} {ZD One}) g))
  (factorN {0} {n} {ZD One} {ZD One} {c₂})))

controlledN : {n : ℕ} {c : C n} →
              (c ⟺ c) → ((times (ZD Bool) c) ⟺ (times (ZD Bool) c))
controlledN f = condN f idN⟷

BoolN : (n : ℕ) → C n
BoolN n = plus (oneN n) (oneN n)

{--
Note: liftN 3 Bool is not quite the same as plus (oneN 3) (oneN 3)

plus (oneN 3) (oneN 3)
=
Node
(Node
  (Node (ZD (Plus One One)) (ZD (Plus Zero Zero)))
  (Node (ZD (Plus Zero Zero)) (ZD (Plus Zero Zero))))
(Node
  (Node (ZD (Plus Zero Zero)) (ZD (Plus Zero Zero)))
  (Node (ZD (Plus Zero Zero)) (ZD (Plus Zero Zero))))

liftN 3 Bool
=
Node
(Node
  (Node (ZD (Plus One One)) (ZD Zero))
  (Node (ZD Zero) (ZD Zero)))
(Node
  (Node (ZD Zero) (ZD Zero))
  (Node (ZD Zero) (ZD Zero)))
--}

cnotN : {n : ℕ} → ((times (ZD Bool) (BoolN n)) ⟺ (times (ZD Bool) (BoolN n)))
cnotN {n} = controlledN {n} (swapN₊ {n} {oneN n} {oneN n})

-- Can't do toffoliN until we get all the products done
--}

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

{--

CODE THAT TRIED TO KEEP PROOF THAT DIMENSIONS ARE EQUAL

------------------------------------------------------------------------------
-- Types indexed by dimension... n-dimensional cubes
-- n-dimensional types represented as trees of depth n

-- Silly lemmas that should be in the library somewhere

suc-inj : {m n : ℕ} → suc m ≡ suc n → m ≡ n
suc-inj {0} {0} refl = refl
suc-inj {0} {suc i} ()
suc-inj {suc i} {suc .i} refl = refl

data C : ℕ → Set where
  ZD   : T → C 0
  Node : {m n : ℕ} → C m → C n → (m ≡ n) → C (suc n)
  Lower : {n : ℕ} → (c₁ c₂ : C n) → (c₁ ≡ c₂) → C 0

zeroN : (n : ℕ) → C n
zeroN 0 = ZD Zero
zeroN (suc n) = Node (zeroN n) (zeroN n) refl

plus : {m n : ℕ} → C m → C n → (m ≡ n) → C n
plus (ZD _) (Node _ _ _) ()
plus (Node _ _ _) (ZD _) ()
plus (ZD t1) (ZD t2) refl = ZD (Plus t1 t2)
plus {suc .m₂} {suc .m₂'}
     (Node {m₁} {m₂} c1 c2 p₁)
     (Node {m₁'} {m₂'} c1' c2' p₁') p =
  Node (plus c1 c1' q)
       (plus c2 c2' (suc-inj p))
       p₁'
  where q = begin
             m₁
              ≡⟨ p₁ ⟩
             m₂
              ≡⟨ suc-inj p ⟩
             m₂'
              ≡⟨ sym p₁' ⟩
             m₁' ∎
plus _ _ _ = {!!}

times : {m n : ℕ} → C m → C n → C (m + n)
times (ZD t1) (ZD t2) = ZD (Times t1 t2)
times (ZD t) (Node c1 c2 p) = Node (times (ZD t) c1) (times (ZD t) c2) p
times {n = n} (Node c1 c2 p) c =
  Node (times c1 c) (times c2 c) (cong (λ z → z + n) p)
times _ _ = {!!}

-- Combinators on nd types

data _⟺_ : {m n : ℕ} → C m → C n → (m ≡ n) → Set where
  baseC : { t₁ t₂ : T } → (t₁ ⟷ t₂) → (_⟺_ (ZD t₁) (ZD t₂) refl)
  nodeC : {m n k l : ℕ} {c₁ : C m} {c₂ : C n} {c₃ : C k} {c₄ : C l}
          {p₁ : m ≡ n} {p₂ : k ≡ l} {p : k ≡ m} →
           (_⟺_ c₁ c₂ p₁) → (_⟺_ c₃ c₄ p₂) →
           (_⟺_ (Node c₁ c₃ (sym p))
                (Node c₂ c₄ (trans (trans (sym p₁) (sym p)) p₂))
                (cong suc p₂))
  eta : {m : ℕ} {c : C m} → _⟺_ (ZD Zero) (Lower c c refl) refl

-- Def. 2.1 lists the conditions for J-graded bipermutative category

-- (0)
-- the additive unit and assoc are implicit in the paper

uniteN₊ : {m : ℕ} {c : C m} → _⟺_ (plus (zeroN m) c refl) c refl
uniteN₊ {0} {ZD t} = baseC (unite₊ {t})
uniteN₊ {suc m} {Node {n} {.m} c₁ c₂ n≡m} = {!!}
uniteN₊ {_} {_} = {!!}

unitiN₊ : {m : ℕ} {c : C m} → _⟺_ c (plus (zeroN m) c refl) refl
unitiN₊ {0} {ZD t} = baseC (uniti₊ {t})
unitiN₊ {suc m} {Node {n} {.m} c₁ c₂ n≡m} = {!!}
--  nodeC (unitiN₊ {n} {c₁}) (unitiN₊ {n} {c₂})
unitiN₊ {_} {_} = {!!}

assoclN₊ : { n : ℕ } { c₁ c₂ c₃ : C n } →
           plus c₁ (plus c₂ c₃) ⟺ plus (plus c₁ c₂) c₃
assoclN₊ {0} {ZD t₁} {ZD t₂} {ZD t₃} = baseC (assocl₊ {t₁} {t₂} {t₃})
assoclN₊ {suc n} {Node c₁ c₂} {Node c₃ c₄} {Node c₅ c₆} =
  nodeC (assoclN₊ {n} {c₁} {c₃} {c₅}) (assoclN₊ {n} {c₂} {c₄} {c₆})

assocrN₊ : { n : ℕ } { c₁ c₂ c₃ : C n } →
           plus (plus c₁ c₂) c₃ ⟺ plus c₁ (plus c₂ c₃)
assocrN₊ {0} {ZD t₁} {ZD t₂} {ZD t₃} = baseC (assocr₊ {t₁} {t₂} {t₃})
assocrN₊ {suc n} {Node c₁ c₂} {Node c₃ c₄} {Node c₅ c₆} =
  nodeC (assocrN₊ {n} {c₁} {c₃} {c₅}) (assocrN₊ {n} {c₂} {c₄} {c₆})

-- (1) have times functor on objects
-- define times functor on combinators
-- timesF should satisfying assoc and unitality conditions...
-- diagram on top of p.6 should commute

timesF : { m n : ℕ } { c₁ : C m } { c₂ : C m } { c₃ : C n } { c₄ : C n } →
         (c₁ ⟺ c₂) → (c₃ ⟺ c₄) → (times c₁ c₃ ⟺ times c₂ c₄)
timesF {0} {0} {ZD t₁} {ZD t₂} {ZD t₃} {ZD t₄} (baseC f) (baseC g) =
  baseC (_⊗_ {t₁} {t₃} {t₂} {t₄} f g)
timesF {0} {suc n} {ZD t₁} {ZD t₂} {Node c₁ c₂} {Node c₃ c₄}
       (baseC f) (nodeC g₁ g₂) = nodeC (timesF (baseC f) g₁) (timesF (baseC f) g₂)
timesF {suc m} {n} {Node c₁ c₂} {Node c₃ c₄} {c₅} {c₆}
       (nodeC f₁ f₂) g = nodeC (timesF f₁ g) (timesF f₂ g)

-- (2) there is a unit object One of dimension 0

uniteN⋆ : {n : ℕ} {c : C n} → times (ZD One) c ⟺ c
uniteN⋆ {0} {ZD t} = baseC (unite⋆ {t})
uniteN⋆ {suc n} {Node c₁ c₂} = nodeC (uniteN⋆ {n} {c₁}) (uniteN⋆ {n} {c₂})

unitiN⋆ : {n : ℕ} {c : C n} → c ⟺ times (ZD One) c
unitiN⋆ {0} {ZD t} = baseC (uniti⋆ {t})
unitiN⋆ {suc n} {Node c₁ c₂} = nodeC (unitiN⋆ {n} {c₁}) (unitiN⋆ {n} {c₂})

-- (3) swap

swapN⋆ : {m n : ℕ} {c₁ : C m} {c₂ : C n} → times c₁ c₂ ⟺ times c₂ c₁
swapN⋆ {0} {0} {ZD t₁} {ZD t₂} = baseC (swap⋆ {t₁} {t₂})
swapN⋆ = ?

swapN₊ : { n : ℕ } { c₁ c₂ : C n } → plus c₁ c₂ ⟺ plus c₂ c₁
swapN₊ {0} {ZD t₁} {ZD t₂} = baseC (swap₊ {t₁} {t₂})
swapN₊ {suc n} {Node c₁ c₂} {Node c₁' c₂'} =
  nodeC (swapN₊ {n} {c₁} {c₁'}) (swapN₊ {n} {c₂} {c₂'})

distzN : {m n : ℕ} {c : C n} → times (zeroN m) c ⟺ zeroN (m + n)
distzN {0} {0} {ZD t} = baseC (distz {t})
distzN {0} {suc n} {Node c₁ c₂} =
  nodeC (distzN {0} {n} {c₁}) (distzN {0} {n} {c₂})
distzN {suc m} {n} {c} =
  nodeC (distzN {m} {n} {c}) (distzN {m} {n} {c})

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

  assocl⋆ : { m n k : ℕ } { c₁ : C m } { c₂ : C n } { c₃ : C k } →
            times c₁ (times c₂ c₃) ⟺ times (times c₁ c₂) c₃
  assocr⋆ : { m n k : ℕ } { c₁ : C m } { c₂ : C n } { c₃ : C k } →
            times (times c₁ c₂) c₃ ⟺ times c₁ (times c₂ c₃)
  distz    : { m n : ℕ } { c : C n } → times (zeroN m) c ⟺ zeroN m
  factorz  : { m n : ℕ } { c : C n } → zeroN m ⟺ times (zeroN m) c
  dist    : { m n : ℕ } { c₁ c₂ : C m } { c₃ : C n } →
            times (plus c₁ c₂) c₃ ⟺ plus (times c₁ c₃) (times c₂ c₃)
  factor  : { m n : ℕ } { c₁ c₂ : C m } { c₃ : C n } →
            plus (times c₁ c₃) (times c₂ c₃) ⟺ times (plus c₁ c₂) c₃
  id⟷   : { n : ℕ } { c : C n } → c ⟺ c
  sym    : { m n : ℕ } { c₁ : C m } { c₂ : C n } → (c₁ ⟺ c₂) → (c₂ ⟺ c₁)
  _◎_    : { m n k : ℕ } { c₁ : C m } { c₂ : C n } { c₃ : C k } →
           (c₁ ⟺ c₂) → (c₂ ⟺ c₃) → (c₁ ⟺ c₃)
  _⊕_    : { m n : ℕ } { c₁ c₃ : C m } { c₂ c₄ : C n } →
           (c₁ ⟺ c₂) → (c₃ ⟺ c₄) → (plus c₁ c₃ ⟺ plus c₂ c₄)

------------------------------------------------------------------------------
-- Semantics

-- probably should have our own × ?
-- should be a sum !
-- we have a value in one of the corners; not in all of them at once

⟦_⟧C : {n : ℕ} → C n → Set
⟦_⟧C (ZD t) = ⟦ t ⟧
⟦_⟧C (Node c₁ c₂ _) = ⟦ c₁ ⟧C ⊎ ⟦ c₂ ⟧C
⟦_⟧C (Lower c₁ c₂ _) = ⊥

evalC : {n m : ℕ} {c₁ : C n} {c₂ : C m} {p : n ≡ m} →
        _⟺_ c₁ c₂ p → ⟦ c₁ ⟧C → ⟦ c₂ ⟧C
evalC (baseC iso) v = eval iso v
evalC (nodeC isoL isoR) (inj₁ v) = inj₁ (evalC isoL v)
evalC (nodeC isoL isoR) (inj₂ v) = inj₂ (evalC isoR v)
evalC _ _ = {!!}

-- now add etas and epsilons...
--}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
{-# OPTIONS --allow-unsolved-metas #-}

module Issue442 where

postulate
  A : Set
  f : (P : A → A → Set) → (∀ {x} → P x x) →
      (∀ {x y z} → P y z → P x y → A) → A
  P : A → A → Set
  reflP : ∀ {x} → P x x
  g : ∀ {x y z} → P y z → P x y → A

a : A
a = f _ reflP g

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
------------------------------------------------------------------------------
-- First-order logic theorems
------------------------------------------------------------------------------

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

module FOL.TheoremsI where

-- The theorems below are valid on intuitionistic logic and with an
-- empty domain.
open import FOL.Base hiding ( D≢∅ ; pem )

------------------------------------------------------------------------------
-- We postulate some formulae and propositional functions.
postulate
  A     : Set
  A¹ B¹ : D → Set
  A²    : D → D → Set

-- The introduction and elimination rules for the quantifiers are theorems.
{-
      φ(x)
  -----------  ∀-intro
    ∀x.φ(x)

    ∀x.φ(x)
  -----------  ∀-elim
     φ(t)

      φ(t)
  -----------  ∃-intro
    ∃x.φ(x)

   ∃x.φ(x)   φ(x) → ψ
 ----------------------  ∃-elim
           ψ
-}

∀-intro : ((x : D) → A¹ x) → ∀ x → A¹ x
∀-intro h = h

∀-intro' : ((x : D) → A¹ x) → ⋀ A¹
∀-intro' = dfun

∀-elim : (t : D) → (∀ x → A¹ x) → A¹ t
∀-elim t h = h t

∀-elim' : (t : D) → ⋀ A¹ → A¹ t
∀-elim' = dapp

∃-intro : (t : D) → A¹ t → ∃ A¹
∃-intro t A¹x = t , A¹x

∃-elim : ∃ A¹ → ((x : D) → A¹ x → A) → A
∃-elim (x , A¹x) h = h x A¹x

-- Generalization of De Morgan's laws.
gDM₂ : ¬ (∃ A¹) ↔ (∀ {x} → ¬ (A¹ x))
gDM₂ = l→r , r→l
  where
  l→r : ¬ (∃ A¹) → ∀ {x} → ¬ (A¹ x)
  l→r h A¹x = h (_ , A¹x)

  r→l : (∀ {x} → ¬ (A¹ x)) → ¬ (∃ A¹)
  r→l h (x , A¹x) = h A¹x

gDM₂' : ¬ (∃ A¹) ⇔ (⋀[ x ] ¬ (A¹ x))
gDM₂' = fun l→r , fun r→l
  where
  l→r : ¬ (∃ A¹) → ⋀[ x ] ¬ A¹ x
  l→r h = dfun (λ d A¹d → h (d , A¹d))

  r→l : ⋀[ x ] ¬ A¹ x → ¬ ∃ A¹
  r→l (dfun f) (x , A¹x) = f x A¹x

-- Quantification over a variable that does not occur can be erased or
-- added.
∃-erase-add : (∃[ x ] A ∧ A¹ x) ↔ A ∧ (∃[ x ] A¹ x)
∃-erase-add = l→r , r→l
  where
  l→r : ∃[ x ] A ∧ A¹ x → A ∧ (∃[ x ] A¹ x)
  l→r (x , a , A¹x) = a , x , A¹x

  r→l : A ∧ (∃[ x ] A¹ x) → ∃[ x ] A ∧ A¹ x
  r→l (a , x , A¹x) = x , a , A¹x

-- Interchange of quantifiers.
-- The related theorem ∀x∃y.Axy → ∃y∀x.Axy is not (classically) valid.
∃∀ : ∃[ x ] (∀ y → A² x y) → ∀ y → ∃[ x ] A² x y
∃∀ (x , h) y = x , h y

-- ∃ in terms of ∀ and ¬.
∃→¬∀¬ : ∃[ x ] A¹ x → ¬ (∀ {x} → ¬ A¹ x)
∃→¬∀¬ (_ , A¹x) h = h A¹x

∃¬→¬∀ : ∃[ x ] ¬ A¹ x → ¬ (∀ {x} → A¹ x)
∃¬→¬∀ (_ , h₁) h₂ = h₁ h₂

-- ∀ in terms of ∃ and ¬.
∀→¬∃¬ : (∀ {x} → A¹ x) → ¬ (∃[ x ] ¬ A¹ x)
∀→¬∃¬ h₁ (_ ,  h₂) = h₂ h₁

∀¬→¬∃ : (∀ {x} → ¬ A¹ x) → ¬ (∃[ x ] A¹ x)
∀¬→¬∃ h₁ (_ , h₂) = h₁ h₂

-- Distribution of ∃ and ∨.
∃∨ : ∃[ x ](A¹ x ∨ B¹ x) → (∃[ x ] A¹ x) ∨ (∃[ x ] B¹ x)
∃∨ (x , inj₁ A¹x) = inj₁ (x , A¹x)
∃∨ (x , inj₂ B¹x) = inj₂ (x , B¹x)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import Mockingbird.Forest using (Forest)

-- Birds Galore
module Mockingbird.Problems.Chapter11 {b ℓ} (forest : Forest {b} {ℓ}) where

open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃-syntax)
open import Data.Unit using (⊤; tt)
open import Function using (_$_)

import Mockingbird.Problems.Chapter09 forest as Chapter₉

open Forest forest

module Parentheses where
  private
    variable
      u v w x y z A A₁ A₂ B : Bird

  -- A variant of _∙_ that is not parsed as a right-associative operator, to
  -- make sure that the parentheses in the right-hand side of the exercises
  -- below are fully restored.
  infix 6 _∙′_
  _∙′_ = _∙_

  exercise-a : x ∙ y ∙ (z ∙ w ∙ y) ∙ v ≈ ((x ∙′ y) ∙′ ((z ∙′ w) ∙′ y)) ∙′ v
  exercise-a = refl

  exercise-b : (x ∙ y ∙ z) ∙ (w ∙ v ∙ x) ≈ ((x ∙′ y) ∙′ z) ∙′ ((w ∙′ v) ∙′ x)
  exercise-b = refl

  exercise-c : x ∙ y ∙ (z ∙ w ∙ v) ∙ (x ∙ z) ≈ ((x ∙′ y) ∙′ ((z ∙′ w) ∙′ v)) ∙′ (x ∙′ z)
  exercise-c = refl

  exercise-d : x ∙ y ∙ (z ∙ w ∙ v) ∙ x ∙ z ≈ (((x ∙′ y) ∙′ ((z ∙′ w) ∙′ v)) ∙′ x) ∙′ z
  exercise-d = refl

  exercise-e : x ∙ (y ∙ (z ∙ w ∙ v)) ∙ x ∙ z ≈ ((x ∙′ (y ∙′ ((z ∙′ w) ∙′ v))) ∙′ x) ∙′ z
  exercise-e = refl

  exercise-f : x ∙ y ∙ z ∙ (A ∙ B) ≈ (x ∙ y ∙ z) ∙ (A ∙ B)
  exercise-f = refl

  exercise-g : A₁ ≈ A₂ → B ∙ A₁ ≈ B ∙ A₂ × A₁ ∙ B ≈ A₂ ∙ B
  exercise-g A₁≈A₂ = (congˡ A₁≈A₂ , congʳ A₁≈A₂)

  exercise-h : x ∙ y ≈ z → x ∙ y ∙ w ≈ z ∙ w
  exercise-h {x} {y} {z} {w} xy≈z = begin
    x ∙ y ∙ w      ≈⟨⟩
    (x ∙′ y) ∙′ w  ≈⟨ congʳ xy≈z ⟩
    z ∙ w          ∎

  -- The other part of exercise h, wxy ≈ wz, does not follow in general.

open import Mockingbird.Forest.Birds forest

problem₁ : ⦃ _ : HasBluebird ⦄ → HasComposition
problem₁ = record
  { _∘_ = λ C D → B ∙ C ∙ D
  ; isComposition = λ C D x → begin
      B ∙ C ∙ D ∙ x  ≈⟨ isBluebird C D x ⟩
      C ∙ (D ∙ x)    ∎
  }

private
  instance
    hasComposition : ⦃ HasBluebird ⦄ → HasComposition
    hasComposition = problem₁

module _ ⦃ _ : HasBluebird ⦄ ⦃ _ : HasMockingbird ⦄ where
  problem₂ : ∀ x → ∃[ y ] x IsFondOf y
  problem₂ x =
    let (_ , isFond) = Chapter₉.problem₁ x

        shorten : M ∙ (B ∙ x ∙ M) ≈ B ∙ x ∙ M ∙ (B ∙ x ∙ M)
        shorten = isMockingbird (B ∙ x ∙ M)

    in (M ∙ (B ∙ x ∙ M) , trans (congˡ shorten) (trans isFond (sym shorten)))

  problem₃ : ∃[ x ] IsEgocentric x
  problem₃ =
    let (_ , isEgocentric) = Chapter₉.problem₂
    in (B ∙ M ∙ M ∙ (B ∙ M ∙ M) , isEgocentric)

module _ ⦃ _ : HasBluebird ⦄ ⦃ _ : HasMockingbird ⦄ ⦃ _ : HasKestrel ⦄ where
  problem₄ : ∃[ x ] IsHopelesslyEgocentric x
  problem₄ =
    let (_ , isHopelesslyEgocentric) = Chapter₉.problem₉
    in (B ∙ K ∙ M ∙ (B ∙ K ∙ M) , isHopelesslyEgocentric)

module _ ⦃ _ : HasBluebird ⦄ where
  problem₅ : HasDove
  problem₅ = record
    { D = B ∙ B
    ; isDove = λ x y z w → begin
        B ∙ B ∙ x ∙ y ∙ z ∙ w  ≈⟨ congʳ $ congʳ $ isBluebird B x y ⟩
        B ∙ (x ∙ y) ∙ z ∙ w    ≈⟨ isBluebird (x ∙ y) z w ⟩
        x ∙ y ∙ (z ∙ w)        ∎
    }

  private instance hasDove = problem₅

  problem₆ : HasBlackbird
  problem₆ = record
    { B₁ = B ∙ B ∙ B
    ; isBlackbird = λ x y z w → begin
        B ∙ B ∙ B ∙ x ∙ y ∙ z ∙ w  ≈⟨ congʳ $ congʳ $ congʳ (isBluebird B B x) ⟩
        B ∙ (B ∙ x) ∙ y ∙ z ∙ w    ≈⟨ congʳ (isBluebird (B ∙ x) y z) ⟩
        B ∙ x ∙ (y ∙ z) ∙ w        ≈⟨ isBluebird x (y ∙ z) w ⟩
        x ∙ (y ∙ z ∙ w)            ∎
    }

  private instance hasBlackbird = problem₆

  problem₇ : HasEagle
  problem₇ = record
    { E = B ∙ B₁
    ; isEagle = λ x y z w v → begin
        B ∙ B₁ ∙ x ∙ y ∙ z ∙ w ∙ v  ≈⟨ congʳ $ congʳ $ congʳ $ isBluebird B₁ x y ⟩
        B₁ ∙ (x ∙ y) ∙ z ∙ w ∙ v    ≈⟨ isBlackbird (x ∙ y) z w v ⟩
        x ∙ y ∙ (z ∙ w ∙ v)         ∎
    }

  private instance hasEagle = problem₇

  problem₈ : HasBunting
  problem₈ = record
    { B₂ = B ∙ B ∙ B₁
    ; isBunting = λ x y z w v → begin
        B ∙ B ∙ B₁ ∙ x ∙ y ∙ z ∙ w ∙ v  ≈⟨ congʳ $ congʳ $ congʳ $ congʳ $ isBluebird B B₁ x ⟩
        B ∙ (B₁ ∙ x) ∙ y ∙ z ∙ w ∙ v    ≈⟨ congʳ $ congʳ $ isBluebird (B₁ ∙ x) y z ⟩
        B₁ ∙ x ∙ (y ∙ z) ∙ w ∙ v        ≈⟨ isBlackbird x (y ∙ z) w v ⟩
        x ∙ (y ∙ z ∙ w ∙ v)             ∎
    }

  private instance hasBunting = problem₈

  problem₉ : HasDickcissel
  problem₉ = record
    { D₁ = B ∙ D
    ; isDickcissel = λ x y z w v → begin
        B ∙ D ∙ x ∙ y ∙ z ∙ w ∙ v  ≈⟨ congʳ $ congʳ $ congʳ $ isBluebird D x y ⟩
        D ∙ (x ∙ y) ∙ z ∙ w ∙ v    ≈⟨ isDove (x ∙ y) z w v ⟩
        x ∙ y ∙ z ∙ (w ∙ v)        ∎
    }

  private instance hasDickcissel = problem₉

  problem₁₀ : HasBecard
  problem₁₀ = record
    { B₃ = B ∙ D ∙ B
    ; isBecard = λ x y z w → begin
        B ∙ D ∙ B ∙ x ∙ y ∙ z ∙ w  ≈⟨ congʳ $ congʳ $ congʳ $ isBluebird D B x ⟩
        D ∙ (B ∙ x) ∙ y ∙ z ∙ w    ≈⟨ isDove (B ∙ x) y z w ⟩
        B ∙ x ∙ y ∙ (z ∙ w)        ≈⟨ isBluebird x y (z ∙ w) ⟩
        x ∙ (y ∙ (z ∙ w))          ∎
    }

  private instance hasBecard = problem₁₀

  problem₁₁ : HasDovekie
  problem₁₁ = record
    { D₂ = D ∙ D
    ; isDovekie = λ x y z w v → begin
        D ∙ D ∙ x ∙ y ∙ z ∙ w ∙ v  ≈⟨ congʳ $ congʳ $ isDove D x y z ⟩
        D ∙ x ∙ (y ∙ z) ∙ w ∙ v    ≈⟨ isDove x (y ∙ z) w v ⟩
        x ∙ (y ∙ z) ∙ (w ∙ v)      ∎
    }

  private instance hasDovekie = problem₁₁

  problem₁₂ : HasBaldEagle
  problem₁₂ = record
    { Ê = E ∙ E
    ; isBaldEagle = λ x y₁ y₂ y₃ z₁ z₂ z₃ → begin
        E ∙ E ∙ x ∙ y₁ ∙ y₂ ∙ y₃ ∙ z₁ ∙ z₂ ∙ z₃  ≈⟨ congʳ $ congʳ $ congʳ $ isEagle E x y₁ y₂ y₃ ⟩
        E ∙ x ∙ (y₁ ∙ y₂ ∙ y₃) ∙ z₁ ∙ z₂ ∙ z₃    ≈⟨ isEagle x (y₁ ∙ y₂ ∙ y₃) z₁ z₂ z₃ ⟩
        x ∙ (y₁ ∙ y₂ ∙ y₃) ∙ (z₁ ∙ z₂ ∙ z₃)      ∎
    }

  private instance hasBaldEagle = problem₁₂

problem₁₄ : ⦃ _ : HasWarbler ⦄ ⦃ _ : HasIdentity ⦄ → HasMockingbird
problem₁₄ = record
  { M = W ∙ I
  ; isMockingbird = λ x → begin
      W ∙ I ∙ x  ≈⟨ isWarbler I x ⟩
      I ∙ x ∙ x  ≈⟨ congʳ $ isIdentity x ⟩
      x ∙ x      ∎
  }

problem₁₅ : ⦃ _ : HasWarbler ⦄ ⦃ _ : HasKestrel ⦄ → HasIdentity
problem₁₅ = record
  { I = W ∙ K
  ; isIdentity = λ x → begin
      W ∙ K ∙ x  ≈⟨ isWarbler K x ⟩
      K ∙ x ∙ x  ≈⟨ isKestrel x x ⟩
      x          ∎
  }

problem₁₃ : ⦃ _ : HasWarbler ⦄ ⦃ _ : HasKestrel ⦄ → HasMockingbird
problem₁₃ = problem₁₄
  where instance _ = problem₁₅

problem₁₆ : ⦃ _ : HasCardinal ⦄ ⦃ _ : HasKestrel ⦄ → HasIdentity
problem₁₆ = record
  { I = C ∙ K ∙ K
  ; isIdentity = λ x → begin
      C ∙ K ∙ K ∙ x  ≈⟨ isCardinal K K x ⟩
      K ∙ x ∙ K      ≈⟨ isKestrel x K ⟩
      x              ∎
  }

problem₁₇ : ⦃ _ : HasCardinal ⦄ ⦃ _ : HasIdentity ⦄ → HasThrush
problem₁₇ = record
  { T = C ∙ I
  ; isThrush = λ x y → begin
      C ∙ I ∙ x ∙ y  ≈⟨ isCardinal I x y ⟩
      I ∙ y ∙ x      ≈⟨ congʳ $ isIdentity y ⟩
      y ∙ x          ∎
  }

problem₁₈ : ⦃ _ : HasThrush ⦄ → (∀ x → IsNormal x) → ∃[ A ] (∀ x → Commute A x)
problem₁₈ isNormal =
  let (A , isFond) = isNormal T

      commute : ∀ x → Commute A x
      commute x = begin
        A ∙ x      ≈˘⟨ (congʳ $ isFond) ⟩
        T ∙ A ∙ x  ≈⟨ isThrush A x ⟩
        x ∙ A      ∎

  in (A , commute)

problem₁₉ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasThrush ⦄ ⦃ _ : HasMockingbird ⦄ → ∃[ x ] (∀ y → Commute x y)
problem₁₉ = problem₁₈ problem₂

problem₂₀ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasThrush ⦄ → HasRobin
problem₂₀ = record
  { R = B ∙ B ∙ T
  ; isRobin = λ x y z → begin
      B ∙ B ∙ T ∙ x ∙ y ∙ z  ≈⟨ congʳ $ congʳ $ isBluebird B T x ⟩
      B ∙ (T ∙ x) ∙ y ∙ z    ≈⟨ isBluebird (T ∙ x) y z ⟩
      T ∙ x ∙ (y ∙ z)        ≈⟨ isThrush x (y ∙ z) ⟩
      (y ∙ z) ∙ x            ≈⟨⟩
      y ∙ z ∙ x              ∎
  }

problem₂₁ : ⦃ _ : HasRobin ⦄ → HasCardinal
problem₂₁ = record
  { C = R ∙ R ∙ R
  ; isCardinal = λ x y z → begin
      R ∙ R ∙ R ∙ x ∙ y ∙ z  ≈⟨ congʳ $ congʳ $ isRobin R R x ⟩
      R ∙ x ∙ R ∙ y ∙ z      ≈⟨ congʳ $ isRobin x R y ⟩
      R ∙ y ∙ x ∙ z          ≈⟨ isRobin y x z ⟩
      x ∙ z ∙ y              ∎
  }

problem₂₁′ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasThrush ⦄ → HasCardinal
problem₂₁′ = problem₂₁ ⦃ problem₂₀ ⦄

problem₂₁-bonus : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasThrush ⦄ → HasCardinal
problem₂₁-bonus = record
  { C = B ∙ (T ∙ (B ∙ B ∙ T)) ∙ (B ∙ B ∙ T)
  ; isCardinal = λ x y z → begin
      B ∙ (T ∙ (B ∙ B ∙ T)) ∙ (B ∙ B ∙ T) ∙ x ∙ y ∙ z    ≈˘⟨ congʳ $ congʳ $ congʳ $ congʳ $ isBluebird B T (B ∙ B ∙ T) ⟩
      B ∙ B ∙ T ∙ (B ∙ B ∙ T) ∙ (B ∙ B ∙ T) ∙ x ∙ y ∙ z  ≈⟨ isCardinal x y z ⟩
      x ∙ z ∙ y                                          ∎
  } where instance hasCardinal = problem₂₁′

module _ ⦃ _ : HasBluebird ⦄ ⦃ _ : HasThrush ⦄ where
  private
    instance hasRobin = problem₂₀
    instance hasCardinal = problem₂₁′

  problem₂₂-a : ∀ x → C ∙ x ≈ R ∙ x ∙ R
  problem₂₂-a x = begin
    C ∙ x          ≈⟨⟩
    R ∙ R ∙ R ∙ x  ≈⟨ isRobin R R x ⟩
    R ∙ x ∙ R      ∎

  problem₂₂-b : ∀ x → C ∙ x ≈ B ∙ (T ∙ x) ∙ R
  problem₂₂-b x = begin
    C ∙ x              ≈⟨ problem₂₂-a x ⟩
    R ∙ x ∙ R          ≈⟨⟩
    B ∙ B ∙ T ∙ x ∙ R  ≈⟨ congʳ $ isBluebird B T x ⟩
    B ∙ (T ∙ x) ∙ R    ∎

problem₂₃ : ⦃ _ : HasCardinal ⦄ → HasRobin
problem₂₃ = record
  { R = C ∙ C
  ; isRobin = λ x y z → begin
      C ∙ C ∙ x ∙ y ∙ z  ≈⟨ congʳ $ isCardinal C x y ⟩
      C ∙ y ∙ x ∙ z      ≈⟨ isCardinal y x z ⟩
      y ∙ z ∙ x          ∎
  }

problem₂₄ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasRobin ⦄ ⦃ _ : HasCardinal ⦄ → HasFinch
problem₂₄ = record
  { F = B ∙ C ∙ R
  ; isFinch = λ x y z → begin
      B ∙ C ∙ R ∙ x ∙ y ∙ z  ≈⟨ congʳ $ congʳ $ isBluebird C R x ⟩
      C ∙ (R ∙ x) ∙ y ∙ z    ≈⟨ isCardinal (R ∙ x) y z ⟩
      R ∙ x ∙ z ∙ y          ≈⟨ isRobin x z y ⟩
      z ∙ y ∙ x              ∎
  }

problem₂₅ : ⦃ _ : HasThrush ⦄ ⦃ _ : HasEagle ⦄ → HasFinch
problem₂₅ = record
  { F = E ∙ T ∙ T ∙ E ∙ T
  ; isFinch = λ x y z → begin
      E ∙ T ∙ T ∙ E ∙ T ∙ x ∙ y ∙ z  ≈⟨ congʳ $ congʳ $ isEagle T T E T x ⟩
      T ∙ T ∙ (E ∙ T ∙ x) ∙ y ∙ z    ≈⟨ congʳ $ congʳ $ isThrush T (E ∙ T ∙ x) ⟩
      E ∙ T ∙ x ∙ T ∙ y ∙ z          ≈⟨ isEagle T x T y z ⟩
      T ∙ x ∙ (T ∙ y ∙ z)            ≈⟨ isThrush x (T ∙ y ∙ z) ⟩
      T ∙ y ∙ z ∙ x                  ≈⟨ congʳ $ isThrush y z ⟩
      z ∙ y ∙ x                      ∎
  }

problem₂₆ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasThrush ⦄ → HasFinch
problem₂₆ = record
  { F = short
  ; isFinch = shortIsFinch
  }
  where
    instance
      hasRobin = problem₂₀
      hasCardinal = problem₂₁-bonus
      hasEagle = problem₇

    long : Bird
    long = (B ∙ (B ∙ (T ∙ (B ∙ B ∙ T)) ∙ (B ∙ B ∙ T)) ∙ (B ∙ B ∙ T))

    longIsFinch : IsFinch long
    longIsFinch = HasFinch.isFinch problem₂₄

    short : Bird
    short = B ∙ (T ∙ T) ∙ (B ∙ (B ∙ B ∙ B) ∙ T)

    short≈ETTET : short ≈ E ∙ T ∙ T ∙ E ∙ T
    short≈ETTET = begin
      short                                            ≈⟨⟩
      B ∙ (T ∙ T) ∙ (B ∙ (B ∙ B ∙ B) ∙ T)              ≈˘⟨ isBluebird (B ∙ (T ∙ T)) (B ∙ (B ∙ B ∙ B)) T ⟩
      B ∙ (B ∙ (T ∙ T)) ∙ (B ∙ (B ∙ B ∙ B)) ∙ T        ≈˘⟨ congʳ $ congʳ $ isBluebird B B (T ∙ T) ⟩
      B ∙ B ∙ B ∙ (T ∙ T) ∙ (B ∙ (B ∙ B ∙ B)) ∙ T      ≈˘⟨ congʳ $ congʳ $ isBluebird (B ∙ B ∙ B) T T ⟩
      B ∙ (B ∙ B ∙ B) ∙ T ∙ T ∙ (B ∙ (B ∙ B ∙ B)) ∙ T  ≈⟨⟩
      E ∙ T ∙ T ∙ E ∙ T                                ∎

    shortIsFinch : IsFinch short
    shortIsFinch x y z = begin
      short ∙ x ∙ y ∙ z              ≈⟨ congʳ $ congʳ $ congʳ $ short≈ETTET ⟩
      E ∙ T ∙ T ∙ E ∙ T ∙ x ∙ y ∙ z  ≈⟨ HasFinch.isFinch problem₂₅ x y z ⟩
      z ∙ y ∙ x                      ∎

problem₂₇ : ⦃ _ : HasCardinal ⦄ ⦃ _ : HasFinch ⦄ → HasVireo
problem₂₇ = record
  { V = C ∙ F
  ; isVireo = λ x y z → begin
      C ∙ F ∙ x ∙ y ∙ z  ≈⟨ congʳ $ isCardinal F x y ⟩
      F ∙ y ∙ x ∙ z      ≈⟨ isFinch y x z ⟩
      z ∙ x ∙ y          ∎
  }

problem₂₈ : ⦃ _ : HasFinch ⦄ ⦃ _ : HasRobin ⦄ → HasVireo
problem₂₈ = record
  { V = R ∙ F ∙ R
  ; isVireo = λ x y z → begin
      R ∙ F ∙ R ∙ x ∙ y ∙ z      ≈˘⟨ congʳ $ congʳ $ congʳ $ isRobin R R F ⟩
      R ∙ R ∙ R ∙ F ∙ x ∙ y ∙ z  ≈⟨ congʳ $ HasCardinal.isCardinal problem₂₁ F x y ⟩
      F ∙ y ∙ x ∙ z              ≈⟨ isFinch y x z ⟩
      z ∙ x ∙ y                  ∎
  }

problem₂₉ : ⦃ _ : HasCardinal ⦄ ⦃ _ : HasVireo ⦄ → HasFinch
problem₂₉ = record
  { F = C ∙ V
  ; isFinch = λ x y z → begin
      C ∙ V ∙ x ∙ y ∙ z  ≈⟨ congʳ $ isCardinal V x y ⟩
      V ∙ y ∙ x ∙ z      ≈⟨ isVireo y x z ⟩
      z ∙ y ∙ x          ∎
  }

problem₃₀ : ⦃ _ : HasRobin ⦄ ⦃ _ : HasKestrel ⦄ → HasIdentity
problem₃₀ = problem₁₆
  where instance hasCardinal = problem₂₁

module _ ⦃ _ : HasBluebird ⦄ ⦃ _ : HasCardinal ⦄ where
  problem₃₁ : HasCardinalOnceRemoved
  problem₃₁ = record
    { C* = B ∙ C
    ; isCardinalOnceRemoved = λ x y z w → begin
        B ∙ C ∙ x ∙ y ∙ z ∙ w  ≈⟨ congʳ $ congʳ $ isBluebird C x y ⟩
        C ∙ (x ∙ y) ∙ z ∙ w    ≈⟨ isCardinal (x ∙ y) z w ⟩
        x ∙ y ∙ w ∙ z          ∎
    }

  private instance hasCardinalOnceRemoved = problem₃₁

  problem₃₂ : HasRobinOnceRemoved
  problem₃₂ = record
    { R* = C* ∙ C*
    ; isRobinOnceRemoved = λ x y z w → begin
        C* ∙ C* ∙ x ∙ y ∙ z ∙ w  ≈⟨ congʳ $ isCardinalOnceRemoved C* x y z ⟩
        C* ∙ x ∙ z ∙ y ∙ w       ≈⟨ isCardinalOnceRemoved x z y w ⟩
        x ∙ z ∙ w ∙ y            ∎
    }

  private instance hasRobinOnceRemoved = problem₃₂

  problem₃₃ : HasFinchOnceRemoved
  problem₃₃ = record
    { F* = B ∙ C* ∙ R*
    ; isFinchOnceRemoved = λ x y z w → begin
        B ∙ C* ∙ R* ∙ x ∙ y ∙ z ∙ w  ≈⟨ congʳ $ congʳ $ congʳ $ isBluebird C* R* x ⟩
        C* ∙ (R* ∙ x) ∙ y ∙ z ∙ w    ≈⟨ isCardinalOnceRemoved (R* ∙ x) y z w ⟩
        R* ∙ x ∙ y ∙ w ∙ z           ≈⟨ isRobinOnceRemoved x y w z ⟩
        x ∙ w ∙ z ∙ y                ∎
    }

  private instance hasFinchOnceRemoved = problem₃₃

  problem₃₄ : HasVireoOnceRemoved
  problem₃₄ = record
    { V* = C* ∙ F*
    ; isVireoOnceRemoved = λ x y z w → begin
        C* ∙ F* ∙ x ∙ y ∙ z ∙ w  ≈⟨ congʳ $ isCardinalOnceRemoved F* x y z ⟩
        F* ∙ x ∙ z ∙ y ∙ w       ≈⟨ isFinchOnceRemoved x z y w ⟩
        x ∙ w ∙ y ∙ z            ∎
    }

  private instance hasVireoOnceRemoved = problem₃₄

  problem₃₅-C** : HasCardinalTwiceRemoved
  problem₃₅-C** = record
    { C** = B ∙ C*
    ; isCardinalTwiceRemoved = λ x y z₁ z₂ z₃ → begin
        B ∙ C* ∙ x ∙ y ∙ z₁ ∙ z₂ ∙ z₃  ≈⟨ congʳ $ congʳ $ congʳ $ isBluebird C* x y ⟩
        C* ∙ (x ∙ y) ∙ z₁ ∙ z₂ ∙ z₃    ≈⟨ isCardinalOnceRemoved (x ∙ y) z₁ z₂ z₃ ⟩
        x ∙ y ∙ z₁ ∙ z₃ ∙ z₂           ∎
    }

  problem₃₅-R** : HasRobinTwiceRemoved
  problem₃₅-R** = record
    { R** = B ∙ R*
    ; isRobinTwiceRemoved = λ x y z₁ z₂ z₃ → begin
        B ∙ R* ∙ x ∙ y ∙ z₁ ∙ z₂ ∙ z₃  ≈⟨ congʳ $ congʳ $ congʳ $ isBluebird R* x y ⟩
        R* ∙ (x ∙ y) ∙ z₁ ∙ z₂ ∙ z₃    ≈⟨ isRobinOnceRemoved (x ∙ y) z₁ z₂ z₃ ⟩
        x ∙ y ∙ z₂ ∙ z₃ ∙ z₁           ∎
    }

  problem₃₅-F** : HasFinchTwiceRemoved
  problem₃₅-F** = record
    { F** = B ∙ F*
    ; isFinchTwiceRemoved = λ x y z₁ z₂ z₃ → begin
        B ∙ F* ∙ x ∙ y ∙ z₁ ∙ z₂ ∙ z₃  ≈⟨ congʳ $ congʳ $ congʳ $ isBluebird F* x y ⟩
        F* ∙ (x ∙ y) ∙ z₁ ∙ z₂ ∙ z₃    ≈⟨ isFinchOnceRemoved (x ∙ y) z₁ z₂ z₃ ⟩
        x ∙ y ∙ z₃ ∙ z₂ ∙ z₁           ∎
    }

  problem₃₅-V** : HasVireoTwiceRemoved
  problem₃₅-V** = record
    { V** = B ∙ V*
    ; isVireoTwiceRemoved = λ x y z₁ z₂ z₃ → begin
        B ∙ V* ∙ x ∙ y ∙ z₁ ∙ z₂ ∙ z₃  ≈⟨ congʳ $ congʳ $ congʳ $ isBluebird V* x y ⟩
        V* ∙ (x ∙ y) ∙ z₁ ∙ z₂ ∙ z₃    ≈⟨ isVireoOnceRemoved (x ∙ y) z₁ z₂ z₃ ⟩
        x ∙ y ∙ z₃ ∙ z₁ ∙ z₂           ∎
    }

problem₃₆ : ⦃ _ : HasCardinalOnceRemoved ⦄ ⦃ _ : HasThrush ⦄ → HasVireo
problem₃₆ = record
  { V = C* ∙ T
  ; isVireo = λ x y z → begin
      C* ∙ T ∙ x ∙ y ∙ z  ≈⟨ isCardinalOnceRemoved T x y z ⟩
      T ∙ x ∙ z ∙ y       ≈⟨ congʳ $ isThrush x z ⟩
      z ∙ x ∙ y           ∎
  }

problem₃₇′ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasCardinal ⦄ → HasQueerBird
problem₃₇′ = record
  { Q = C ∙ B
  ; isQueerBird = λ x y z → begin
      C ∙ B ∙ x ∙ y ∙ z  ≈⟨ congʳ $ isCardinal B x y ⟩
      B ∙ y ∙ x ∙ z      ≈⟨ isBluebird y x z ⟩
      y ∙ (x ∙ z)        ∎
  }

problem₃₈′ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasCardinalOnceRemoved ⦄ → HasQuixoticBird
problem₃₈′ = record
  { Q₁ = C* ∙ B
  ; isQuixoticBird = λ x y z → begin
      C* ∙ B ∙ x ∙ y ∙ z  ≈⟨ isCardinalOnceRemoved B x y z ⟩
      B ∙ x ∙ z ∙ y       ≈⟨ isBluebird x z y ⟩
      x ∙ (z ∙ y)         ∎
  }

problem₃₉′-F* : ⦃ _ : HasFinchOnceRemoved ⦄ ⦃ _ : HasQueerBird ⦄ → HasQuizzicalBird
problem₃₉′-F* = record
  { Q₂ = F* ∙ Q
  ; isQuizzicalBird = λ x y z → begin
      F* ∙ Q ∙ x ∙ y ∙ z  ≈⟨ isFinchOnceRemoved Q x y z ⟩
      Q ∙ z ∙ y ∙ x       ≈⟨ isQueerBird z y x ⟩
      y ∙ (z ∙ x)         ∎
  }

problem₃₉′-R* : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasRobinOnceRemoved ⦄ → HasQuizzicalBird
problem₃₉′-R* = record
  { Q₂ = R* ∙ B
  ; isQuizzicalBird = λ x y z → begin
      R* ∙ B ∙ x ∙ y ∙ z  ≈⟨ isRobinOnceRemoved B x y z ⟩
      B ∙ y ∙ z ∙ x       ≈⟨ isBluebird y z x ⟩
      y ∙ (z ∙ x)         ∎
  }

problem₄₁′ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasVireoOnceRemoved ⦄ → HasQuirkyBird
problem₄₁′ = record
  { Q₃ = V* ∙ B
  ; isQuirkyBird = λ x y z → begin
      V* ∙ B ∙ x ∙ y ∙ z  ≈⟨ isVireoOnceRemoved B x y z ⟩
      B ∙ z ∙ x ∙ y       ≈⟨ isBluebird z x y ⟩
      z ∙ (x ∙ y)         ∎
  }

problem₄₂′ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasFinchOnceRemoved ⦄ → HasQuackyBird
problem₄₂′ = record
  { Q₄ = F* ∙ B
  ; isQuackyBird = λ x y z → begin
      F* ∙ B ∙ x ∙ y ∙ z  ≈⟨ isFinchOnceRemoved B x y z ⟩
      B ∙ z ∙ y ∙ x       ≈⟨ isBluebird z y x ⟩
      z ∙ (y ∙ x)         ∎
  }

module _ ⦃ _ : HasBluebird ⦄ ⦃ _ : HasThrush ⦄ where
  private
    instance
      hasCardinal = problem₂₁-bonus
      hasCardinalOnceRemoved = problem₃₁
      hasRobinOnceRemoved = problem₃₂
      hasFinchOnceRemoved = problem₃₃
      hasVireoOnceRemoved = problem₃₄

  problem₃₇ : HasQueerBird
  problem₃₇ = problem₃₇′

  private instance hasQueerBird = problem₃₇

  problem₃₈ : HasQuixoticBird
  problem₃₈ = problem₃₈′

  private instance hasQuixoticBird = problem₃₈

  problem₃₉-F* : HasQuizzicalBird
  problem₃₉-F* = problem₃₉′-F*

  problem₃₉-R* : HasQuizzicalBird
  problem₃₉-R* = problem₃₉′-R*

  private instance hasQuizzicalBird = problem₃₉-F*

  problem₄₁ : HasQuirkyBird
  problem₄₁ = problem₄₁′

  problem₄₂ : HasQuackyBird
  problem₄₂ = problem₄₂′

module _ ⦃ _ : HasCardinal ⦄ where
  problem₄₀-Q₁ : ⦃ _ : HasQuizzicalBird ⦄ → HasQuixoticBird
  problem₄₀-Q₁ = record
    { Q₁ = C ∙ Q₂
    ; isQuixoticBird = λ x y z → begin
        C ∙ Q₂ ∙ x ∙ y ∙ z  ≈⟨ congʳ $ isCardinal Q₂ x y ⟩
        Q₂ ∙ y ∙ x ∙ z      ≈⟨ isQuizzicalBird y x z ⟩
        x ∙ (z ∙ y)         ∎
    }

  problem₄₀-Q₂ : ⦃ _ : HasQuixoticBird ⦄ → HasQuizzicalBird
  problem₄₀-Q₂ = record
    { Q₂ = C ∙ Q₁
    ; isQuizzicalBird = λ x y z → begin
        C ∙ Q₁ ∙ x ∙ y ∙ z  ≈⟨ congʳ $ isCardinal Q₁ x y ⟩
        Q₁ ∙ y ∙ x ∙ z      ≈⟨ isQuixoticBird y x z ⟩
        y ∙ (z ∙ x)         ∎
    }

  problem₄₃-Q₃ : ⦃ _ : HasQuackyBird ⦄ → HasQuirkyBird
  problem₄₃-Q₃ = record
    { Q₃ = C ∙ Q₄
    ; isQuirkyBird = λ x y z → begin
        C ∙ Q₄ ∙ x ∙ y ∙ z  ≈⟨ congʳ $ isCardinal Q₄ x y ⟩
        Q₄ ∙ y ∙ x ∙ z      ≈⟨ isQuackyBird y x z ⟩
        z ∙ (x ∙ y)         ∎
    }

  problem₄₃-Q₄ : ⦃ _ : HasQuirkyBird ⦄ → HasQuackyBird
  problem₄₃-Q₄ = record
    { Q₄ = C ∙ Q₃
    ; isQuackyBird = λ x y z → begin
        C ∙ Q₃ ∙ x ∙ y ∙ z  ≈⟨ congʳ $ isCardinal Q₃ x y ⟩
        Q₃ ∙ y ∙ x ∙ z      ≈⟨ isQuirkyBird y x z ⟩
        z ∙ (y ∙ x)         ∎
    }

problem₄₄ : ⦃ _ : HasQuixoticBird ⦄ ⦃ _ : HasThrush ⦄ → HasQuackyBird
problem₄₄ = record
  { Q₄ = Q₁ ∙ T
  ; isQuackyBird = λ x y z → begin
      Q₁ ∙ T ∙ x ∙ y ∙ z  ≈⟨ congʳ $ isQuixoticBird T x y ⟩
      T ∙ (y ∙ x) ∙ z     ≈⟨ isThrush (y ∙ x) z ⟩
      z ∙ (y ∙ x)         ∎
  }

problem₄₅ : ⦃ _ : HasQueerBird ⦄ ⦃ _ : HasThrush ⦄ → HasBluebird
problem₄₅ = record
  { B = Q ∙ T ∙ (Q ∙ Q)
  ; isBluebird = λ x y z → begin
      Q ∙ T ∙ (Q ∙ Q) ∙ x ∙ y ∙ z  ≈⟨ congʳ $ congʳ $ isQueerBird T (Q ∙ Q) x ⟩
      Q ∙ Q ∙ (T ∙ x) ∙ y ∙ z      ≈⟨ congʳ $ isQueerBird Q (T ∙ x) y ⟩
      T ∙ x ∙ (Q ∙ y) ∙ z          ≈⟨ congʳ $ isThrush x (Q ∙ y) ⟩
      Q ∙ y ∙ x ∙ z                ≈⟨ isQueerBird y x z ⟩
      x ∙ (y ∙ z)                  ∎
  }

problem₄₆ : ⦃ _ : HasQueerBird ⦄ ⦃ _ : HasThrush ⦄ → HasCardinal
problem₄₆ = record
  { C = Q ∙ Q ∙ (Q ∙ T)
  ; isCardinal = λ x y z → begin
      Q ∙ Q ∙ (Q ∙ T) ∙ x ∙ y ∙ z  ≈⟨ congʳ $ congʳ $ isQueerBird Q (Q ∙ T) x ⟩
      Q ∙ T ∙ (Q ∙ x) ∙ y ∙ z      ≈⟨ congʳ $ isQueerBird T (Q ∙ x) y ⟩
      Q ∙ x ∙ (T ∙ y) ∙ z          ≈⟨ isQueerBird x (T ∙ y) z ⟩
      T ∙ y ∙ (x ∙ z)              ≈⟨ isThrush y (x ∙ z) ⟩
      x ∙ z ∙ y                    ∎
  }

problem₄₇ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasThrush ⦄ → HasGoldfinch
problem₄₇ = record
  { G = D ∙ C
  ; isGoldfinch = λ x y z w → begin
      D ∙ C ∙ x ∙ y ∙ z ∙ w  ≈⟨ congʳ $ isDove C x y z ⟩
      C ∙ x ∙ (y ∙ z) ∙ w    ≈⟨ isCardinal x (y ∙ z) w ⟩
      x ∙ w ∙ (y ∙ z)        ∎
  } where
  instance
    hasCardinal = problem₂₁-bonus
    hasDove = problem₅

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic