text:
------------------------------------------------------------------------
-- An example that uses natural numbers as names, implemented using
-- the coinductive definition of bisimilarity
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

module Bisimilarity.CCS.Examples.Natural-numbers where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude
open import Prelude.Size

open import Bijection equality-with-J using (_↔_)
open import Equality.Decision-procedures equality-with-J
open import Fin equality-with-J
open import Function-universe equality-with-J as F
  hiding (id; _∘_; Distinct↔≢)
open import Nat equality-with-J hiding (Distinct)

open import Bisimilarity.CCS
import Bisimilarity.Equational-reasoning-instances
open import Bisimilarity.CCS.Examples
open import Equational-reasoning
open import Labelled-transition-system.CCS ℕ

open import Bisimilarity CCS

module _ (μ : Action) where

  -- Two processes that are strongly bisimilar.

  P : ∀ {i} → ℕ → Proc i
  P n = Restricted n ∣ (μ · λ { .force → P (1 + n) })

  Q : ∀ {i} → Proc i
  Q = μ · λ { .force → Q }

  P∼Q : ∀ {i n} → [ i ] P n ∼ Q
  P∼Q {n = n} =
    P n    ∼⟨ Restricted∼∅ ∣-cong (refl ·-cong λ { .force → P∼Q }) ⟩
    ∅ ∣ Q  ∼⟨ ∣-left-identity ⟩■
    Q

  -- Q is not finite.

  Q-infinite : ¬ Finite Q
  Q-infinite (action f) = Q-infinite f

  -- However, Q is regular.

  Q-regular : Regular Q
  Q-regular = 1 , (λ _ → Q) , (fzero ,_) ∘ lemma
    where
    lemma : ∀ {P} → Subprocess P Q → Equal ∞ P Q
    lemma (refl eq)    = eq
    lemma (action sub) = lemma sub

  -- The processes in the family P are not finite.

  P-infinite : ∀ {n} → ¬ Finite (P n)
  P-infinite (_ ∣ action f) = P-infinite f

  -- Furthermore they are irregular.

  P-irregular : ∀ {n} → ¬ Regular (P n)
  P-irregular (k , Qs , hyp) = irregular′ k hyp
    where
    Regular′ : ℕ → ∀ k → (Fin k → Proc ∞) → Type
    Regular′ n k Qs =
      ∀ {Q} → Subprocess Q (P n) →
        ∃ λ (i : Fin k) → Equal ∞ Q (Qs i)

    irregular′ : ∀ {n} k {Qs} → ¬ Regular′ n k Qs
    irregular′ {n} zero {Qs} =
      Regular′ n zero Qs        ↝⟨ _$ refl (Proc-refl _) ⟩
      (∃ λ (i : Fin zero) → _)  ↝⟨ proj₁ ⟩□
      ⊥                         □
    irregular′ {n} (suc k) {Qs} =
      Regular′ n (suc k) Qs               ↝⟨ lemma₂ ⟩
      (∃ λ Qs′ → Regular′ (suc n) k Qs′)  ↝⟨ irregular′ k ∘ proj₂ ⟩□
      ⊥                                   □
      where
      lemma₁ :
        ∀ {Q} m {n} → Subprocess Q (P (1 + m + n)) → ¬ Equal ∞ Q (P n)
      lemma₁ m (par-right (action sub)) eq = lemma₁ (suc m) sub eq

      lemma₁ m {n} (refl (⟨ν refl ⟩ _ ∣ _)) (⟨ν suc[m+n]≡n ⟩ _ ∣ _) =
        ≢1+ _ (n            ≡⟨ sym suc[m+n]≡n ⟩
               suc (m + n)  ≡⟨ cong suc (+-comm m) ⟩∎
               suc (n + m)  ∎)

      lemma₁ _ (par-left (refl ()))                        (_ ∣ _)
      lemma₁ _ (par-left (restriction (refl ())))          (_ ∣ _)
      lemma₁ _ (par-left (restriction (action (refl ())))) (_ ∣ _)
      lemma₁ _ (par-right (refl p)) q
        with Proc-trans (Proc-sym p) q
      ... | ()

      lemma₂ : ∀ {n k Qs} →
               Regular′ n (suc k) Qs →
               ∃ λ Qs′ → Regular′ (suc n) k Qs′
      lemma₂ {n} {k} {Qs} reg =
        let i , Pn≡Qsi = reg (refl (Proc-refl _))
            Fin↔       = Fin↔Fin+≢ i
            Qs′        =
              Fin k                                   ↔⟨ Fin↔ ⟩
              (∃ λ (j : Fin (suc k)) → Distinct j i)  ↝⟨ Qs ∘ proj₁ ⟩□
              Proc ∞                                  □
        in
        Qs′ , λ {Q} →
          Subprocess Q (P (1 + n))                                    ↝⟨ (λ sub → reg (par-right (action sub)) , lemma₁ 0 sub) ⟩

          (∃ λ (j : Fin (suc k)) → Equal ∞ Q (Qs j)) ×
          ¬ Equal ∞ Q (P n)                                           ↝⟨ (λ { ((j , Q≡Qsj) , Q≢Pn) →
                                                                                ( j
                                                                                , (case j Fin.≟ i of λ where
                                                                                (inj₁ refl) → ⊥-elim $
                                                                                Q≢Pn (Proc-trans Q≡Qsj (Proc-sym Pn≡Qsi))
                                                                                (inj₂ j≢i)  → _⇔_.from (Distinct↔≢ _) j≢i)
                                                                                )
                                                                              , Q≡Qsj }) ⟩
          (∃ λ (j : ∃ λ (j : Fin (suc k)) → Distinct j i) →
             Equal ∞ Q (Qs (proj₁ j)))                                ↝⟨ ∃-cong (λ _ → ≡⇒↝ _ $ cong (λ j → Equal ∞ Q (Qs (proj₁ j))) $ sym $
                                                                         _↔_.right-inverse-of Fin↔ _) ⟩
          (∃ λ (j : ∃ λ (j : Fin (suc k)) → Distinct j i) →
             Equal ∞ Q (Qs (proj₁ (_↔_.to Fin↔ (_↔_.from Fin↔ j)))))  ↔⟨⟩

          (∃ λ (j : ∃ λ (j : Fin (suc k)) → Distinct j i) →
             Equal ∞ Q (Qs′ (_↔_.from Fin↔ j)))                       ↝⟨ Σ-cong (inverse Fin↔) (λ _ → F.id) ⟩□

          (∃ λ (j : Fin k) → Equal ∞ Q (Qs′ j))                       □

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
import Relation.Binary.EqReasoning as EqReasoning
open import SemiNearRingRecords
module ZeroLemmas (snr : SemiNearRing) where
  open SemiNearRing snr -- public
  open import CommAssocLemmas s _≃s_ _+s_ zers isCommMon hiding (_<+>_) renaming (SA to Ss)

  zeroˡLemma : ∀ x y → zers *s x +s zers *s y ≃s zers
  zeroˡLemma x y = begin
         zers *s x +s zers *s y
       ≈⟨ zeroˡ x <+> zeroˡ y ⟩
         zers +s zers
       ≈⟨ identityˡs zers ⟩
         zers
       ∎
    where open EqReasoning Ss

  zeroʳLemma : ∀ x y →  x *s zers  +s  y *s zers   ≃s  zers
  zeroʳLemma x y =
       begin
           x *s zers  +s   y *s zers
       ≈⟨  zeroʳ x    <+>  zeroʳ y ⟩
         zers         +s   zers
       ≈⟨ identityˡs zers ⟩
         zers
       ∎
    where open EqReasoning Ss

  zeroˡʳLemma : ∀ w x y → w +s (zers *s x +s  y *s zers)  ≃s  w
  zeroˡʳLemma w x y = begin
        w +s (zers *s x  +s  y *s zers)
     ≈⟨ refls <+> (zeroˡ x <+> zeroʳ y) ⟩
        w +s (zers +s zers)
     ≈⟨ refls <+> identityˡs zers ⟩
        w +s zers
     ≈⟨ identityʳs w ⟩
        w
     ∎
     where open EqReasoning Ss

  -- Some lemmas are needed to eliminate the zers and massage the terms.
  zeroLemma01 = lemmaCommAssoc01

  zeroLemma10 : ∀ {a b c d e} →   a +s ( ((zers *s b) +s c) +s (d +s (e *s zers)))
                              ≃s  a +s                 ( c  +s  d )
  zeroLemma10 {a} {b} {c} {d} {e} = refls <+>
    (begin
       ((zers *s b) +s c)      +s (d      +s (e *s zers))
     ≈⟨ (zeroˡ   b <+> refls) <+> (refls <+>  zeroʳ e) ⟩
       ( zers       +s c)      +s (d      +s zers)
     ≈⟨ identityˡs c <+> identityʳs d ⟩
        c +s d
     ∎)
      where open EqReasoning Ss

  zeroLemma00 : ∀ {a b c d e} →   a +s ((c +s b) +s (d +s (e *s zers)) )
                             ≃s  (a +s b) +s (c  +s  d)
  zeroLemma00 {a} {b} {c} {d} {e} =
    (begin
       a       +s ((c +s b)   +s (d      +s (e *s zers)) )
     ≈⟨ refls <+> (comms c b <+> (refls <+> zeroʳ e)) ⟩
       a       +s ((b +s c)   +s (d      +s zers) )
     ≈⟨ refls <+> (refls <+> identityʳs d) ⟩
       a       +s ((b +s c)   +s d)
     ≈⟨ refls <+> assocs b c d ⟩
       a +s (b +s (c +s d))
     ≈⟨ syms (assocs a b _) ⟩
       (a +s b) +s (c +s d)
     ∎)
      where open EqReasoning Ss

  zeroLemma11 : ∀ {a b c d e} →   a +s (((zers *s e)  +s  c) +s (b +s d))
                             ≃s  (a +s b) +s (c +s  d)
  zeroLemma11 {a} {b} {c} {d} {e} =
    (begin
       a       +s (((zers *s e)  +s  c)     +s (b +s d))
     ≈⟨ refls <+> ((zeroˡ e     <+> refls) <+> refls) ⟩
       a       +s ((zers        +s  c)      +s (b +s d))
     ≈⟨ refls <+> (identityˡs c            <+> refls) ⟩
       a       +s (                 c       +s (b +s d))
     ≈⟨ refls <+> syms (assocs c b d) ⟩
       a       +s ((c +s b) +s d)
     ≈⟨ refls <+> (comms c b <+> refls) ⟩
       a       +s ((b +s c) +s d)
     ≈⟨ refls <+> (assocs _ _ _) ⟩
       a       +s (b +s (c +s d))
     ≈⟨ syms (assocs _ _ _) ⟩
       (a +s b) +s (c +s d)
     ∎)
      where open EqReasoning Ss

ext: agda

max_stars_repo_name: DSLsofMath/ValiantAgda

max_issues_repo_name: DSLsofMath/ValiantAgda

max_forks_repo_name: DSLsofMath/ValiantAgda


text:
module Data.Finitude.Exponent where
open import Data.Finitude
open import Data.Fin as Fin using (Fin; toℕ)
open import Data.Nat
open import Data.Vec as Vec
open import Relation.Binary.PropositionalEquality as P
open import Data.Nat.DivMod
open import Relation.Nullary.Decidable
open import Function
open import Function.Equality as F using (_⟶_; _⟨$⟩_; _⇨_)
open import Function.Inverse as Inv using (module Inverse; Inverse)
open import Data.Product
open import Data.Sum
open import Data.Empty
open import Relation.Binary

exponent : ∀ {m} {n} → Finitude (P.setoid (Vec (Fin m) n)) (m ^ n)
exponent {m} {n} = record {
    to = P.→-to-⟶ to
  ; from = P.→-to-⟶ from
  ; inverse-of = record {
      left-inverse-of = from∘to
    ; right-inverse-of = to∘from {m}{n}
    }
  }
  where
    open import Data.Nat.Properties
    open import Data.Fin.Properties hiding (≤-refl; _≟_; <-cmp)
    open import Relation.Nullary.Negation
    shift : ∀ {m n} (i : Fin m)(j : Fin n) → toℕ j + (toℕ i) * n < m * n
    shift {m}{n} i j =
              begin suc (toℕ j) + toℕ i * n
                ≤⟨ +-mono-≤ (toℕ<n j) (≤-refl {(toℕ i) * n}) ⟩
                  n + toℕ i * n
                ≤⟨ *-mono-≤ (toℕ<n i) ≤-refl ⟩ m * n ∎
          where
            open ≤-Reasoning
    to : ∀ {m n} → Vec (Fin m) n → Fin (m ^ n)
    to [] = Fin.zero
    to {m}{n = suc n} (i ∷ is) = Fin.fromℕ≤ (shift i (to is))

    suci^j≢0  : ∀ i j → suc i ^ j ≢ 0
    suci^j≢0 i j eq with i^j≡0⇒i≡0 _ j eq
    ... | ()

    from : ∀ {m n} → Fin (m ^ n) → Vec (Fin m) n
    from {m} {zero} i = []
    from {zero} {suc n} ()
    from {suc m} {suc n} i with ((toℕ i) divMod (suc m ^ n))
      {≢0 = fromWitnessFalse (suci^j≢0 _ n)}
    from {suc m} {suc n} i | result quotient remainder property
      = Fin.fromℕ≤ q<sm  ∷ from remainder
      where
        q<sm : quotient < suc m
        q<sm = ≰⇒> (λ sm≤q → <⇒≱ (toℕ<n i)
                (begin (suc m) * (suc m ^ n)
                   ≤⟨ *-mono-≤ sm≤q ≤-refl ⟩ quotient * (suc m ^ n)
                   ≤⟨ +-mono-≤ (z≤n {toℕ remainder}) ≤-refl ⟩ toℕ remainder + quotient * (suc m ^ n)
                   ≡⟨ P.sym property ⟩ toℕ i ∎))
              where
                open ≤-Reasoning
    ≢→<⊎> : ∀ {m n} → m ≢ n → m < n ⊎ n < m
    ≢→<⊎> {m}{n} m≢n  with <-cmp m n
    ≢→<⊎> {m} {n} m≢n | tri<  m<n _ _ = inj₁ m<n
    ≢→<⊎> {m} {n} m≢n | tri≈ _ m≡n _ = ⊥-elim (m≢n m≡n)
    ≢→<⊎> {m} {n} m≢n | tri> _ _ n<m = inj₂ n<m

    chn : ∀ m → ∀ {k₀ k₁} {r₀ r₁ : Fin m} → toℕ r₀ + k₀ * m  ≡ toℕ r₁ + k₁ * m → k₀ ≡ k₁ × r₀ ≡ r₁
    chn zero {k₀} {k₁} {()} {r₁} _
    chn (suc m) {k₀} {k₁} {r₀} {r₁} eq = k₀≡k₁ , r₀≡r₁
      where
        open ≤-Reasoning
        contra : k₀ ≢ k₁ → ⊥
        contra k₀≢k₁ with ≢→<⊎> k₀≢k₁
        ... | inj₁ k₀<k₁ = <⇒≱  (toℕ<n r₀) (+-cancelʳ-≤ (suc m) (toℕ r₀)
                                 (begin suc m + k₀ * suc m
                                   ≡⟨ refl ⟩ suc k₀ * suc m
                                   ≤⟨ *-mono-≤ (m≤m+n (suc k₀) (k₁ ∸ suc k₀)) (≤-refl {suc m}) ⟩
                                          (suc k₀ + (k₁ ∸ suc k₀)) * suc m
                                   ≡⟨ P.cong₂ _*_ (m+n∸m≡n k₀<k₁) refl ⟩ k₁ * suc m
                                   ≤⟨ n≤m+n (toℕ r₁) (k₁ * suc m)  ⟩ toℕ r₁ + k₁ * suc m
                                   ≡⟨ P.sym eq ⟩ toℕ r₀ + k₀ * suc m ∎))
        ... | inj₂ k₁<k₀ = <⇒≱  (toℕ<n r₁) (+-cancelʳ-≤  (suc m) (toℕ r₁)
                  (begin suc k₁ * suc m
                         ≤⟨ *-mono-≤ (m≤m+n (suc k₁) (k₀ ∸ suc k₁)) (≤-refl {suc m}) ⟩
                         (suc k₁ + (k₀ ∸ suc k₁)) * suc m
                         ≡⟨ P.cong₂ _*_ (m+n∸m≡n k₁<k₀) refl ⟩ k₀ * suc m
                         ≤⟨ n≤m+n  (toℕ r₀) (k₀ * suc m) ⟩ toℕ r₀ + k₀ * suc m
                         ≡⟨ eq ⟩ toℕ r₁ + k₁ * suc m  ∎ ))
        k₀≡k₁ : k₀ ≡ k₁
        k₀≡k₁ = decidable-stable (k₀ ≟ k₁) contra

        r₀≡r₁ : r₀ ≡ r₁
        r₀≡r₁ = toℕ-injective (+-cancelʳ-≡ (toℕ r₀) (toℕ r₁)
          (P.subst (λ k → toℕ r₀ + k * (suc m)  ≡ toℕ r₁ + k₁ * (suc m)) k₀≡k₁ eq))

    from∘to : ∀ {m n}(is : Vec (Fin m) n) → from (to is) ≡ is
    from∘to {m} {.0} [] = P.refl
    from∘to {zero} {.(suc _)} (() ∷ is)
    from∘to {suc m} {suc n} (i ∷ is) with to (i ∷ is) | P.inspect to (i ∷ is)
    from∘to {suc m} {suc n} (i ∷ is) | j | Reveal_·_is_.[ eq ] with P.cong toℕ eq
    ... | eq2 rewrite toℕ-fromℕ≤ (shift i (to is)) with ((toℕ j) divMod (suc m ^ n))
      {≢0 = fromWitnessFalse (suci^j≢0 _ n)}
    ... | result quotient remainder property with chn (suc m ^ n) {toℕ i}{quotient}
          {to is}{remainder} (trans eq2 property)
    ... | k₀≡k₁ , r₀≡r₁ rewrite P.sym r₀≡r₁ | from∘to is =
        P.cong (_∷ is) (toℕ-injective (begin toℕ (Fin.fromℕ≤ _)
                                               ≡⟨ toℕ-fromℕ≤ _ ⟩ quotient
                                               ≡⟨ P.sym k₀≡k₁ ⟩ toℕ i ∎))
        where
          open ≡-Reasoning

    to∘from : ∀ {m n}(i : Fin (m ^ n)) → to (from{m}{n} i) ≡ i
    to∘from {m} {zero} Fin.zero = refl
    to∘from {m} {zero} (Fin.suc ())
    to∘from {zero} {suc n} ()
    to∘from {suc m} {suc n} i with ((toℕ i) divMod (suc m ^ n))
      {≢0 = fromWitnessFalse (suci^j≢0 _ n)}
    to∘from {suc m} {suc n} i | result quotient remainder property = goal
      where
        q<sm : quotient < suc m
        q<sm = ≰⇒> (λ sm≤q → <⇒≱ (toℕ<n i)
                (begin (suc m) * (suc m ^ n)
                   ≤⟨ *-mono-≤ sm≤q ≤-refl ⟩ quotient * (suc m ^ n)
                   ≤⟨ +-mono-≤ (z≤n {toℕ remainder}) ≤-refl ⟩ toℕ remainder + quotient * (suc m ^ n)
                   ≡⟨ P.sym property ⟩ toℕ i ∎))
              where
                open ≤-Reasoning

        goal : to (Fin.fromℕ≤ q<sm  ∷ from {suc m}{n} remainder) ≡ i
        goal = toℕ-injective
              (begin _ ≡⟨ toℕ-fromℕ≤ _ ⟩
                         toℕ (to (from {suc m} {n} remainder)) + toℕ (Fin.fromℕ≤ q<sm ) * (suc m ^ n)
                       ≡⟨ P.cong₂ (λ r k → toℕ r + k * (suc m ^ n))
                            (to∘from {suc m} {n} remainder) (toℕ-fromℕ≤ q<sm)
                          ⟩  toℕ remainder + quotient * (suc m ^ n)
                       ≡⟨ P.sym property ⟩ toℕ i ∎)
          where
            open ≡-Reasoning

⟶-finitude-toVec : ∀{m n a b p q}{A : Setoid a p}{B : Setoid b q} → Finitude A m → Finitude B n
             → A ⟶ B → Vec (Fin n) m
⟶-finitude-toVec finA finB f = Vec.tabulate
                                   (λ i → (Inverse.to finB  F.∘ f F.∘ Inverse.from finA) ⟨$⟩ i )

⟶-finitude-fromVec : ∀{m n a b p q}{A : Setoid a p}{B : Setoid b q} → Finitude A m → Finitude B n
             → Vec (Fin n) m → A ⟶ B
⟶-finitude-fromVec {A = SA}{B = SB} finA finB vec =
  record {   _⟨$⟩_ = f
          ;  cong  = f-cong   }
  where
    open module SA = Setoid SA renaming (Carrier to A) using ()
    open module SB = Setoid SB renaming (Carrier to B) using ()
    f : A → B
    f x = Inverse.from finB ⟨$⟩ Vec.lookup (Inverse.to finA ⟨$⟩ x) vec

    f-cong : ∀ {x y} → x SA.≈ y → f x SB.≈ f y
    f-cong {x}{y} x≈y = F.cong (Inverse.from finB)
                           (P.cong (flip Vec.lookup vec) (F.cong (Inverse.to finA) x≈y))

⟶-finitude↔Vec : ∀{m n a b p q}{A : Setoid a p}{B : Setoid b q} → Finitude A n → Finitude B m
                 → Inverse (A ⇨ B) (P.setoid (Vec (Fin m) n))
Inverse.to (⟶-finitude↔Vec {m} {n} {A = S₁} {S₂} finA finB) ._⟨$⟩_ = ⟶-finitude-toVec finA finB
Inverse.to (⟶-finitude↔Vec {m} {n} {A = S₁} {S₂} finA finB) .F.cong {f} {g} eq = tabulate-cong ( λ i →
  F.cong (Inverse.to finB) (eq ≈₁-refl) )
  where
    open import Data.Vec.Properties
    open Setoid S₁ renaming (isEquivalence to isEquivalence₁)
    open IsEquivalence isEquivalence₁ renaming (refl to ≈₁-refl)

Inverse.from (⟶-finitude↔Vec finA finB) = P.→-to-⟶ (⟶-finitude-fromVec finA finB)
Inv._InverseOf_.left-inverse-of (Inverse.inverse-of (⟶-finitude↔Vec {m = m}{n}{A = S₁} {S₂} finA finB)) f {x}{y} x≈y =
  begin ⟶-finitude-fromVec finA finB (⟶-finitude-toVec finA finB f) ⟨$⟩ x
         ≈⟨ F.cong (Inverse.from finB) lemma  ⟩ _
         ≈⟨ linv₂ _  ⟩ _
         ≈⟨ F.cong f (linv₁ x) ⟩ _
         ≈⟨ F.cong f x≈y ⟩ f ⟨$⟩ y ∎
  where
    open import Data.Vec.Properties
    open import Relation.Binary.Reasoning.Setoid (S₂)
    open Setoid S₁ renaming (isEquivalence to isEquivalence₁)
    open IsEquivalence isEquivalence₁ renaming (refl to ≈₁-refl; trans to ≈₁-trans)
    open Setoid S₂ renaming (isEquivalence to isEquivalence₂)
    open IsEquivalence isEquivalence₂ renaming (refl to ≈₂-refl; trans to ≈₂-trans)
    F = (Inverse.to finB  F.∘ f F.∘ Inverse.from finA) ⟨$⟩_
    lemma = lookup∘tabulate F (Inverse.to finA ⟨$⟩ x)
    linv₁ = finA .Inverse.inverse-of .Inv._InverseOf_.left-inverse-of
    linv₂ = finB .Inverse.inverse-of .Inv._InverseOf_.left-inverse-of
Inv._InverseOf_.right-inverse-of (Inverse.inverse-of (⟶-finitude↔Vec finA finB)) vec =
  begin _  ≡⟨ tabulate-cong lemma ⟩ _
           ≡⟨ tabulate∘lookup vec ⟩ vec ∎
  where
    open import Data.Vec.Properties
    open P.≡-Reasoning
    rinv₁ = finA .Inverse.inverse-of .Inv._InverseOf_.right-inverse-of
    rinv₂ = finB .Inverse.inverse-of .Inv._InverseOf_.right-inverse-of
    lemma : Inverse.to finB F.∘ (⟶-finitude-fromVec finA finB vec) F.∘ Inverse.from finA ⟨$⟩_ ≗ flip lookup vec
    lemma i = begin _ ≡⟨ rinv₂ _ ⟩ _
                      ≡⟨ P.cong (flip lookup vec) (rinv₁ i)  ⟩ lookup i vec ∎

⟶-finitude : ∀{m n a b p q}{A : Setoid a p}{B : Setoid b q} → Finitude A n → Finitude B m
                 → Finitude (A ⇨ B) (m ^ n)
⟶-finitude finA finB = exponent  Inv.∘ (⟶-finitude↔Vec finA finB)

max_stars_repo_name: tizmd/agda-finitary

max_issues_repo_name: tizmd/agda-finitary

max_forks_repo_name: tizmd/agda-finitary


text:
module product where

open import level

----------------------------------------------------------------------
-- types
----------------------------------------------------------------------

data Σ {ℓ ℓ'} (A : Set ℓ) (B : A → Set ℓ') : Set (ℓ ⊔ ℓ') where
  _,_ : (a : A) → (b : B a) → Σ A B

data Σi {ℓ ℓ'} (A : Set ℓ) (B : A → Set ℓ') : Set (ℓ ⊔ ℓ') where
  ,_ : {a : A} → (b : B a) → Σi A B

_×_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
A × B = Σ A (λ x → B)

_i×_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
A i× B = Σi A (λ x → B)

----------------------------------------------------------------------
-- syntax
----------------------------------------------------------------------

infix 1 Σ-syntax
infixr 2 _×_ _i×_ _∧_
infixr 4 _,_
infix  4 ,_

-- This provides the syntax: Σ[ x ∈ A ] B it is taken from the Agda
-- standard library. This style is nice when working in Set.
Σ-syntax : ∀ {a b} (A : Set a) → (A → Set b) → Set (a ⊔ b)
Σ-syntax = Σ

syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B

----------------------------------------------------------------------
-- operations
----------------------------------------------------------------------
fst : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → A × B → A
fst (a , b) = a

snd : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → A × B → B
snd (a , b) = b

⟨_,_⟩ : ∀{ℓ₁ ℓ₂ ℓ₃ ℓ₄}
         {A : Set ℓ₁}{B : Set ℓ₂}
         {C : Set ℓ₃}{D : Set ℓ₄}
       → (A → C)
       → (B → D)
       → (A × B → C × D)
⟨ f , g ⟩ (a , b) = f a , g b

twist-× : ∀{ℓ₁ ℓ₂}
     {A : Set ℓ₁}{B : Set ℓ₂}
    → A × B
    → B × A
twist-× (a , b) = (b , a)

rl-assoc-× : ∀{ℓ₁ ℓ₂ ℓ₃}
             {A : Set ℓ₁}{B : Set ℓ₂}
             {C : Set ℓ₃}
           → A × (B × C)
           → (A × B) × C
rl-assoc-× (a , b , c) =  ((a , b) , c)

lr-assoc-× : ∀{ℓ₁ ℓ₂ ℓ₃}
             {A : Set ℓ₁}{B : Set ℓ₂}
             {C : Set ℓ₃}
           → (A × B) × C
           → A × (B × C)
lr-assoc-× ((a , b) , c) = (a , b , c)

----------------------------------------------------------------------
-- some logical notation
----------------------------------------------------------------------
_∧_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
_∧_ = _×_

∃ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : A → Set ℓ') → Set (ℓ ⊔ ℓ')
∃ = Σ

∃i : ∀ {ℓ ℓ'} (A : Set ℓ) (B : A → Set ℓ') → Set (ℓ ⊔ ℓ')
∃i = Σi

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
------------------------------------------------------------------------
-- Fixity and associativity
------------------------------------------------------------------------

module Mixfix.Fixity where

open import Data.Fin using (Fin; zero; suc; #_)
open import Data.Fin.Properties using (eq?)
open import Function.LeftInverse
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as Eq

data Associativity : Set where
  left  : Associativity
  right : Associativity
  non   : Associativity

-- A combination of fixity and associativity. Only infix operators
-- have associativity.

-- Note that infix is a reserved word.

data Fixity : Set where
  prefx  : Fixity
  infx   : (assoc : Associativity) → Fixity
  postfx : Fixity
  closed : Fixity

Fixity-is-finite : LeftInverse (Eq.setoid Fixity) (Eq.setoid (Fin 6))
Fixity-is-finite = record
  { from            = Eq.→-to-⟶ from
  ; to              = Eq.→-to-⟶ to
  ; left-inverse-of = left-inverse-of
  }
  where
  to : Fixity → Fin 6
  to prefx        = # 0
  to (infx left)  = # 1
  to (infx right) = # 2
  to (infx non)   = # 3
  to postfx       = # 4
  to closed       = # 5

  from : Fin 6 → Fixity
  from zero                                   = prefx
  from (suc zero)                             = infx left
  from (suc (suc zero))                       = infx right
  from (suc (suc (suc zero)))                 = infx non
  from (suc (suc (suc (suc zero))))           = postfx
  from (suc (suc (suc (suc (suc zero)))))     = closed
  from (suc (suc (suc (suc (suc (suc ()))))))

  left-inverse-of : Eq.→-to-⟶ from LeftInverseOf Eq.→-to-⟶ to
  left-inverse-of prefx        = refl
  left-inverse-of (infx left)  = refl
  left-inverse-of (infx right) = refl
  left-inverse-of (infx non)   = refl
  left-inverse-of postfx       = refl
  left-inverse-of closed       = refl

_≟_ : Decidable (_≡_ {A = Fixity})
_≟_ = eq? injection
  where open LeftInverse Fixity-is-finite

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


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

open import Categories.Category.Core

-- Reflexive pairs and reflexive coequalizers
-- https://ncatlab.org/nlab/show/reflexive+coequalizer
module Categories.Diagram.ReflexivePair {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level

open import Categories.Diagram.Coequalizer 𝒞

open Category 𝒞
open HomReasoning
open Equiv

private
  variable
    A B R : Obj

-- A reflexive pair can be thought of as a vast generalization of a reflexive relation.
-- To see this, consider the case in 'Set' where 'R ⊆ A × A', and 'f' and 'g' are the projections.
-- Then, our morphism 's' would have to look something like the diagonal morphism due to the
-- restriction it is a section of both 'f' and 'g'.
record IsReflexivePair (f g : R ⇒ A) (s : A ⇒ R) : Set e where
  field
    sectionₗ : f ∘ s ≈ id
    sectionᵣ : g ∘ s ≈ id

  section : f ∘ s ≈ g ∘ s
  section = sectionₗ ○ ⟺ sectionᵣ

record ReflexivePair (f g : R ⇒ A) : Set (ℓ ⊔ e) where
  field
    s : A ⇒ R
    isReflexivePair : IsReflexivePair f g s

  open IsReflexivePair isReflexivePair public

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
------------------------------------------------------------------------
-- A large class of algebraic structures satisfies the property that
-- isomorphic instances of a structure are equal (assuming univalence)
------------------------------------------------------------------------

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

-- This code has been superseded by more recent developments. See
-- README.agda.

-- This module has been developed in collaboration with Thierry
-- Coquand.

open import Equality

module Univalence-axiom.Isomorphism-implies-equality
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Bijection eq
open Derived-definitions-and-properties eq
open import Equivalence eq as Eq
open import H-level eq
open import H-level.Closure eq
open import Logical-equivalence
open import Prelude
open import Univalence-axiom eq

------------------------------------------------------------------------
-- N-ary functions

-- N-ary functions.

_^_⟶_ : Type → ℕ → Type → Type
A ^ zero  ⟶ B = B
A ^ suc n ⟶ B = A → A ^ n ⟶ B

-- N-ary function morphisms.

Is-_-ary-morphism :
  (n : ℕ) {A B : Type} → A ^ n ⟶ A → B ^ n ⟶ B → (A → B) → Type
Is- zero  -ary-morphism f₁ f₂ m = m f₁ ≡ f₂
Is- suc n -ary-morphism f₁ f₂ m =
  ∀ x → Is- n -ary-morphism (f₁ x) (f₂ (m x)) m

abstract

  -- If _↔_.to m is a morphism, then _↔_.from m is also a morphism.

  from-also-_-ary-morphism :
    (n : ℕ) {A B : Type} (f₁ : A ^ n ⟶ A) (f₂ : B ^ n ⟶ B) (m : A ↔ B) →
    Is- n -ary-morphism f₁ f₂ (_↔_.to m) →
    Is- n -ary-morphism f₂ f₁ (_↔_.from m)
  from-also- zero  -ary-morphism f₁ f₂ m is = _↔_.to-from m is
  from-also- suc n -ary-morphism f₁ f₂ m is = λ x →
    from-also- n -ary-morphism (f₁ (from x)) (f₂ x) m
      (subst (λ y → Is- n -ary-morphism (f₁ (from x)) (f₂ y) to)
             (right-inverse-of x)
             (is (from x)))
    where open _↔_ m

-- Changes the type of an n-ary function.

cast : {A₁ A₂ : Type} → A₁ ≃ A₂ → ∀ n → A₁ ^ n ⟶ A₁ → A₂ ^ n ⟶ A₂
cast A₁≃A₂ zero    = _≃_.to A₁≃A₂
cast A₁≃A₂ (suc n) = λ f x → cast A₁≃A₂ n (f (_≃_.from A₁≃A₂ x))

abstract

  -- Cast simplification lemma.

  cast-id : {A : Type} →
            (∀ n → Extensionality′ A (λ _ → A ^ n ⟶ A)) →
            ∀ n (f : A ^ n ⟶ A) → cast Eq.id n f ≡ f
  cast-id ext zero    f = refl f
  cast-id ext (suc n) f = ext n $ λ x → cast-id ext n (f x)

  -- We can express cast as an instance of subst (assuming
  -- extensionality and univalence).

  cast-is-subst :
    (∀ {A : Type} n → Extensionality′ A (λ _ → A ^ n ⟶ A)) →
    {A₁ A₂ : Type}
    (univ : Univalence′ A₁ A₂)
    (A₁≃A₂ : A₁ ≃ A₂) (n : ℕ) (f : A₁ ^ n ⟶ A₁) →
    cast A₁≃A₂ n f ≡ subst (λ C → C ^ n ⟶ C) (≃⇒≡ univ A₁≃A₂) f
  cast-is-subst ext univ A₁≃A₂ n =
    transport-theorem
      (λ A → A ^ n ⟶ A)
      (λ A≃B f → cast A≃B n f)
      (cast-id ext n)
      univ
      A₁≃A₂

  -- If there is an isomorphism from f₁ to f₂, then the corresponding
  -- instance of cast maps f₁ to f₂ (assuming extensionality).

  cast-isomorphism :
    {A₁ A₂ : Type} →
    (∀ n → Extensionality′ A₂ (λ _ → A₂ ^ n ⟶ A₂)) →
    (A₁≃A₂ : A₁ ≃ A₂)
    (n : ℕ) (f₁ : A₁ ^ n ⟶ A₁) (f₂ : A₂ ^ n ⟶ A₂) →
    Is- n -ary-morphism f₁ f₂ (_≃_.to A₁≃A₂) →
    cast A₁≃A₂ n f₁ ≡ f₂
  cast-isomorphism ext A₁≃A₂ zero    f₁ f₂ is = is
  cast-isomorphism ext A₁≃A₂ (suc n) f₁ f₂ is = ext n $ λ x →
    cast A₁≃A₂ n (f₁ (from x))  ≡⟨ cast-isomorphism ext A₁≃A₂ n _ _ (is (from x)) ⟩
    f₂ (to (from x))            ≡⟨ cong f₂ (right-inverse-of x) ⟩∎
    f₂ x                        ∎
    where open _≃_ A₁≃A₂

  -- Combining the results above we get the following: if there is an
  -- isomorphism from f₁ to f₂, then the corresponding instance of
  -- subst maps f₁ to f₂ (assuming extensionality and univalence).

  subst-isomorphism :
    (∀ {A : Type} n → Extensionality′ A (λ _ → A ^ n ⟶ A)) →
    {A₁ A₂ : Type}
    (univ : Univalence′ A₁ A₂)
    (A₁≃A₂ : A₁ ≃ A₂)
    (n : ℕ) (f₁ : A₁ ^ n ⟶ A₁) (f₂ : A₂ ^ n ⟶ A₂) →
    Is- n -ary-morphism f₁ f₂ (_≃_.to A₁≃A₂) →
    subst (λ A → A ^ n ⟶ A) (≃⇒≡ univ A₁≃A₂) f₁ ≡ f₂
  subst-isomorphism ext univ A₁≃A₂ n f₁ f₂ is =
    subst (λ A → A ^ n ⟶ A) (≃⇒≡ univ A₁≃A₂) f₁  ≡⟨ sym $ cast-is-subst ext univ A₁≃A₂ n f₁ ⟩
    cast A₁≃A₂ n f₁                              ≡⟨ cast-isomorphism ext A₁≃A₂ n f₁ f₂ is ⟩∎
    f₂                                           ∎

------------------------------------------------------------------------
-- A class of algebraic structures

-- An algebraic structure universe.

mutual

  -- Codes for structures.

  infixl 5 _+operator_ _+axiom_

  data Structure : Type₁ where
    empty : Structure

    -- N-ary functions.
    _+operator_ : Structure → (n : ℕ) → Structure

    -- Arbitrary /propositional/ axioms.
    _+axiom_ : (s : Structure)
               (P : ∃ λ (P : (A : Type) → ⟦ s ⟧ A → Type) →
                      ∀ A s → Is-proposition (P A s)) →
               Structure

  -- Interpretation of the codes.

  ⟦_⟧ : Structure → Type → Type₁
  ⟦ empty                 ⟧ A = ↑ _ ⊤
  ⟦ s +operator n         ⟧ A = ⟦ s ⟧ A × (A ^ n ⟶ A)
  ⟦ s +axiom (P , P-prop) ⟧ A = Σ (⟦ s ⟧ A) (P A)

-- Top-level interpretation.

⟪_⟫ : Structure → Type₁
⟪ s ⟫ = ∃ ⟦ s ⟧

-- Morphisms.

Is-structure-morphism :
  (s : Structure) →
  {A B : Type} → ⟦ s ⟧ A → ⟦ s ⟧ B →
  (A → B) → Type
Is-structure-morphism empty           _          _          m = ⊤
Is-structure-morphism (s +axiom _)    (s₁ , _)   (s₂ , _)   m =
  Is-structure-morphism s s₁ s₂ m
Is-structure-morphism (s +operator n) (s₁ , op₁) (s₂ , op₂) m =
  Is-structure-morphism s s₁ s₂ m × Is- n -ary-morphism op₁ op₂ m

-- Isomorphisms.

Isomorphism : (s : Structure) → ⟪ s ⟫ → ⟪ s ⟫ → Type
Isomorphism s (A₁ , s₁) (A₂ , s₂) =
  ∃ λ (m : A₁ ↔ A₂) → Is-structure-morphism s s₁ s₂ (_↔_.to m)

abstract

  -- If _↔_.to m is a morphism, then _↔_.from m is also a morphism.

  from-also-structure-morphism :
    (s : Structure) →
    {A B : Type} {s₁ : ⟦ s ⟧ A} {s₂ : ⟦ s ⟧ B} →
    (m : A ↔ B) →
    Is-structure-morphism s s₁ s₂ (_↔_.to m) →
    Is-structure-morphism s s₂ s₁ (_↔_.from m)
  from-also-structure-morphism empty           m = _
  from-also-structure-morphism (s +axiom _)    m =
    from-also-structure-morphism s m
  from-also-structure-morphism (s +operator n) m =
    Σ-map (from-also-structure-morphism s m)
          (from-also- n -ary-morphism _ _ m)

  -- Isomorphic structures are equal (assuming univalence).

  isomorphic-equal :
    Univalence′ (Type ²/≡) Type →
    Univalence lzero →
    (s : Structure) (s₁ s₂ : ⟪ s ⟫) →
    Isomorphism s s₁ s₂ → s₁ ≡ s₂
  isomorphic-equal univ₁ univ₂
    s (A₁ , s₁) (A₂ , s₂) (m , is) =

    (A₁ , s₁)  ≡⟨ Σ-≡,≡→≡ A₁≡A₂ (lemma s s₁ s₂ is) ⟩∎
    (A₂ , s₂)  ∎

    where
    open _↔_ m

    -- Extensionality follows from univalence.

    ext : {A : Type} {B : A → Type} → Extensionality′ A B
    ext = dependent-extensionality′ univ₁ (λ _ → univ₂)

    -- The presence of the bijection implies that the structure's
    -- underlying types are equal (due to univalence).

    A₁≡A₂ : A₁ ≡ A₂
    A₁≡A₂ = _≃_.from (≡≃≃ univ₂) $ ↔⇒≃ m

    -- We can lift subst-isomorphism to structures by recursion on
    -- structure codes.

    lemma : (s : Structure)
            (s₁ : ⟦ s ⟧ A₁) (s₂ : ⟦ s ⟧ A₂) →
            Is-structure-morphism s s₁ s₂ to →
            subst ⟦ s ⟧ A₁≡A₂ s₁ ≡ s₂
    lemma empty _ _ _ = refl _

    lemma (s +axiom (P , P-prop)) (s₁ , ax₁) (s₂ , ax₂) is =
      subst (λ A → Σ (⟦ s ⟧ A) (P A)) A₁≡A₂ (s₁ , ax₁)  ≡⟨ push-subst-pair′ ⟦ s ⟧ (uncurry P) (lemma s s₁ s₂ is) ⟩
      (s₂ , _)                                          ≡⟨ cong (_,_ s₂) $ P-prop _ _ _ _ ⟩∎
      (s₂ , ax₂)                                        ∎

    lemma (s +operator n) (s₁ , op₁) (s₂ , op₂) (is-s , is-o) =
      subst (λ A → ⟦ s ⟧ A × (A ^ n ⟶ A)) A₁≡A₂ (s₁ , op₁)  ≡⟨ push-subst-pair′ ⟦ s ⟧ (λ { (A , _) → A ^ n ⟶ A }) (lemma s s₁ s₂ is-s) ⟩

      (s₂ , subst₂ (λ { (A , _) → A ^ n ⟶ A }) A₁≡A₂
                   (lemma s s₁ s₂ is-s) op₁)                ≡⟨ cong (_,_ s₂) $ subst₂-proj₁ (λ A → A ^ n ⟶ A) ⟩

      (s₂ , subst (λ A → A ^ n ⟶ A) A₁≡A₂ op₁)              ≡⟨ cong (_,_ s₂) $ subst-isomorphism (λ _ → ext) univ₂ (↔⇒≃ m) n op₁ op₂ is-o ⟩∎
      (s₂ , op₂)                                            ∎

------------------------------------------------------------------------
-- Some example structures

-- Example: magmas.

magma : Structure
magma = empty +operator 2

Magma : Type₁
Magma = ⟪ magma ⟫

private

  -- An unfolding of Magma.

  Magma-unfolded : Magma ≡ ∃ λ (A : Type) → ↑ _ ⊤ × (A → A → A)
  Magma-unfolded = refl _

-- Example: semigroups. The definition uses extensionality to prove
-- that the axioms are propositional. Note that one axiom states that
-- the underlying type is a set. This assumption is used to prove that
-- the other axiom is propositional.

semigroup : Extensionality lzero lzero → Structure
semigroup ext =
  empty

  +axiom
    ( (λ A _ → Is-set A)
    , is-set-prop
    )

  +operator 2

  +axiom
    ( (λ { _ (_ , _∙_) →
           ∀ x y z → (x ∙ (y ∙ z)) ≡ ((x ∙ y) ∙ z) })
    , assoc-prop
    )

  where
  is-set-prop = λ _ _ → H-level-propositional ext 2

  assoc-prop = λ { _ ((_ , A-set) , _) →
      Π-closure ext 1 λ _ →
      Π-closure ext 1 λ _ →
      Π-closure ext 1 λ _ →
      A-set
    }

Semigroup : Extensionality lzero lzero → Type₁
Semigroup ext = ⟪ semigroup ext ⟫

private

  -- An unfolding of Semigroup.

  Semigroup-unfolded :
    (ext : Extensionality lzero lzero) →
    Semigroup ext ≡ Σ
      Type                                       λ A → Σ (Σ (Σ (↑ _ ⊤) λ _ →
      Is-set A                                 ) λ _ →
      A → A → A                                ) λ { (_ , _∙_) →
      ∀ x y z → (x ∙ (y ∙ z)) ≡ ((x ∙ y) ∙ z) }
  Semigroup-unfolded _ = refl _

-- Example: abelian groups.

abelian-group : Extensionality lzero lzero → Structure
abelian-group ext =
  empty

  -- The underlying type is a set.
  +axiom
    ( (λ A _ → Is-set A)
    , is-set-prop
    )

  -- The binary group operation.
  +operator 2

  -- Commutativity.
  +axiom
    ( (λ { _ (_ , _∙_) →
           ∀ x y → (x ∙ y) ≡ (y ∙ x) })
    , comm-prop
    )

  -- Associativity.
  +axiom
    ( (λ { _ ((_ , _∙_) , _) →
           ∀ x y z → (x ∙ (y ∙ z)) ≡ ((x ∙ y) ∙ z) })
    , assoc-prop
    )

  -- Identity.
  +operator 0

  -- Left identity.
  +axiom
    ( (λ { _ ((((_ , _∙_) , _) , _) , e) →
           ∀ x → (e ∙ x) ≡ x })
    , left-identity-prop
    )

  -- Right identity.
  +axiom
    ( (λ { _ (((((_ , _∙_) , _) , _) , e) , _) →
           ∀ x → (x ∙ e) ≡ x })
    , right-identity-prop
    )

  -- Inverse.
  +operator 1

  -- Left inverse.
  +axiom
    ( (λ { _ (((((((_ , _∙_) , _) , _) , e) , _) , _) , _⁻¹) →
           ∀ x → ((x ⁻¹) ∙ x) ≡ e })
    , left-inverse-prop
    )

  -- Right inverse.
  +axiom
    ( (λ { _ ((((((((_ , _∙_) , _) , _) , e) , _) , _) , _⁻¹) , _) →
           ∀ x → (x ∙ (x ⁻¹)) ≡ e })
    , right-inverse-prop
    )

  where
  is-set-prop = λ _ _ → H-level-propositional ext 2

  comm-prop =
    λ { _ ((_ , A-set) , _) →
      Π-closure ext 1 λ _ →
      Π-closure ext 1 λ _ →
      A-set
    }

  assoc-prop =
    λ { _ (((_ , A-set) , _) , _) →
      Π-closure ext 1 λ _ →
      Π-closure ext 1 λ _ →
      Π-closure ext 1 λ _ →
      A-set
    }

  left-identity-prop =
    λ { _ (((((_ , A-set) , _) , _) , _) , _) →
      Π-closure ext 1 λ _ →
      A-set
    }

  right-identity-prop =
    λ { _ ((((((_ , A-set) , _) , _) , _) , _) , _) →
      Π-closure ext 1 λ _ →
      A-set
    }

  left-inverse-prop =
    λ { _ ((((((((_ , A-set) , _) , _) , _) , _) , _) , _) , _) →
      Π-closure ext 1 λ _ →
      A-set
    }

  right-inverse-prop =
    λ { _ (((((((((_ , A-set) , _) , _) , _) , _) , _) , _) , _) , _) →
      Π-closure ext 1 λ _ →
      A-set
    }

Abelian-group : Extensionality lzero lzero → Type₁
Abelian-group ext = ⟪ abelian-group ext ⟫

private

  -- An unfolding of Abelian-group. Note that the inner structure is
  -- left-nested.

  Abelian-group-unfolded :
    (ext : Extensionality lzero lzero) →
    Abelian-group ext ≡ Σ
      Type                                       λ A → Σ (Σ (Σ (Σ (Σ (Σ (Σ (Σ (Σ (Σ (↑ _ ⊤) λ _ →
      Is-set A                                 ) λ _ →
      A → A → A                                ) λ {        (_ , _∙_) →
      ∀ x y → (x ∙ y) ≡ (y ∙ x)               }) λ {       ((_ , _∙_) , _) →
      ∀ x y z → (x ∙ (y ∙ z)) ≡ ((x ∙ y) ∙ z) }) λ _ →
      A                                        ) λ {     ((((_ , _∙_) , _) , _) , e) →
      ∀ x → (e ∙ x) ≡ x                       }) λ {    (((((_ , _∙_) , _) , _) , e) , _) →
      ∀ x → (x ∙ e) ≡ x                       }) λ _ →
      A → A                                    ) λ {  (((((((_ , _∙_) , _) , _) , e) , _) , _) , _⁻¹) →
      ∀ x → ((x ⁻¹) ∙ x) ≡ e                  }) λ { ((((((((_ , _∙_) , _) , _) , e) , _) , _) , _⁻¹) , _) →
      ∀ x → (x ∙ (x ⁻¹)) ≡ e                  }

  Abelian-group-unfolded _ = refl _

------------------------------------------------------------------------
-- Right-nested structures

-- Right-nested structures are arguably easier to define (see the
-- example below). However, the following class of right-nested
-- structures is in some sense different from the class above. Take
-- "operator 0 f : Structureʳ Bool", for instance. The /shape/ of f op
-- can vary depending on whether the operator op is true or false.
--
-- One could perhaps avoid this issue by only considering values of
-- type ∀ A → Structureʳ A. However, it is not obvious how to convert
-- elements of this type to elements of type Structure in a
-- meaning-preserving way. Furthermore it seems to be awkward to
-- define things like Is-structure-isomorphism when using values of
-- type ∀ A → Structureʳ A (see the definition of
-- Is-structure-isomorphismʳ below).

-- Codes. (Note that these structures are defined for a single
-- underlying type.)

data Structureʳ (A : Type) : Type₁ where
  empty : Structureʳ A

  -- N-ary functions.
  operator : (n : ℕ)
             (s : A ^ n ⟶ A → Structureʳ A) →
             Structureʳ A

  -- Arbitrary /propositional/ axioms.
  axiom : (P : Type)
          (P-prop : Is-proposition P)
          (s : P → Structureʳ A) →
          Structureʳ A

-- Interpretation of the codes.

⟦_⟧ʳ : {A : Type} → Structureʳ A → Type₁
⟦ empty            ⟧ʳ = ↑ _ ⊤
⟦ operator n s     ⟧ʳ = ∃ λ op → ⟦ s op ⟧ʳ
⟦ axiom P P-prop s ⟧ʳ = ∃ λ p  → ⟦ s p  ⟧ʳ

-- Top-level interpretation.

⟪_⟫ʳ : (∀ A → Structureʳ A) → Type₁
⟪ s ⟫ʳ = ∃ λ A → ⟦ s A ⟧ʳ

-- The property of being an isomorphism.

Is-structure-isomorphismʳ :
  (s : ∀ A → Structureʳ A) →
  {A B : Type} → ⟦ s A ⟧ʳ → ⟦ s B ⟧ʳ →
  A ↔ B → Type
Is-structure-isomorphismʳ s {A} {B} S₁ S₂ m =
  helper (s A) (s B) S₁ S₂
  where
  helper : (s₁ : Structureʳ A) (s₂ : Structureʳ B) →
           ⟦ s₁ ⟧ʳ → ⟦ s₂ ⟧ʳ → Type
  helper empty            empty            _          _          = ⊤
  helper (operator n₁ s₁) (operator n₂ s₂) (op₁ , S₁) (op₂ , S₂) =
    (∃ λ (eq : n₁ ≡ n₂) →
       Is- n₁ -ary-morphism
         op₁ (subst (λ n → B ^ n ⟶ B) (sym eq) op₂) (_↔_.to m)) ×
    helper (s₁ op₁) (s₂ op₂) S₁ S₂
  helper (axiom P₁ _ s₁) (axiom P₂ _ s₂) (p₁ , S₁) (p₂ , S₂) =
    helper (s₁ p₁) (s₂ p₂) S₁ S₂

  helper empty               (operator n s₂)     _ _ = ⊥
  helper empty               (axiom P P-prop s₂) _ _ = ⊥
  helper (operator n s₁)     empty               _ _ = ⊥
  helper (operator n s₁)     (axiom P P-prop s₂) _ _ = ⊥
  helper (axiom P P-prop s₁) empty               _ _ = ⊥
  helper (axiom P P-prop s₁) (operator n s₂)     _ _ = ⊥

-- Example: semigroups.

semigroupʳ :
  Extensionality lzero lzero →
  ∀ A → Structureʳ A
semigroupʳ ext A =
  axiom (Is-set A)

        (H-level-propositional ext 2)

        λ A-set →

  operator 2 λ _∙_ →

  axiom (∀ x y z → (x ∙ (y ∙ z)) ≡ ((x ∙ y) ∙ z))

        (Π-closure ext 1 λ _ →
         Π-closure ext 1 λ _ →
         Π-closure ext 1 λ _ →
         A-set)

        λ _ →

  empty

Semigroupʳ : Extensionality lzero lzero → Type₁
Semigroupʳ ext = ⟪ semigroupʳ ext ⟫ʳ

private

  -- An unfolding of Semigroupʳ.

  Semigroupʳ-unfolded :
    (ext : Extensionality lzero lzero) →
    Semigroupʳ ext ≡
    ∃ λ (A   : Type) →
    ∃ λ (_   : Is-set A) →
    ∃ λ (_∙_ : A → A → A) →
    ∃ λ (_   : ∀ x y z → (x ∙ (y ∙ z)) ≡ ((x ∙ y) ∙ z)) →
    ↑ _ ⊤
  Semigroupʳ-unfolded _ = refl _

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Construction.Properties.Kleisli where

open import Level
import Relation.Binary.PropositionalEquality as ≡

open import Categories.Adjoint
open import Categories.Adjoint.Properties
open import Categories.Category
open import Categories.Functor using (Functor; _∘F_)
open import Categories.Functor.Equivalence
open import Categories.Monad
import Categories.Morphism.Reasoning as MR

open import Categories.Adjoint.Construction.Kleisli
open import Categories.Category.Construction.Kleisli

private
  variable
    o ℓ e : Level
    𝒞 𝒟 : Category o ℓ e

module _ {F : Functor 𝒞 𝒟} {G : Functor 𝒟 𝒞} (F⊣G : Adjoint F G) where
  private
    T : Monad 𝒞
    T = adjoint⇒monad F⊣G

    𝒞ₜ : Category _ _ _
    𝒞ₜ = Kleisli T

    module 𝒞 = Category 𝒞
    module 𝒟 = Category 𝒟
    module 𝒞ₜ = Category 𝒞ₜ

    module T = Monad T
    module F = Functor F
    module G = Functor G

    open Adjoint F⊣G

  -- Maclane's Comparison Functor
  ComparisonF : Functor 𝒞ₜ 𝒟
  ComparisonF = record
    { F₀ = λ X → F.F₀ X
    ; F₁ = λ {A} {B} f → 𝒟 [ counit.η (F.F₀ B) ∘ F.F₁ f ]
    ; identity = zig
    ; homomorphism = λ {X} {Y} {Z} {f} {g} → begin
      𝒟 [ counit.η (F.F₀ Z) ∘ F.F₁ (𝒞 [ 𝒞 [ G.F₁ (counit.η (F.F₀ Z)) ∘ G.F₁ (F.F₁ g)] ∘ f ])]                 ≈⟨ refl⟩∘⟨ F.homomorphism ⟩
      𝒟 [ counit.η (F.F₀ Z) ∘ 𝒟 [ F.F₁ (𝒞 [ G.F₁ (counit.η (F.F₀ Z)) ∘ G.F₁ (F.F₁ g) ]) ∘ F.F₁ f ] ]          ≈⟨ refl⟩∘⟨ F.homomorphism  ⟩∘⟨refl ⟩
      𝒟 [ counit.η (F.F₀ Z) ∘ 𝒟 [ 𝒟 [ F.F₁ (G.F₁ (counit.η (F.F₀ Z))) ∘ F.F₁ (G.F₁ (F.F₁ g)) ] ∘ F.F₁ f ] ]   ≈⟨ center⁻¹ refl refl ⟩
      𝒟 [ 𝒟 [ counit.η (F.F₀ Z) ∘ F.F₁ (G.F₁ (counit.η (F.F₀ Z))) ] ∘ 𝒟 [ F.F₁ (G.F₁ (F.F₁ g)) ∘ F.F₁ f ] ]   ≈⟨ counit.commute (counit.η (F.F₀ Z)) ⟩∘⟨refl ⟩
      𝒟 [ 𝒟 [ counit.η (F.F₀ Z) ∘ (counit.η (F.F₀ (G.F₀ (F.F₀ Z)))) ] ∘ 𝒟 [ F.F₁ (G.F₁ (F.F₁ g)) ∘ F.F₁ f ] ] ≈⟨ extend² (counit.commute (F.F₁ g))  ⟩
      𝒟 [ 𝒟 [ counit.η (F.F₀ Z) ∘ F.F₁ g ] ∘ 𝒟 [ counit.η (F.F₀ Y) ∘ F.F₁ f ] ]                               ∎
    ; F-resp-≈ = λ eq → 𝒟.∘-resp-≈ʳ (F.F-resp-≈ eq)
    }
    where
      open 𝒟.HomReasoning
      open MR 𝒟

  private
    L = ComparisonF
    module L = Functor L
    module Gₜ = Functor (Forgetful T)
    module Fₜ = Functor (Free T)

  G∘L≡Forgetful : (G ∘F L) ≡F Forgetful T
  G∘L≡Forgetful = record
    { eq₀ = λ X → ≡.refl
    ; eq₁ = λ {A} {B} f → begin
      𝒞 [ 𝒞.id ∘ G.F₁ (𝒟 [ counit.η (F.F₀ B) ∘ F.F₁ f ]) ]        ≈⟨ 𝒞.identityˡ ⟩
      G.F₁ (𝒟 [ counit.η (F.F₀ B) ∘ F.F₁ f ])                      ≈⟨ G.homomorphism ⟩
      𝒞 [ G.F₁ (counit.η (F.F₀ B)) ∘ G.F₁ (F.F₁ f) ]               ≈˘⟨ 𝒞.identityʳ ⟩
      𝒞 [ 𝒞 [ G.F₁ (counit.η (F.F₀ B)) ∘ G.F₁ (F.F₁ f) ] ∘ 𝒞.id ] ∎

    }
    where
      open 𝒞.HomReasoning

  L∘Free≡F : (L ∘F Free T) ≡F F
  L∘Free≡F = record
    { eq₀ = λ X → ≡.refl
    ; eq₁ = λ {A} {B} f → begin
      𝒟 [ 𝒟.id ∘ 𝒟 [ counit.η (F.F₀ B) ∘ F.F₁ (𝒞 [ unit.η B ∘ f ]) ] ] ≈⟨ 𝒟.identityˡ ⟩
      𝒟 [ counit.η (F.F₀ B) ∘ F.F₁ (𝒞 [ unit.η B ∘ f ]) ]               ≈⟨ pushʳ F.homomorphism ⟩
      𝒟 [ 𝒟 [ counit.η (F.F₀ B) ∘ F.F₁ (unit.η B) ] ∘ F.F₁ f ]          ≈⟨ elimˡ zig ⟩
      F.F₁ f                                                              ≈˘⟨ 𝒟.identityʳ ⟩
      𝒟 [ F.F₁ f ∘ 𝒟.id ]                                               ∎
    }
    where
      open 𝒟.HomReasoning
      open MR 𝒟

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module Issue599 where

data Bool : Set where
  true false : Bool

-- standard lambda here
foo : Bool → Bool
foo = ?

-- pattern matching lambda here
bar : Bool → Bool
bar = ?

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The halting problem
------------------------------------------------------------------------

module Halting-problem where

open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)
open import Prelude hiding (const; Decidable)
open import Tactic.By.Propositional
open import Univalence-axiom

open import Equality.Decision-procedures equality-with-J
open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional equality-with-paths
  as Trunc hiding (rec)

-- To simplify the development, let's work with actual natural numbers
-- as variables and constants (see
-- Atom.one-can-restrict-attention-to-χ-ℕ-atoms).

open import Atom

open import Cancellation   χ-ℕ-atoms
open import Chi            χ-ℕ-atoms
open import Coding         χ-ℕ-atoms
open import Compatibility  χ-ℕ-atoms
open import Computability  χ-ℕ-atoms hiding (_∘_)
open import Constants      χ-ℕ-atoms
open import Deterministic  χ-ℕ-atoms
open import Free-variables χ-ℕ-atoms
open import Propositional  χ-ℕ-atoms
open import Reasoning      χ-ℕ-atoms
open import Termination    χ-ℕ-atoms
open import Values         χ-ℕ-atoms

open χ-atoms χ-ℕ-atoms

import Coding.Instances.Nat
open import Combinators as χ hiding (id; if_then_else_)
open import Internal-coding

------------------------------------------------------------------------
-- The extensional halting problem

-- The extensional halting problem is undecidable.

extensional-halting-problem :
  ¬ ∃ λ halts →
      Closed halts
        ×
      ∀ p → Closed p →
        (Terminates p →
         apply halts (lambda v-underscore p) ⇓ ⌜ true  ⦂ Bool ⌝)
          ×
        (¬ Terminates p →
         apply halts (lambda v-underscore p) ⇓ ⌜ false ⦂ Bool ⌝)
extensional-halting-problem (halts , cl , hyp) = contradiction
  where
  terminv : Exp → Exp
  terminv p = χ.if apply halts (lambda v-underscore p)
              then loop
              else ⌜ zero ⌝

  terminv-lemma : ∀ {p} → Closed p →
                  Terminates (terminv p) ⇔ ¬ Terminates p
  terminv-lemma {p} cl-p = record { to = to; from = from }
    where
    to : Terminates (terminv p) → ¬ Terminates p
    to (_ , case _           (there _ (there _ ())) _  _) p⇓
    to (_ , case halts⇓false (there _ here)         [] _) p⇓ =
      C.distinct-codes→distinct-names (λ ()) $
        proj₁ $ cancel-const $
          ⇓-deterministic (proj₁ (hyp p cl-p) p⇓) halts⇓false
    to (_ , case _ here [] loop⇓) p⇓ = ¬loop⇓ (_ , loop⇓)

    from : ¬ Terminates p → Terminates (terminv p)
    from ¬p⇓ =
      _ , case (proj₂ (hyp p cl-p) ¬p⇓) (there lemma here) [] (const [])
      where
      lemma = C.distinct-codes→distinct-names (λ ())

  strange : Exp
  strange = rec v-p (terminv (var v-p))

  strange-closed : Closed strange
  strange-closed =
    Closed′-closed-under-rec $
    if-then-else-closed
      (Closed′-closed-under-apply
         (Closed→Closed′ cl)
         (Closed′-closed-under-lambda
            (Closed′-closed-under-var (inj₂ (inj₁ refl)))))
      (Closed→Closed′ loop-closed)
      (Closed→Closed′ $ rep-closed zero)

  subst-lemma : terminv (var v-p) [ v-p ← strange ] ≡ terminv strange
  subst-lemma =
    terminv (var v-p) [ v-p ← strange ]             ≡⟨⟩

    χ.if apply ⟨ halts [ v-p ← strange ] ⟩
               (lambda v-underscore strange)
    then loop else ⌜ zero ⌝                         ≡⟨ ⟨by⟩ (subst-closed _ _ cl) ⟩

    χ.if apply halts (lambda v-underscore strange)
    then loop else ⌜ zero ⌝                         ≡⟨⟩

    terminv strange                                 ∎

  strange-lemma : Terminates strange ⇔ ¬ Terminates strange
  strange-lemma =
    Terminates strange                                ↝⟨ record { to   = λ { (_ , rec p) → _ , p }
                                                                ; from = Σ-map _ rec
                                                                } ⟩
    Terminates (terminv (var v-p) [ v-p ← strange ])  ↔⟨ ≡⇒↝ bijection (by subst-lemma) ⟩
    Terminates (terminv strange)                      ↝⟨ terminv-lemma strange-closed ⟩
    ¬ Terminates strange                              □

  contradiction : ⊥
  contradiction = ¬[⇔¬] strange-lemma

-- A variant of the statement above.

extensional-halting-problem′ :
  ¬ ∃ λ halts →
      Closed halts
        ×
      ∀ p → Closed p →
        ∃ λ (b : Bool) →
          apply halts (lambda v-underscore p) ⇓ ⌜ b ⌝
            ×
          if b then Terminates p else (¬ Terminates p)
extensional-halting-problem′ (halts , cl , hyp) =
  extensional-halting-problem
    ( halts
    , cl
    , λ _ cl-p → ⇓→⇓true   cl-p
               , ¬⇓→⇓false cl-p
    )
  where
  ⇓→⇓true : ∀ {p} → Closed p → Terminates p →
            apply halts (lambda v-underscore p) ⇓ ⌜ true ⦂ Bool ⌝
  ⇓→⇓true {p} cl p⇓ with hyp p cl
  ... | true ,  halts⇓true , _   = halts⇓true
  ... | false , _          , ¬p⇓ = ⊥-elim (¬p⇓ p⇓)

  ¬⇓→⇓false :
    ∀ {p} → Closed p → ¬ Terminates p →
    apply halts (lambda v-underscore p) ⇓ ⌜ false ⦂ Bool ⌝
  ¬⇓→⇓false {p} cl ¬p⇓ with hyp p cl
  ... | false ,  halts⇓false , _  = halts⇓false
  ... | true  , _            , p⇓ = ⊥-elim (¬p⇓ p⇓)

-- And another variant.

extensional-halting-problem″ :
  ¬ ∃ λ halts →
      Closed halts
        ×
      ∀ p → Closed p →
        ∥ (∃ λ (b : Bool) →
             apply halts (lambda v-underscore p) ⇓ ⌜ b ⌝
               ×
             if b then Terminates p else (¬ Terminates p)) ∥
extensional-halting-problem″ (halts , cl , hyp) =
  extensional-halting-problem
    ( halts
    , cl
    , λ _ cl-p → ⇓→⇓true cl-p , ¬⇓→⇓false cl-p
    )
  where
  ⇓→⇓true : ∀ {p} → Closed p → Terminates p →
            apply halts (lambda v-underscore p) ⇓ ⌜ true ⦂ Bool ⌝
  ⇓→⇓true cl p⇓ =
    flip (Trunc.rec ⇓-propositional) (hyp _ cl) λ where
      (false , _          , ¬p⇓) → ⊥-elim (¬p⇓ p⇓)
      (true  , halts⇓true , _)   → halts⇓true

  ¬⇓→⇓false :
    ∀ {p} → Closed p → ¬ Terminates p →
    apply halts (lambda v-underscore p) ⇓ ⌜ false ⦂ Bool ⌝
  ¬⇓→⇓false cl ¬p⇓ =
    flip (Trunc.rec ⇓-propositional) (hyp _ cl) λ where
      (true  , _           , p⇓) → ⊥-elim (¬p⇓ p⇓)
      (false , halts⇓false , _)  → halts⇓false

------------------------------------------------------------------------
-- The intensional halting problem with arbitrary or non-standard
-- coding relations

-- A "termination inversion" function, parametrised by a solution to
-- the (generalised) intensional halting problem of self application.

terminv : Exp → Exp
terminv halts =
  lambda v-x
    (χ.if apply halts (var v-x)
     then loop
     else ⌜ zero ⌝)

-- A generalised variant of the intensional halting problem of
-- self-application is not decidable. This variant replaces the coding
-- function for expressions with an arbitrary relation, restricted so
-- that codes have to be values. Furthermore the statement is changed
-- to include the assumption that there is a code for a certain
-- "strange" program.

generalised-intensional-halting-problem-of-self-application :
  (Code : Exp → ∃ Value → Type) →
  ¬ ∃ λ halts →
      Closed halts
        ×
      ∃ (Code (terminv halts))
        ×
      ∀ p c → Closed p → Code p c →
        let c′ = proj₁ c in
        (Terminates (apply p c′) →
           apply halts c′ ⇓ ⌜ true ⦂ Bool ⌝)
          ×
        (¬ Terminates (apply p c′) →
           apply halts c′ ⇓ ⌜ false ⦂ Bool ⌝)
generalised-intensional-halting-problem-of-self-application
  Code (halts , cl , (code-strange , cd) , hyp) =
  contradiction
  where
  terminv-lemma : ∀ p c → Closed p → Code p c →
                  Terminates (apply (terminv halts) (proj₁ c))
                    ⇔
                  ¬ Terminates (apply p (proj₁ c))
  terminv-lemma p (c , c-vl) cl-p cd-p =
    record { to = to; from = from }
    where
    to : Terminates (apply (terminv halts) c) →
         ¬ Terminates (apply p c)
    to (_ , apply lambda _ (case _ here [] loop⇓)) p⇓ =
      ¬loop⇓ (_ , loop⇓)

    to (_ , apply lambda _ (case _ (there _ (there _ ())) _  _)) p⇓

    to (_ , apply lambda rep-p⇓
              (case halts⇓false′ (there _ here) [] _)) p⇓ =
      C.distinct-codes→distinct-names (λ ()) $
        proj₁ $ cancel-const $
          ⇓-deterministic
            (proj₁ (hyp p (c , c-vl) cl-p cd-p) p⇓)
            halts⇓false
      where
      halts⇓false : apply halts c ⇓ ⌜ false ⦂ Bool ⌝
      halts⇓false
        rewrite sym $ values-only-compute-to-themselves c-vl rep-p⇓ =
        subst (λ e → apply e _ ⇓ _)
              (subst-closed _ _ cl)
              halts⇓false′

    from : ¬ Terminates (apply p c) →
           Terminates (apply (terminv halts) c)
    from ¬p⇓ =
      _ , apply lambda (values-compute-to-themselves c-vl)
            (case halts⇓false
                  (there (C.distinct-codes→distinct-names (λ ())) here)
                  []
                  (const []))
      where
      halts⇓false : apply (halts [ v-x ← c ]) c ⇓
                    ⌜ false ⦂ Bool ⌝
      halts⇓false =
        subst (λ e → apply e _ ⇓ _)
              (sym $ subst-closed _ _ cl)
              (proj₂ (hyp p (c , c-vl) cl-p cd-p) ¬p⇓)

  strange : Exp
  strange = apply (terminv halts) (proj₁ code-strange)

  terminv-closed : Closed (terminv halts)
  terminv-closed =
    Closed′-closed-under-lambda $
    if-then-else-closed
      (Closed′-closed-under-apply
         (Closed→Closed′ cl)
         (Closed′-closed-under-var (inj₁ refl)))
      (Closed→Closed′ loop-closed)
      (Closed→Closed′ $ rep-closed zero)

  strange-lemma : Terminates strange ⇔ ¬ Terminates strange
  strange-lemma =
    terminv-lemma
      (terminv halts) code-strange
      terminv-closed cd

  contradiction : ⊥
  contradiction = ¬[⇔¬] strange-lemma

-- A coding relation: An expression e that terminates is encoded by
-- the representation of true, and an expression e that does not
-- terminate is encoded by the representation of false.

⇓-coding : Exp → ∃ Value → Type
⇓-coding e (c , _) =
  Terminates e × c ≡ ⌜ true ⦂ Bool ⌝
    ⊎
  ¬ Terminates e × c ≡ ⌜ false ⦂ Bool ⌝

-- When this coding relation is used the intensional halting problem
-- with zero arguments is decidable.

intensional-halting-problem₀-with-⇓-coding :
  ∃ λ halts →
    Closed halts
      ×
    ∀ p (c@(c′ , _) : ∃ Value) → Closed p → ⇓-coding p c →
      (Terminates p → apply halts c′ ⇓ ⌜ true ⦂ Bool ⌝)
        ×
      (¬ Terminates p → apply halts c′ ⇓ ⌜ false ⦂ Bool ⌝)
intensional-halting-problem₀-with-⇓-coding =
    halts
  , halts-closed
  , halts-correct
  where
  halts : Exp
  halts =
    lambda v-p
      (case (var v-p)
         (branch c-true  [] ⌜ true  ⦂ Bool ⌝ ∷
          branch c-false [] ⌜ false ⦂ Bool ⌝ ∷
          []))

  halts-closed : Closed halts
  halts-closed = from-⊎ (closed? halts)

  halts-correct :
    ∀ p (c@(c′ , _) : ∃ Value) → Closed p → ⇓-coding p c →
    (Terminates p → apply halts c′ ⇓ ⌜ true ⦂ Bool ⌝)
      ×
    (¬ Terminates p → apply halts c′ ⇓ ⌜ false ⦂ Bool ⌝)
  halts-correct _ (.(⌜ true ⌝) , _) _ (inj₁ (p⇓ , refl)) =
      (λ _   → apply lambda (rep⇓rep (true ⦂ Bool))
                 (case (rep⇓rep (true ⦂ Bool)) here []
                    (rep⇓rep (true ⦂ Bool))))
    , (λ ¬p⇓ → ⊥-elim (¬p⇓ p⇓))

  halts-correct _ (.(⌜ false ⌝) , _) _ (inj₂ (¬p⇓ , refl)) =
      (λ p⇓ → ⊥-elim (¬p⇓ p⇓))
    , (λ _   → apply lambda (rep⇓rep (false ⦂ Bool))
                 (case (rep⇓rep (false ⦂ Bool)) (there (λ ()) here) []
                    (rep⇓rep (false ⦂ Bool))))

------------------------------------------------------------------------
-- The intensional halting problem

-- The intensional halting problem of self-application. (This
-- definition is not used below.)

Intensional-halting-problem-of-self-application : Closed-exp →Bool
Intensional-halting-problem-of-self-application =
  as-function-to-Bool₁ (λ { (e , _) → Terminates (apply e ⌜ e ⌝) })

-- The intensional halting problem of self-application is not
-- decidable.

intensional-halting-problem-of-self-application :
  ¬ ∃ λ halts →
      Closed halts
        ×
      ∀ p → Closed p →
        (Terminates (apply p ⌜ p ⌝) →
           apply halts ⌜ p ⌝ ⇓ ⌜ true ⦂ Bool ⌝)
          ×
        (¬ Terminates (apply p ⌜ p ⌝) →
           apply halts ⌜ p ⌝ ⇓ ⌜ false ⦂ Bool ⌝)
intensional-halting-problem-of-self-application
  (halts , cl , hyp) =
  generalised-intensional-halting-problem-of-self-application
     ⌜⌝-Code
     ( halts
     , cl
     , ( ( ⌜ terminv halts ⌝
         , const→value (rep-const (terminv halts))
         )
       , refl
       )
     , λ { p _ cl-p refl → hyp p cl-p }
     )
  where
  ⌜⌝-Code : Exp → ∃ Value → Type
  ⌜⌝-Code e (c , _) = ⌜ e ⌝ ≡ c

-- The intensional halting problem with one argument is not decidable.

intensional-halting-problem₁ :
  ¬ ∃ λ halts →
      Closed halts
        ×
      ∀ p x → Closed p → Closed x →
        (Terminates (apply p ⌜ x ⌝) →
           apply halts ⌜ p , x ⌝ ⇓ ⌜ true ⦂ Bool ⌝)
          ×
        (¬ Terminates (apply p ⌜ x ⌝) →
           apply halts ⌜ p , x ⌝ ⇓ ⌜ false ⦂ Bool ⌝)
intensional-halting-problem₁ (halts , cl , hyp) =
  intensional-halting-problem-of-self-application
    ( halts′
    , cl′
    , λ p cl-p → Σ-map (lemma p true ∘_) (lemma p false ∘_)
                       (hyp p p cl-p cl-p)
    )
  where
  arg    = const c-pair (var v-p ∷ var v-p ∷ [])
  halts′ = lambda v-p (apply halts arg)

  cl′ : Closed halts′
  cl′ =
    Closed′-closed-under-lambda $
    Closed′-closed-under-apply
      (Closed→Closed′ cl)
      (from-⊎ (closed′? arg (v-p ∷ [])))

  lemma : (p : Exp) (b : Bool) →
          apply halts ⌜ p , p ⌝ ⇓ ⌜ b ⌝ →
          apply halts′ ⌜ p ⌝ ⇓ ⌜ b ⌝
  lemma p b halts⇓ =
    apply halts′ ⌜ p ⌝                         ⟶⟨ apply lambda (rep⇓rep p) ⟩
    apply ⟨ halts [ v-p ← ⌜ p ⌝ ] ⟩ ⌜ p , p ⌝  ≡⟨ ⟨by⟩ (subst-closed _ _ cl) ⟩⟶
    apply halts ⌜ p , p ⌝                      ⇓⟨ halts⇓ ⟩■
    ⌜ b ⌝

-- The intensional halting problem with zero arguments is not
-- decidable.

intensional-halting-problem₀ :
  ¬ ∃ λ halts →
      Closed halts
        ×
      ∀ p → Closed p →
        (Terminates p → apply halts ⌜ p ⌝ ⇓ ⌜ true ⦂ Bool ⌝)
          ×
        (¬ Terminates p → apply halts ⌜ p ⌝ ⇓ ⌜ false ⦂ Bool ⌝)
intensional-halting-problem₀ (halts , cl , hyp) =
  intensional-halting-problem-of-self-application
    ( halts′
    , cl′
    , λ p cl-p → Σ-map (lemma p true ∘_) (lemma p false ∘_)
                       (hyp (apply p ⌜ p ⌝)
                            (Closed′-closed-under-apply
                               (Closed→Closed′ cl-p)
                               (Closed→Closed′ (rep-closed p))))
    )
  where
  halts′ =
    lambda v-p (apply halts (
       const c-apply (var v-p ∷ apply internal-code (var v-p) ∷ [])))

  cl′ : Closed halts′
  cl′ =
    Closed′-closed-under-lambda $
    Closed′-closed-under-apply
      (Closed→Closed′ cl)
      (Closed′-closed-under-const
         (λ { _ (inj₁ refl) →
                Closed′-closed-under-var (inj₁ refl)

            ; _ (inj₂ (inj₁ refl)) →
                Closed′-closed-under-apply
                  (Closed→Closed′ internal-code-closed)
                  (Closed′-closed-under-var (inj₁ refl))

            ; _ (inj₂ (inj₂ ()))
            }))

  abstract

    lemma : (p : Exp) (b : Bool) →
            apply halts ⌜ Exp.apply p ⌜ p ⌝ ⌝ ⇓ ⌜ b ⌝ →
            apply halts′ ⌜ p ⌝ ⇓ ⌜ b ⌝
    lemma p b halts⇓ =
      apply halts′ ⌜ p ⌝                                              ⟶⟨ apply lambda (rep⇓rep p) ⟩

      apply ⟨ halts [ v-p ← ⌜ p ⌝ ] ⟩ (const c-apply (
        ⌜ p ⌝ ∷ apply (internal-code [ v-p ← ⌜ p ⌝ ]) ⌜ p ⌝ ∷ []))    ≡⟨ ⟨by⟩ (subst-closed _ _ cl) ⟩⟶

      apply halts (const c-apply (
        ⌜ p ⌝ ∷ apply ⟨ internal-code [ v-p ← ⌜ p ⌝ ] ⟩ ⌜ p ⌝ ∷ []))  ≡⟨ ⟨by⟩ (subst-closed v-p ⌜ p ⌝ internal-code-closed) ⟩⟶

      apply halts (const c-apply (
        ⌜ p ⌝ ∷ apply internal-code ⌜ p ⌝ ∷ []))                      ⟶⟨ []⇓ (apply→ ∙) (const (rep⇓rep p ∷ internal-code-correct p ∷ [])) ⟩

      apply halts (const c-apply (⌜ p ⌝ ∷ ⌜ ⌜ p ⌝ ⦂ Exp ⌝ ∷ []))      ⟶⟨⟩

      apply halts ⌜ Exp.apply p ⌜ p ⌝ ⌝                               ⇓⟨ halts⇓ ⟩■

      ⌜ b ⌝

-- Two statements of the intensional halting problem with zero
-- arguments.

Intensional-halting-problem₀₁ : Closed-exp →Bool
Intensional-halting-problem₀₁ =
  as-function-to-Bool₁ (Terminates ∘ proj₁)

Intensional-halting-problem₀₂ : Closed-exp →Bool
Intensional-halting-problem₀₂ =
  as-function-to-Bool₂ (Terminates ∘ proj₁) Terminates-propositional

-- The first variant is not decidable.

intensional-halting-problem₀₁ :
  ¬ Decidable Intensional-halting-problem₀₁
intensional-halting-problem₀₁ (halts , cl , hyp , _) =
  intensional-halting-problem₀
    ( halts
    , cl
    , λ p cl-p →
        (λ p⇓ →
           apply halts ⌜ p ⌝  ⇓⟨ hyp (p , cl-p) true ((λ _ → refl) , λ ¬p⇓ → ⊥-elim (¬p⇓ p⇓)) ⟩■
           ⌜ true ⦂ Bool ⌝) ,
        λ ¬p⇓ →
          apply halts ⌜ p ⌝  ⇓⟨ hyp (p , cl-p) false ((λ p⇓ → ⊥-elim (¬p⇓ p⇓)) , λ _ → refl) ⟩■
          ⌜ false ⦂ Bool ⌝
    )

-- The second variant is not decidable.

intensional-halting-problem₀₂ :
  ¬ Decidable Intensional-halting-problem₀₂
intensional-halting-problem₀₂ (halts , cl , hyp , _) =
  intensional-halting-problem₀
    ( halts
    , cl
    , λ p cl-p →
          (λ p⇓  →
             apply halts ⌜ p ⌝  ⇓⟨ hyp (p , cl-p) true (inj₁ (p⇓  , refl)) ⟩■
             ⌜ true ⦂ Bool ⌝)
        , (λ ¬p⇓ →
             apply halts ⌜ p ⌝  ⇓⟨ hyp (p , cl-p) false (inj₂ (¬p⇓ , refl)) ⟩■
             ⌜ false ⦂ Bool ⌝)
    )

-- Under the assumption of excluded middle one can prove that
-- Intensional-halting-problem₀₁ and Intensional-halting-problem₀₂ are
-- pointwise equal.

Intensional-halting-problem₀₂→Intensional-halting-problem₀₁ :
  ∀ {e b} →
  proj₁ Intensional-halting-problem₀₂ [ e ]= b →
  proj₁ Intensional-halting-problem₀₁ [ e ]= b
Intensional-halting-problem₀₂→Intensional-halting-problem₀₁
  (inj₁ (e⇓ , refl)) = (λ _ → refl) , (⊥-elim ∘ (_$ e⇓))
Intensional-halting-problem₀₂→Intensional-halting-problem₀₁
  (inj₂ (¬e⇓ , refl)) = (⊥-elim ∘ ¬e⇓) , λ _ → refl

Intensional-halting-problem₀₁→Intensional-halting-problem₀₂ :
  (excluded-middle : (P : Type) → Is-proposition P → Dec P) →
  ∀ {e} b →
  proj₁ Intensional-halting-problem₀₁ [ e ]= b →
  proj₁ Intensional-halting-problem₀₂ [ e ]= b
Intensional-halting-problem₀₁→Intensional-halting-problem₀₂ em =
  λ where
    true (_ , ¬¬e⇓) →
      inj₁ ( double-negation-elimination
               Terminates-propositional
               (Bool.true≢false ∘ ¬¬e⇓)
           , refl
           )
    false (¬e⇓ , _) →
      inj₂ ( Bool.true≢false ∘ sym ∘ ¬e⇓
           , refl
           )
  where
  double-negation-elimination :
    {P : Type} → Is-proposition P → ¬ ¬ P → P
  double-negation-elimination P-prop ¬¬p =
    case em _ P-prop of λ where
      (inj₁ p)  → p
      (inj₂ ¬p) → ⊥-elim (¬¬p ¬p)

------------------------------------------------------------------------
-- "Half of the halting problem"

-- If a (correct) self-interpreter can be implemented, then "half of
-- the halting problem" is computable.

half-of-the-halting-problem :
  (eval : Exp) →
  Closed eval →
  (∀ p v → Closed p → p ⇓ v → apply eval ⌜ p ⌝ ⇓ ⌜ v ⌝) →
  (∀ p → Closed p → ¬ Terminates p →
     ¬ Terminates (apply eval ⌜ p ⌝)) →
  ∃ λ halts →
      Closed halts
        ×
      ∀ p → Closed p →
        (Terminates p → apply halts ⌜ p ⌝ ⇓ ⌜ true ⦂ Bool ⌝)
          ×
        (¬ Terminates p → ¬ Terminates (apply halts ⌜ p ⌝))
half-of-the-halting-problem eval cl eval⇓ eval¬⇓ =
  halts , cl′ , λ p cl-p → lemma₁ p cl-p , lemma₂ p cl-p
  module Half-of-the-halting-problem where
  halts = lambda v-p (apply (lambda v-underscore ⌜ true ⦂ Bool ⌝)
                            (apply eval (var v-p)))

  cl′ : Closed halts
  cl′ =
    Closed′-closed-under-lambda $
    Closed′-closed-under-apply
      (from-⊎ (closed′? (lambda v-underscore ⌜ true ⦂ Bool ⌝) _))
      (Closed′-closed-under-apply
        (Closed→Closed′ cl)
        (Closed′-closed-under-var (inj₁ refl)))

  lemma₁ : ∀ p → Closed p → Terminates p →
           apply halts ⌜ p ⌝ ⇓ ⌜ true ⦂ Bool ⌝
  lemma₁ p cl-p (v , p⇓v) =
    apply halts ⌜ p ⌝                             ⟶⟨ apply lambda (rep⇓rep p) ⟩

    apply (lambda v-underscore ⌜ true ⦂ Bool ⌝)
          (apply ⟨ eval [ v-p ← ⌜ p ⌝ ] ⟩ ⌜ p ⌝)  ≡⟨ ⟨by⟩ (subst-closed _ _ cl) ⟩⟶

    apply (lambda v-underscore ⌜ true ⦂ Bool ⌝)
          (apply eval ⌜ p ⌝)                      ⇓⟨ apply lambda (eval⇓ p v cl-p p⇓v) (rep⇓rep (true ⦂ Bool)) ⟩■

    ⌜ true ⦂ Bool ⌝

  halts-eval-inversion :
    ∀ e →
    Terminates (apply halts e) →
    Terminates (apply eval e)
  halts-eval-inversion e (_ , apply {v₂ = v} lambda e⇓
                           (apply {v₂ = v₂} _ eval⇓ _)) =
    _ , (apply eval e                ⟶⟨ []⇓ (apply→ ∙) e⇓ ⟩
         apply eval v                ≡⟨ by (subst-closed _ _ cl) ⟩⟶
         apply (eval [ v-p ← v ]) v  ⇓⟨ eval⇓ ⟩■
         v₂)

  lemma₂ : ∀ p → Closed p →
           ¬ Terminates p →
           ¬ Terminates (apply halts ⌜ p ⌝)
  lemma₂ p cl-p ¬p⇓ =
    Terminates (apply halts ⌜ p ⌝)  ↝⟨ halts-eval-inversion ⌜ p ⌝ ⟩
    Terminates (apply eval ⌜ p ⌝)   ↝⟨ eval¬⇓ p cl-p ¬p⇓ ⟩□
    ⊥                               □

-- Two statements of "half of the halting problem".

Half-of-the-halting-problem₁ : Closed-exp ⇀ Bool
Half-of-the-halting-problem₁ =
  as-partial-function-to-Bool₁ (Terminates ∘ proj₁)

Half-of-the-halting-problem₂ : Closed-exp ⇀ Bool
Half-of-the-halting-problem₂ =
  as-partial-function-to-Bool₂
    (Terminates ∘ proj₁)
    Terminates-propositional

-- If a (correct) self-interpreter can be implemented, then
-- Half-of-the-halting-problem₂ is computable.

half-of-the-halting-problem₂ :
  (eval : Exp) →
  Closed eval →
  (∀ p v → Closed p → p ⇓ v → apply eval ⌜ p ⌝ ⇓ ⌜ v ⌝) →
  (∀ p v → Closed p → apply eval ⌜ p ⌝ ⇓ v →
     ∃ λ v′ → p ⇓ v′ × v ≡ ⌜ v′ ⌝) →
  Computable Half-of-the-halting-problem₂
half-of-the-halting-problem₂ eval cl eval₁ eval₂ =
  H.halts , H.cl′ ,
  (λ { (p , cl-p) .true (p⇓ , refl) → H.lemma₁ p cl-p p⇓ }) ,
  (λ { (p , cl-p) v halts⌜p⌝⇓v → true ,
       Σ-map (_, refl) id (lemma₂ p v cl-p halts⌜p⌝⇓v) })
  where
  eval-inversion :
    ∀ p → Closed p →
    Terminates (apply eval ⌜ p ⌝) →
    Terminates p
  eval-inversion p cl-p = Σ-map id proj₁ ∘ eval₂ p _ cl-p ∘ proj₂

  module H = Half-of-the-halting-problem eval cl eval₁
               (λ { p cl-p ¬p⇓ →
                    Terminates (apply eval ⌜ p ⌝)  ↝⟨ eval-inversion p cl-p ⟩
                    Terminates p                   ↝⟨ ¬p⇓ ⟩□
                    ⊥                              □ })

  lemma₂ : ∀ p v → Closed p → apply H.halts ⌜ p ⌝ ⇓ v →
           Terminates p × v ≡ ⌜ true ⦂ Bool ⌝
  lemma₂ p v cl-p q@(apply lambda _ (apply lambda _ (const []))) =
      (                                  $⟨ _ , q ⟩
       Terminates (apply H.halts ⌜ p ⌝)  ↝⟨ H.halts-eval-inversion ⌜ p ⌝ ⟩
       Terminates (apply eval ⌜ p ⌝)     ↝⟨ eval-inversion p cl-p ⟩□
       Terminates p                      □)
    , refl

------------------------------------------------------------------------
-- Halting with zero

-- If the expression terminates with ⌜ zero ⌝ as the result, then this
-- (total partial) function returns true. If the expression does not
-- terminate with ⌜ zero ⌝ as the result, then the function returns
-- false.

Halts-with-zero : Closed-exp →Bool
Halts-with-zero =
  as-function-to-Bool₁ (λ { (e , _) → e ⇓ ⌜ zero ⌝ })

-- Halts-with-zero is not decidable.

halts-with-zero : ¬ Decidable Halts-with-zero
halts-with-zero =
  Reduction→¬Computable→¬Computable
    (proj₁ Intensional-halting-problem₀₁) (proj₁ Halts-with-zero) red
    intensional-halting-problem₀₁
  where
  red : Reduction (proj₁ Intensional-halting-problem₀₁)
                  (proj₁ Halts-with-zero)
  red (halts-with-zero , cl , hyp₁ , hyp₂) =
    halts , cl-halts , hyp₁′ , hyp₂′
    where
    argument : Closed-exp → Closed-exp
    argument (p , cl-p) =
        apply (lambda v-x (const c-zero [])) p
      , (Closed′-closed-under-apply
           (from-⊎ (closed′? (lambda v-x (const c-zero [])) []))
           (Closed→Closed′ cl-p))

    coded-argument : Exp → Exp
    coded-argument p = const c-apply (
      ⌜ Exp.lambda v-x (const c-zero []) ⌝ ∷
      p ∷
      [])

    halts : Exp
    halts =
      lambda v-p (apply halts-with-zero (coded-argument (var v-p)))

    cl-halts : Closed halts
    cl-halts =
      Closed′-closed-under-lambda $
      Closed′-closed-under-apply
        (Closed→Closed′ cl)
        (Closed′-closed-under-const λ where
           _ (inj₁ refl)        → Closed→Closed′ $
                                    rep-closed (Exp.lambda v-x (const c-zero []))
           _ (inj₂ (inj₁ refl)) → Closed′-closed-under-var (inj₁ refl)
           _ (inj₂ (inj₂ ())))

    lemma₁ :
      ∀ p b →
      proj₁ Intensional-halting-problem₀₁ [ p ]= b →
      proj₁ Halts-with-zero [ argument p ]= b
    lemma₁ p true (_ , ¬¬p⇓) =
        (λ _ → refl)
      , λ ¬arg-p⇓zero → ¬¬p⇓ λ p⇓ → ¬arg-p⇓zero
                          (proj₁ (argument p)  ⇓⟨ apply lambda (proj₂ p⇓) (const []) ⟩■
                           const c-zero [])

    lemma₁ p false (¬p⇓ , _) =
        (λ { (apply _ p⇓ _) → ¬p⇓ (_ , p⇓) })
      , λ _ → refl

    hyp₁′ : ∀ p b → proj₁ Intensional-halting-problem₀₁ [ p ]= b →
            apply halts ⌜ p ⌝ ⇓ ⌜ b ⌝
    hyp₁′ p b halts[p]=b =
      apply halts ⌜ p ⌝                                                 ⟶⟨ apply lambda (rep⇓rep p) ⟩
      apply ⟨ halts-with-zero [ v-p ← ⌜ p ⌝ ] ⟩ (coded-argument ⌜ p ⌝)  ≡⟨ ⟨by⟩ (subst-closed _ _ cl) ⟩⟶
      apply halts-with-zero (coded-argument ⌜ p ⌝)                      ⟶⟨⟩
      apply halts-with-zero ⌜ argument p ⌝                              ⇓⟨ hyp₁ (argument p) b (lemma₁ p _ halts[p]=b) ⟩■
      ⌜ b ⌝

    pattern coded-argument-⇓ p =
      const (const (const (const (const (const [] ∷ []) ∷ []) ∷ []) ∷
                    const (const [] ∷ const [] ∷ []) ∷
                    []) ∷
             p ∷
             [])

    lemma₂ :
      ∀ p v →
      apply halts ⌜ p ⌝ ⇓ v →
      apply halts-with-zero ⌜ argument p ⌝ ⇓ v
    lemma₂ p v (apply {v₂ = v₂} lambda q r) =
      apply ⟨ halts-with-zero ⟩ ⌜ argument p ⌝                     ≡⟨ ⟨by⟩ (subst-closed _ _ cl) ⟩⟶
      apply (halts-with-zero [ v-p ← v₂ ]) (coded-argument ⌜ p ⌝)  ⟶⟨ []⇓ (apply→ ∙) (coded-argument-⇓ q) ⟩
      apply (halts-with-zero [ v-p ← v₂ ]) (coded-argument v₂)     ⇓⟨ r ⟩■
      v

    hyp₂′ : ∀ p v → apply halts ⌜ p ⌝ ⇓ v →
            ∃ λ v′ →
              proj₁ Intensional-halting-problem₀₁ [ p ]= v′
                ×
              v ≡ ⌜ v′ ⌝
    hyp₂′ p v q =
      Σ-map id
        (Σ-map
           (Σ-map
              (_∘ λ p⇓ → apply lambda (proj₂ p⇓) (const []))
              (_∘ λ ¬p⇓ → λ { (apply lambda p⇓ (const [])) →
                              ¬p⇓ (_ , p⇓) }))
           id) $
        hyp₂ (argument p) v (lemma₂ p v q)

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi


text:
module IrrelevantLambda where

postulate
  A : Set
  P : .A -> Set

f : ._ -> Set
f = λ .x -> P x

f' = λ .(x : _) -> P x

f'' = λ .{x y z : _} -> P x

g : ((.A -> Set) -> Set) -> Set
g k = k f

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: dagit/agda

max_forks_repo_name: dagit/agda


text:
module Golden.InsertionSort where

open import Agda.Builtin.Nat
open import Agda.Builtin.List
open import Agda.Builtin.Bool

insert : Nat -> List Nat -> List Nat
insert a [] = a ∷ []
insert x (a ∷ b) with x < a
... | true = x ∷ a ∷ b
... | false = a ∷ (insert x b)

foldr : ∀ {a b : Set} → (a → b → b) → b → List a -> b
foldr f ini [] = ini
foldr f ini (x ∷ l) = f x (foldr f ini l)

insertSort : List Nat -> List Nat
insertSort = foldr insert []

atDef : ∀ {a : Set} → a → List a -> Nat -> a
atDef def (x ∷ l) zero = x
atDef def (x ∷ l) (suc ix) = atDef def l ix
atDef def _ _ = def

lst : List Nat
lst = 4 ∷ 2 ∷ 7 ∷ []

slst : List Nat
slst = insertSort lst

l0 : Nat
l0 = atDef 0 slst 0

l1 : Nat
l1 = atDef 0 slst 1

l2 : Nat
l2 = atDef 0 slst 2

max_stars_repo_name: agda/agda-ocaml

max_issues_repo_name: agda/agda-ocaml

max_forks_repo_name: agda/agda-ocaml


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Universe levels
------------------------------------------------------------------------

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

module Level where

-- Levels.

open import Agda.Primitive as Prim public
  using    (Level; _⊔_)
  renaming (lzero to zero; lsuc to suc)

-- Lifting.

record Lift {a} ℓ (A : Set a) : Set (a ⊔ ℓ) where
  constructor lift
  field lower : A

open Lift public

-- Synonyms

0ℓ : Level
0ℓ = zero


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.MonoidSolver.Solver where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure

open import Cubical.Data.FinData using (Fin)
open import Cubical.Data.Nat using (ℕ)
open import Cubical.Data.List
open import Cubical.Data.Vec using (Vec; lookup)

open import Cubical.Algebra.Monoid

open import Cubical.Algebra.MonoidSolver.MonoidExpression

private
  variable
    ℓ : Level

module Eval (M : Monoid ℓ) where
  open MonoidStr (snd M)

  Env : ℕ → Type ℓ
  Env n = Vec ⟨ M ⟩ n

  -- evaluation of an expression (without normalization)
  ⟦_⟧ : ∀{n} → Expr ⟨ M ⟩ n → Env n → ⟨ M ⟩
  ⟦ ε⊗ ⟧ v      = ε
  ⟦ ∣ i ⟧ v     = lookup i v
  ⟦ e₁ ⊗ e₂ ⟧ v = ⟦ e₁ ⟧ v · ⟦ e₂ ⟧ v

  NormalForm : ℕ → Type _
  NormalForm n = List (Fin n)

  -- normalization of an expression
  normalize : ∀{n} → Expr ⟨ M ⟩ n → NormalForm n
  normalize (∣ i)     = i ∷ []
  normalize ε⊗        = []
  normalize (e₁ ⊗ e₂) = (normalize e₁) ++ (normalize e₂)

  -- evaluation of normalform
  eval : ∀ {n} → NormalForm n → Env n → ⟨ M ⟩
  eval [] v       = ε
  eval (x ∷ xs) v = (lookup x v) · (eval xs v)

  -- some calculation
  evalIsHom : ∀ {n} (x y : NormalForm n) (v : Env n)
            → eval (x ++ y) v ≡ eval x v · eval y v
  evalIsHom [] y v       = sym (·IdL _)
  evalIsHom (x ∷ xs) y v =
    cong (λ m → (lookup x v) · m) (evalIsHom xs y v) ∙ ·Assoc _ _ _

module EqualityToNormalform (M : Monoid ℓ) where
  open Eval M
  open MonoidStr (snd M)

  -- proof that evaluation of an expression is invariant under normalization
  isEqualToNormalform : (n : ℕ)
                      → (e : Expr ⟨ M ⟩ n)
                      → (v : Env n)
                      → eval (normalize e) v ≡ ⟦ e ⟧ v
  isEqualToNormalform n (∣ i) v     = ·IdR _
  isEqualToNormalform n ε⊗ v        = refl
  isEqualToNormalform n (e₁ ⊗ e₂) v =
    eval ((normalize e₁) ++ (normalize e₂)) v         ≡⟨ evalIsHom (normalize e₁) (normalize e₂) v ⟩
    (eval (normalize e₁) v) · (eval (normalize e₂) v) ≡⟨ cong₂ _·_ (isEqualToNormalform n e₁ v) (isEqualToNormalform n e₂ v) ⟩
    ⟦ e₁ ⟧ v · ⟦ e₂ ⟧ v                               ∎

  solve : {n : ℕ}
        → (e₁ e₂ : Expr ⟨ M ⟩ n)
        → (v : Env n)
        → (p : eval (normalize e₁) v ≡ eval (normalize e₂) v)
        → ⟦ e₁ ⟧ v ≡ ⟦ e₂ ⟧ v
  solve e₁ e₂ v p =
    ⟦ e₁ ⟧ v              ≡⟨ sym (isEqualToNormalform _ e₁ v) ⟩
    eval (normalize e₁) v ≡⟨ p ⟩
    eval (normalize e₂) v ≡⟨ isEqualToNormalform _ e₂ v ⟩
    ⟦ e₂ ⟧ v              ∎

solve : (M : Monoid ℓ)
        {n : ℕ} (e₁ e₂ : Expr ⟨ M ⟩ n) (v : Eval.Env M n)
        (p :  Eval.eval M (Eval.normalize M e₁) v ≡ Eval.eval M (Eval.normalize M e₂) v)
        → _
solve M = EqualityToNormalform.solve M

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

module Cubical.Homotopy.Base where

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

private
  variable
    ℓ ℓ' : Level

_∼_ : {X : Type ℓ} {Y : X → Type ℓ'} → (f g : (x : X) → Y x) → Type (ℓ-max ℓ ℓ')
_∼_ {X = X} f g = (x : X) → f x ≡ g x

funExt∼ : {X : Type ℓ} {Y : X → Type ℓ'} {f g : (x : X) → Y x} (H : f ∼ g) → f ≡ g
funExt∼ = funExt

∼-refl : {X : Type ℓ} {Y : X → Type ℓ'} {f : (x : X) → Y x} → f ∼ f
∼-refl {f = f} = λ x → refl {x = f x}

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 --cubical --safe --postfix-projections #-}

module Categories.Exercises where

open import Prelude
open import Categories

open Category ⦃ ... ⦄
open import Categories.Product
open Product public
open HasProducts ⦃ ... ⦄ public

-- module _ {ℓ₁} {ℓ₂} ⦃ c : Category ℓ₁ ℓ₂ ⦄ ⦃ hp : HasProducts c ⦄ where
--   ex17 : (t : Terminal) (x : Ob) → Product.obj (product (fst t) x) ≅ x
--   ex17 t x .fst = proj₂ (product (fst t) x)
--   ex17 t x .snd .fst = ump (product (fst t) x) (t .snd .fst) Id .fst
--   ex17 t x .snd .snd .fst = let p = ump (product (fst t) x) (t .snd .fst) Id .snd .snd ({!!} , {!!}) in {!!}
--   ex17 t x .snd .snd .snd = {!!}

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Multiplication
open import Semirings.Definition
open import Rings.Definition
open import Setoids.Setoids

module Numbers.Integers.RingStructure.Ring where

open import Numbers.Integers.Definition public
open import Numbers.Integers.Addition public
open import Numbers.Integers.Multiplication public

*ZCommutative : (a b : ℤ) → a *Z b ≡ b *Z a
*ZCommutative (nonneg x) (nonneg y) = applyEquality nonneg (multiplicationNIsCommutative x y)
*ZCommutative (nonneg zero) (negSucc y) = refl
*ZCommutative (nonneg (succ x)) (negSucc y) = refl
*ZCommutative (negSucc x) (nonneg zero) = refl
*ZCommutative (negSucc x) (nonneg (succ y)) = refl
*ZCommutative (negSucc x) (negSucc y) = applyEquality nonneg (multiplicationNIsCommutative (succ x) (succ y))

*ZleftIdent : (a : ℤ) → (nonneg 1) *Z a ≡ a
*ZleftIdent (nonneg x) = applyEquality nonneg (Semiring.commutative ℕSemiring x 0)
*ZleftIdent (negSucc x) = applyEquality negSucc (transitivity (Semiring.commutative ℕSemiring (x +N 0) 0) (Semiring.commutative ℕSemiring x 0))

*ZrightIdent : (a : ℤ) → a *Z (nonneg 1) ≡ a
*ZrightIdent (nonneg x) = applyEquality nonneg (Semiring.productOneRight ℕSemiring x)
*ZrightIdent (negSucc x) = applyEquality negSucc (transitivity (Semiring.commutative ℕSemiring (x +N 0) 0) (Semiring.commutative ℕSemiring x 0))

*ZZeroLeft : (a : ℤ) → nonneg 0 *Z a ≡ nonneg 0
*ZZeroLeft (nonneg x) = refl
*ZZeroLeft (negSucc x) = refl

*ZZeroRight : (a : ℤ) → a *Z nonneg 0 ≡ nonneg 0
*ZZeroRight (nonneg x) = applyEquality nonneg (Semiring.productZeroRight ℕSemiring x)
*ZZeroRight (negSucc x) = refl

*ZAssociative : (a b c : ℤ) → a *Z (b *Z c) ≡ (a *Z b) *Z c
*ZAssociative (nonneg zero) b c = transitivity (*ZZeroLeft (b *Z c)) (transitivity (equalityCommutative (*ZZeroLeft c)) (applyEquality (_*Z c) (equalityCommutative (*ZZeroLeft b))))
*ZAssociative (nonneg (succ a)) (nonneg zero) c rewrite Semiring.productZeroRight ℕSemiring a | *ZZeroLeft c | Semiring.productZeroRight ℕSemiring a = refl
*ZAssociative (nonneg (succ a)) (nonneg (succ b)) (nonneg zero) rewrite Semiring.productZeroRight ℕSemiring b | Semiring.productZeroRight ℕSemiring (b +N a *N succ b) | Semiring.productZeroRight ℕSemiring a = refl
*ZAssociative (nonneg (succ a)) (nonneg (succ b)) (nonneg (succ c)) = applyEquality nonneg (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ c))
*ZAssociative (nonneg (succ a)) (nonneg (succ b)) (negSucc x) rewrite productDistributes' b (a *N succ b) x | Semiring.+Associative ℕSemiring x (b *N x) ((a *N succ b) *N x) | equalityCommutative (Semiring.+Associative ℕSemiring ((x +N b *N x) +N b) (a *N ((x +N b *N x) +N b)) a) | equalityCommutative (Semiring.+Associative ℕSemiring (x +N b *N x) ((a *N succ b) *N x) (b +N a *N succ b)) | equalityCommutative (Semiring.+Associative ℕSemiring (x +N b *N x) b (a *N ((x +N b *N x) +N b) +N a)) = applyEquality (λ i → negSucc ((x +N b *N x) +N i)) ans
  where
    ans3 : (succ b +N (succ b *N x)) *N a ≡ succ x *N (a *N succ b)
    ans3 rewrite multiplicationNIsCommutative (succ b) x = transitivity (equalityCommutative (Semiring.*Associative ℕSemiring (succ x) (succ b) a)) (applyEquality (succ x *N_) (multiplicationNIsCommutative (succ b) a))
    ans2 : a *N ((x +N b *N x) +N b) +N a ≡ (a *N succ b) +N (a *N succ b) *N x
    ans2 rewrite multiplicationNIsCommutative (a *N succ b) x | Semiring.commutative ℕSemiring (succ b *N x) b | multiplicationNIsCommutative a (b +N (succ b *N x)) | Semiring.commutative ℕSemiring ((b +N (succ b *N x)) *N a) a = ans3
    ans : b +N (a *N ((x +N b *N x) +N b) +N a) ≡ (a *N succ b) *N x +N (b +N a *N succ b)
    ans rewrite Semiring.commutative ℕSemiring ((a *N succ b) *N x) (b +N a *N succ b) | equalityCommutative (Semiring.+Associative ℕSemiring b (a *N succ b) ((a *N succ b) *N x)) = applyEquality (b +N_) ans2
*ZAssociative (nonneg (succ a)) (negSucc b) (nonneg zero) = applyEquality nonneg (Semiring.productZeroRight ℕSemiring a)
*ZAssociative (nonneg (succ a)) (negSucc b) (nonneg (succ c)) = applyEquality negSucc ans
  where
    ans4 : (b +N b *N c) +N (a *N b +N (a *N b) *N c) ≡ (b +N a *N b) +N (b *N c +N (a *N b) *N c)
    ans4 rewrite Semiring.+Associative ℕSemiring (b +N b *N c) (a *N b) ((a *N b) *N c) | Semiring.+Associative ℕSemiring (b +N a *N b) (b *N c) ((a *N b) *N c) = applyEquality (_+N (a *N b) *N c) (transitivity (transitivity (applyEquality (_+N a *N b) (Semiring.commutative ℕSemiring b (b *N c))) (equalityCommutative (Semiring.+Associative ℕSemiring (b *N c) b (a *N b)))) (Semiring.commutative ℕSemiring (b *N c) (b +N a *N b)))
    ans3 : ((b +N b *N c) +N (a *N b +N (a *N b) *N c)) +N ((c +N a *N c) +N a) ≡ ((b +N a *N b) +N (b *N c +N (a *N b) *N c)) +N ((a +N a *N c) +N c)
    ans3 rewrite Semiring.commutative ℕSemiring (c +N a *N c) a | Semiring.commutative ℕSemiring c (a *N c) | Semiring.+Associative ℕSemiring a (a *N c) c = applyEquality (λ i → i +N ((a +N a *N c) +N c)) {(b +N b *N c) +N (a *N b +N (a *N b) *N c)} {(b +N a *N b) +N (b *N c +N (a *N b) *N c)} ans4
    ans2 : (((b +N c *N b) +N (a *N b +N a *N (c *N b))) +N (c +N a *N c)) +N a ≡ (((b +N a *N b) +N (c *N b +N c *N (a *N b))) +N (a +N c *N a)) +N c
    ans2 rewrite multiplicationNIsCommutative c b | multiplicationNIsCommutative c (a *N b) | Semiring.*Associative ℕSemiring a b c | multiplicationNIsCommutative c a = transitivity (equalityCommutative (Semiring.+Associative ℕSemiring ((b +N b *N c) +N (a *N b +N (a *N b) *N c)) (c +N a *N c) a)) (transitivity ans3 (Semiring.+Associative ℕSemiring ((b +N a *N b) +N (b *N c +N (a *N b) *N c)) (a +N a *N c) c))
    ans : succ a *N ((succ c *N b) +N c) +N a ≡ succ c *N ((succ a *N b) +N a) +N c
    ans = transitivity (applyEquality (_+N a) (productDistributes (succ a) (succ c *N b) c)) (transitivity (transitivity (applyEquality (λ i → ((((b +N c *N b) +N i) +N (c +N a *N c)) +N a)) (productDistributes a b (c *N b))) (transitivity ans2 (applyEquality (λ i → (((b +N a *N b) +N i) +N (a +N c *N a)) +N c) (equalityCommutative (productDistributes c b (a *N b)))))) (applyEquality (_+N c) (equalityCommutative (productDistributes (succ c) (succ a *N b) a))))
*ZAssociative (nonneg (succ a)) (negSucc b) (negSucc x) = applyEquality nonneg ans
  where
    ans : succ a *N (succ b *N succ x) ≡ succ ((succ a *N b) +N a) *N succ x
    ans rewrite Semiring.commutative ℕSemiring (succ a *N b) a | multiplicationNIsCommutative (succ a) b = transitivity (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ x)) (applyEquality (_*N succ x) {succ a *N succ b} {succ b *N succ a} (multiplicationNIsCommutative (succ a) (succ b)))
*ZAssociative (negSucc a) (nonneg zero) c rewrite *ZZeroLeft c = refl
*ZAssociative (negSucc a) (nonneg (succ b)) (nonneg zero) rewrite multiplicationNIsCommutative b 0 = refl
*ZAssociative (negSucc a) (nonneg (succ b)) (nonneg (succ c)) = applyEquality negSucc ans
  where
    ans2 : (d : ℕ) → ((succ b *N d) *N a) +N b *N d ≡ d *N ((succ b *N a) +N b)
    ans2 d = transitivity (transitivity (applyEquality (((d +N b *N d) *N a) +N_) (multiplicationNIsCommutative b d)) (applyEquality (_+N d *N b) (transitivity (applyEquality (_*N a) {d +N b *N d} {d *N succ b} (multiplicationNIsCommutative (succ b) d)) (equalityCommutative (Semiring.*Associative ℕSemiring d (succ b) a))))) (equalityCommutative (Semiring.+DistributesOver* ℕSemiring d (succ b *N a) b))
    ans : (succ (c +N b *N succ c) *N a) +N (c +N b *N succ c) ≡ (succ c *N ((succ b *N a) +N b)) +N c
    ans rewrite Semiring.commutative ℕSemiring c (b *N succ c) | Semiring.+Associative ℕSemiring (succ (b *N succ c +N c) *N a) (b *N succ c) c | Semiring.commutative ℕSemiring (b *N succ c) c = applyEquality (_+N c) (ans2 (succ c))
*ZAssociative (negSucc a) (nonneg (succ b)) (negSucc c) = applyEquality nonneg ans
  where
    ans : succ a *N ((succ ((succ b) *N c)) +N b) ≡ (succ (succ b *N a) +N b) *N succ c
    ans rewrite Semiring.commutative ℕSemiring (succ b *N a) b | multiplicationNIsCommutative (succ b) a = transitivity (applyEquality (succ a *N_) (applyEquality succ (transitivity (equalityCommutative (Semiring.+Associative ℕSemiring c (b *N c) b)) (applyEquality (c +N_) (transitivity (transitivity (Semiring.commutative ℕSemiring (b *N c) b) (applyEquality (b +N_) (multiplicationNIsCommutative b c))) (multiplicationNIsCommutative (succ c) b)))))) (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ c))
*ZAssociative (negSucc a) (negSucc b) (nonneg zero) rewrite Semiring.productZeroRight ℕSemiring (b +N a *N succ b) = refl
*ZAssociative (negSucc a) (negSucc b) (nonneg (succ x)) = applyEquality nonneg (transitivity (applyEquality (succ a *N_) ans) (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ x)))
  where
    ans : succ ((succ x *N b) +N x) ≡ (succ b *N succ x)
    ans rewrite Semiring.commutative ℕSemiring (succ x *N b) x | multiplicationNIsCommutative (succ x) b = refl
*ZAssociative (negSucc a) (negSucc b) (negSucc x) = applyEquality negSucc t
  where
    l1 : (a b c d e f g : ℕ) → (a +N b) +N d ≡ e +N (f +N g) → (a +N b) +N (c +N d) ≡ (c +N e) +N (f +N g)
    l1 a b c d e f g pr rewrite Semiring.commutative ℕSemiring c d | Semiring.+Associative ℕSemiring (a +N b) d c | pr | Semiring.commutative ℕSemiring (e +N (f +N g)) c | Semiring.+Associative ℕSemiring c e (f +N g) = refl
    v : (((succ b) *N succ x) *N a) ≡ (succ x) *N (a *N succ b)
    v = transitivity (applyEquality (_*N a) (multiplicationNIsCommutative (succ b) (succ x))) (transitivity (equalityCommutative (Semiring.*Associative ℕSemiring (succ x) (succ b) a)) (applyEquality (succ x *N_) (multiplicationNIsCommutative (succ b) a)))
    u : (a +N (x +N b *N succ x) *N a) +N b *N succ x ≡ (b +N a *N succ b) *N x +N (b +N a *N succ b)
    u = transitivity (transitivity (transitivity (Semiring.commutative ℕSemiring (a +N (x +N b *N succ x) *N a) (b *N succ x)) (transitivity (applyEquality (_+N (a +N (x +N b *N succ x) *N a)) (multiplicationNIsCommutative b (succ x))) (transitivity (applyEquality ((b +N x *N b) +N_) v) (equalityCommutative (productDistributes (succ x) b (a *N succ b)))))) (applyEquality ((b +N a *N succ b) +N_) (multiplicationNIsCommutative x (b +N a *N succ b)))) (Semiring.commutative ℕSemiring (b +N a *N succ b) ((b +N a *N succ b) *N x))
    t : (a +N (x +N b *N succ x) *N a) +N (x +N b *N succ x) ≡ (x +N (b +N a *N succ b) *N x) +N (b +N a *N succ b)
    t = l1 a ((x +N b *N succ x) *N a) x (b *N succ x) ((b +N (a *N succ b)) *N x) b (a *N succ b) u

multLemma : (a b : ℕ) → a *N succ b ≡ a *N b +N a
multLemma a b rewrite multiplicationNIsCommutative a (succ b) | Semiring.commutative ℕSemiring a (b *N a) | multiplicationNIsCommutative a b = refl

negSucc+Nonneg : (a b : ℕ) → negSucc a ≡ negSucc (a +N b) +Z nonneg b
negSucc+Nonneg zero zero = refl
negSucc+Nonneg zero (succ b) = negSucc+Nonneg zero b
negSucc+Nonneg (succ a) zero rewrite Semiring.commutative ℕSemiring a 0 = refl
negSucc+Nonneg (succ a) (succ b) rewrite Semiring.commutative ℕSemiring a (succ b) | Semiring.commutative ℕSemiring b a = negSucc+Nonneg (succ a) b

distLemma : (a b : ℕ) →  negSucc a *Z nonneg b ≡ negSucc ((a +N b *N a) +N b) +Z nonneg (succ a)
distLemma a b rewrite Semiring.commutative ℕSemiring (a +N b *N a) b | Semiring.commutative ℕSemiring a (b *N a) | Semiring.+Associative ℕSemiring b (b *N a) a = transitivity u (transitivity (equalityCommutative (+ZAssociative (negSucc ((b +N b *N a) +N a)) (nonneg a) (nonneg 1))) (applyEquality ((negSucc ((b +N b *N a) +N a)) +Z_) {nonneg a +Z nonneg 1} {nonneg (succ a)} (+ZCommutative (nonneg a) (nonneg 1))))
  where
    v : (a b : ℕ) → negSucc a *Z nonneg b ≡ (negSucc (b +N b *N a)) +Z nonneg 1
    v zero zero = refl
    v zero (succ b) rewrite Semiring.productZeroRight ℕSemiring b = applyEquality negSucc (equalityCommutative (Semiring.sumZeroRight ℕSemiring b))
    v (succ a) zero = refl
    v (succ a) (succ b) = applyEquality negSucc (Semiring.commutative ℕSemiring (succ (a +N b *N succ a)) b)
    u : negSucc a *Z nonneg b ≡ (negSucc ((b +N b *N a) +N a) +Z nonneg a) +Z nonneg 1
    u = transitivity (v a b) (applyEquality (_+Z nonneg 1) (negSucc+Nonneg (b +N b *N a) a))

*ZDistributesOver+Z : (a b c : ℤ) → a *Z (b +Z c) ≡ (a *Z b) +Z (a *Z c)
*ZDistributesOver+Z (nonneg zero) b c rewrite *ZZeroLeft (b +Z c) | *ZZeroLeft b | *ZZeroLeft c = refl
*ZDistributesOver+Z (nonneg (succ a)) (nonneg zero) (nonneg c) rewrite Semiring.productZeroRight ℕSemiring a = refl
*ZDistributesOver+Z (nonneg (succ a)) (nonneg (succ b)) (nonneg c) = applyEquality nonneg (productDistributes (succ a) (succ b) c)
*ZDistributesOver+Z (nonneg (succ a)) (nonneg zero) (negSucc c) rewrite Semiring.productZeroRight ℕSemiring a = refl
*ZDistributesOver+Z (nonneg (succ a)) (nonneg (succ b)) (negSucc zero) rewrite Semiring.productZeroRight ℕSemiring a = t a
  where
    t : (a : ℕ) → nonneg (succ a *N b) ≡ nonneg (succ a *N succ b) +Z negSucc a
    t zero = refl
    t (succ a) = transitivity (+Zinherits b (b +N a *N b)) (transitivity (applyEquality (nonneg b +Z_) (t a)) (transitivity (+ZAssociative (nonneg b) (nonneg (succ (b +N a *N succ b))) (negSucc a)) (applyEquality (_+Z negSucc a) {nonneg b +Z nonneg (succ (b +N a *N succ b))} {nonneg (b +N succ (b +N a *N succ b))} (equalityCommutative (+Zinherits b _)))))
*ZDistributesOver+Z (nonneg (succ a)) (nonneg (succ x)) (negSucc (succ b)) = transitivity (applyEquality ((nonneg (succ a)) *Z_) (+ZCommutative (nonneg x) (negSucc b))) (transitivity (transitivity (*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (nonneg x)) t) (+ZCommutative (negSucc ((b +N a *N succ b) +N a)) (nonneg (x +N a *N succ x))))
  where
    t : negSucc ((b +N a *N b) +N a) +Z nonneg (x +N a *N x) ≡ negSucc ((b +N a *N succ b) +N a) +Z nonneg (x +N a *N succ x)
    t rewrite multLemma a x | multLemma a b | Semiring.+Associative ℕSemiring x (a *N x) a | Semiring.+Associative ℕSemiring b (a *N b) a | Semiring.commutative ℕSemiring (x +N a *N x) a | +Zinherits a (x +N a *N x) | +ZAssociative (negSucc (((b +N a *N b) +N a) +N a)) (nonneg a) (nonneg (x +N a *N x)) = applyEquality (_+Z nonneg (x +N a *N x)) {negSucc ((b +N a *N b) +N a)} {negSucc (((b +N a *N b) +N a) +N a) +Z nonneg a} (negSucc+Nonneg ((b +N a *N b) +N a) a)
*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (nonneg zero) rewrite Semiring.productZeroRight ℕSemiring a = refl
*ZDistributesOver+Z (nonneg (succ a)) (negSucc zero) (nonneg (succ x)) rewrite Semiring.productZeroRight ℕSemiring a = t a x
  where
    t : (a x : ℕ) → nonneg (succ a *N x) ≡ negSucc a +Z nonneg (succ a *N succ x)
    t zero x = refl
    t (succ a) x with t a x
    ... | bl rewrite +Zinherits x (a *N x) | +Zinherits x (x +N a *N x) = transitivity (transitivity (applyEquality (nonneg x +Z_) (+Zinherits x (a *N x))) (+ZCommutative (nonneg x) (nonneg x +Z nonneg (a *N x)))) (transitivity (applyEquality (_+Z nonneg x) bl) (transitivity (equalityCommutative (+ZAssociative (negSucc a) (nonneg (succ x +N a *N succ x)) (nonneg x))) (applyEquality (λ i → negSucc a +Z nonneg i) {succ (x +N a *N succ x) +N x} {x +N succ (x +N a *N succ x)} (Semiring.commutative ℕSemiring (succ (x +N a *N succ x)) x))))
*ZDistributesOver+Z (nonneg (succ a)) (negSucc (succ b)) (nonneg (succ x)) = transitivity (*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (nonneg x)) t
  where
    t : negSucc ((b +N a *N b) +N a) +Z nonneg (x +N a *N x) ≡ negSucc ((b +N a *N succ b) +N a) +Z nonneg (x +N a *N succ x)
    t rewrite multLemma a x | multLemma a b | Semiring.+Associative ℕSemiring x (a *N x) a | Semiring.+Associative ℕSemiring b (a *N b) a | Semiring.commutative ℕSemiring (x +N a *N x) a | +Zinherits a (x +N a *N x) | +ZAssociative (negSucc (((b +N a *N b) +N a) +N a)) (nonneg a) (nonneg (x +N a *N x)) = applyEquality (_+Z nonneg (x +N a *N x)) {negSucc ((b +N a *N b) +N a)} {negSucc (((b +N a *N b) +N a) +N a) +Z nonneg a} (negSucc+Nonneg ((b +N a *N b) +N a) a)
*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (negSucc x) = applyEquality negSucc (transitivity (applyEquality (_+N a) (transitivity (productDistributes (succ a) (succ b) x) (applyEquality (_+N (x +N a *N x)) {succ b +N a *N succ b} {succ (b +N a *N b) +N a} (applyEquality succ u)))) (equalityCommutative (Semiring.+Associative ℕSemiring (succ ((b +N a *N b) +N a)) (succ a *N x) a)))
  where
    u : b +N a *N succ b ≡ (succ a *N b) +N a
    u rewrite multiplicationNIsCommutative a (succ b) | Semiring.commutative ℕSemiring a (b *N a) | multiplicationNIsCommutative b a = Semiring.+Associative ℕSemiring b (a *N b) a
*ZDistributesOver+Z (negSucc a) (nonneg zero) (nonneg x) = refl
*ZDistributesOver+Z (negSucc a) (nonneg zero) (negSucc x) = refl
*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (nonneg zero) rewrite Semiring.commutative ℕSemiring b 0 = refl
*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (nonneg (succ c)) = applyEquality negSucc t
  where
    v : a *N b +N a *N succ c ≡ c *N a +N (a +N b *N a)
    v rewrite multiplicationNIsCommutative b a | Semiring.+Associative ℕSemiring (c *N a) a (a *N b) | Semiring.commutative ℕSemiring (c *N a +N a) (a *N b) | Semiring.commutative ℕSemiring (c *N a) a = applyEquality (λ i → a *N b +N i) (transitivity (multLemma a c) (transitivity (Semiring.commutative ℕSemiring (a *N c) a) (applyEquality (a +N_) (multiplicationNIsCommutative a c))))
    u : (a +N (b +N succ c) *N a) +N b ≡ (a +N c *N a) +N ((a +N b *N a) +N b)
    u rewrite Semiring.+Associative ℕSemiring (a +N c *N a) (a +N b *N a) b | (equalityCommutative (Semiring.+Associative ℕSemiring a (c *N a) (a +N b *N a))) = applyEquality (λ i → (a +N i) +N b) (transitivity (multiplicationNIsCommutative (b +N succ c) a) (transitivity (productDistributes a b (succ c)) v))
    t : (a +N (b +N succ c) *N a) +N (b +N succ c) ≡ succ (((a +N b *N a) +N b) +N ((a +N c *N a) +N c))
    t rewrite Semiring.+Associative ℕSemiring ((a +N (b +N succ c) *N a)) b (succ c) | Semiring.commutative ℕSemiring ((a +N b *N a) +N b) ((a +N c *N a) +N c) | Semiring.commutative ℕSemiring (a +N c *N a) c | equalityCommutative (Semiring.+Associative ℕSemiring (succ c) (a +N c *N a) ((a +N b *N a) +N b)) | Semiring.commutative ℕSemiring (succ c) ((a +N c *N a) +N ((a +N b *N a) +N b)) = applyEquality (_+N succ c) u
*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (negSucc zero) rewrite Semiring.productOneRight ℕSemiring a = distLemma a b
*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (negSucc (succ c)) = transitivity (*ZDistributesOver+Z (negSucc a) (nonneg b) (negSucc c)) (transitivity (applyEquality (_+Z nonneg (succ (c +N a *N succ c))) (distLemma a b)) (transitivity (equalityCommutative (+ZAssociative (negSucc ((a +N b *N a) +N b)) (nonneg (succ a)) (nonneg (succ (c +N a *N succ c))))) (applyEquality (negSucc ((a +N b *N a) +N b) +Z_) {nonneg (succ (a +N succ (c +N a *N succ c)))} {nonneg (succ (succ (c +N a *N succ (succ c))))} (applyEquality nonneg (t (succ a) (succ c))))))
  where
    t : (x y : ℕ) → x +N x *N y ≡ x *N succ y
    t x y = transitivity (Semiring.commutative ℕSemiring x (x *N y)) (equalityCommutative (multLemma x y))
*ZDistributesOver+Z (negSucc a) (negSucc b) (nonneg zero) rewrite Semiring.commutative ℕSemiring (b +N a *N succ b) 0 = refl
*ZDistributesOver+Z (negSucc a) (negSucc zero) (nonneg (succ b)) = transitivity (distLemma a b) (transitivity (+ZCommutative (negSucc ((a +N b *N a) +N b)) (nonneg (succ a))) (applyEquality (λ i → nonneg (succ i) +Z negSucc ((a +N b *N a) +N b)) (equalityCommutative (Semiring.productOneRight ℕSemiring a))))
*ZDistributesOver+Z (negSucc a) (negSucc (succ c)) (nonneg (succ b)) = transitivity (applyEquality (negSucc a *Z_) (+ZCommutative (negSucc c) (nonneg b))) (transitivity (transitivity (*ZDistributesOver+Z (negSucc a) (nonneg b) (negSucc c)) (transitivity (applyEquality (_+Z nonneg (succ (c +N a *N succ c))) (distLemma a b)) (transitivity (equalityCommutative (+ZAssociative (negSucc ((a +N b *N a) +N b)) (nonneg (succ a)) (nonneg (succ (c +N a *N succ c))))) (applyEquality (negSucc ((a +N b *N a) +N b) +Z_) {nonneg (succ (a +N succ (c +N a *N succ c)))} {nonneg (succ (succ (c +N a *N succ (succ c))))} (applyEquality nonneg (t (succ a) (succ c))))))) (+ZCommutative (negSucc ((a +N b *N a) +N b)) (nonneg (succ (succ (c +N a *N succ (succ c)))))))
  where
    t : (x y : ℕ) → x +N x *N y ≡ x *N succ y
    t x y = transitivity (Semiring.commutative ℕSemiring x (x *N y)) (equalityCommutative (multLemma x y))
*ZDistributesOver+Z (negSucc a) (negSucc b) (negSucc c) = applyEquality nonneg (transitivity (applyEquality (λ i → succ a *N (succ i)) (transitivity (applyEquality succ (Semiring.commutative ℕSemiring b c)) (Semiring.commutative ℕSemiring (succ c) b))) (productDistributes (succ a) (succ b) (succ c)))

ℤRing : Ring (reflSetoid ℤ) _+Z_ _*Z_
Ring.additiveGroup ℤRing = ℤGroup
Ring.*WellDefined ℤRing refl refl = refl
Ring.1R ℤRing = nonneg 1
Ring.groupIsAbelian ℤRing {a} {b} = +ZCommutative a b
Ring.*Associative ℤRing {a} {b} {c} = *ZAssociative a b c
Ring.*Commutative ℤRing {a} {b} = *ZCommutative a b
Ring.*DistributesOver+ ℤRing {a} {b} {c} = *ZDistributesOver+Z a b c
Ring.identIsIdent ℤRing {a} = *ZleftIdent a