text:
------------------------------------------------------------------------
-- The SKI encoding into types
------------------------------------------------------------------------

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

module FOmegaInt.Undecidable.Encoding where

open import Data.Context.WellFormed
open import Data.List using ([]; _∷_)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Fin using (Fin; zero; suc; raise)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.ExtraLemmas
open import Relation.Binary.PropositionalEquality hiding ([_])

open import FOmegaInt.Syntax
open import FOmegaInt.Syntax.SingleVariableSubstitution
open import FOmegaInt.Syntax.HereditarySubstitution
open import FOmegaInt.Syntax.Normalization
open import FOmegaInt.Kinding.Canonical
open import FOmegaInt.Undecidable.SK

open Syntax
open ElimCtx
open ContextConversions using (⌞_⌟Ctx)
open RenamingCommutes
open Kinding
open ≡-Reasoning

----------------------------------------------------------------------
-- Support for the encoding: injection of shapes into kinds.

-- For every shape `k' there is a kind `⌈ k ⌉' that erases/simplifies
-- back to `k', i.e. `⌈_⌉' is a right inverse of kind erasure `⌊_⌋'.
--
-- NOTE. The definition here is almost identical to that in
-- FOmegaInt.Typing.Encodings except we inject shapes into `Kind Elim
-- n' rather than `Kind Term n'.

⌈_⌉ : ∀ {n} → SKind → Kind Elim n
⌈ ★     ⌉ = ⌜*⌝
⌈ j ⇒ k ⌉ = Π ⌈ j ⌉ ⌈ k ⌉

⌊⌋∘⌈⌉-id : ∀ {n} k → ⌊ ⌈_⌉ {n} k ⌋ ≡ k
⌊⌋∘⌈⌉-id ★       = refl
⌊⌋∘⌈⌉-id (j ⇒ k) = cong₂ _⇒_ (⌊⌋∘⌈⌉-id j) (⌊⌋∘⌈⌉-id k)

-- The kind `⌈ k ⌉' is well-formed (in any well-formed context).

⌈⌉-kd : ∀ {n} {Γ : Ctx n} k → Γ ctx → Γ ⊢ ⌈ k ⌉ kd
⌈⌉-kd ★       Γ-ctx = kd-⌜*⌝ Γ-ctx
⌈⌉-kd (j ⇒ k) Γ-ctx =
  let ⌈j⌉-kd = ⌈⌉-kd j Γ-ctx
  in kd-Π ⌈j⌉-kd (⌈⌉-kd k (wf-kd ⌈j⌉-kd ∷ Γ-ctx))

-- Injected kinds are stable under application of substitutions.

module InjSubstAppLemmas {T : ℕ → Set} (l : Lift T Term) where
  open Lift l
  open SubstApp l

  ⌈⌉-Kind/ : ∀ {m n} k {σ : Sub T m n} → ⌈ k ⌉ Kind′/ σ ≡ ⌈ k ⌉
  ⌈⌉-Kind/ ★       = refl
  ⌈⌉-Kind/ (j ⇒ k) = cong₂ Π (⌈⌉-Kind/ j) (⌈⌉-Kind/ k)

open Substitution hiding (subst; _[_]; _↑; sub)
open TermSubst termSubst using (varLift; termLift)

open InjSubstAppLemmas varLift public renaming (⌈⌉-Kind/ to ⌈⌉-Kind/Var)

⌈⌉-weaken : ∀ {n} k → weakenKind′ {n} ⌈ k ⌉ ≡ ⌈ k ⌉
⌈⌉-weaken k = ⌈⌉-Kind/Var k

kd-⌈⌉-weaken : ∀ {n} k → weakenElimAsc {n} (kd ⌈ k ⌉) ≡ kd ⌈ k ⌉
kd-⌈⌉-weaken k = cong kd (⌈⌉-weaken k)

kd-⌈⌉-weaken⋆ : ∀ {n k} m → weakenElimAsc⋆ m {n} (kd ⌈ k ⌉) ≡ kd ⌈ k ⌉
kd-⌈⌉-weaken⋆ zero    = refl
kd-⌈⌉-weaken⋆ (suc m) =
  trans (cong weakenElimAsc (kd-⌈⌉-weaken⋆ m)) (kd-⌈⌉-weaken _)

lookup-raise-* : ∀ {n m} {Γ : Ctx n} (E : CtxExt n m) {x} k →
                 lookup Γ x ≡ kd ⌈ k ⌉ →
                 lookup (E ++ Γ) (raise m x) ≡ kd ⌈ k ⌉
lookup-raise-* {_} {m} {Γ} E {x} k hyp = begin
  lookup (E ++ Γ) (raise m x)    ≡⟨ lookup-weaken⋆ m E Γ x ⟩
  weakenElimAsc⋆ m (lookup Γ x)  ≡⟨ cong (weakenElimAsc⋆ m) hyp ⟩
  weakenElimAsc⋆ m (kd ⌈ k ⌉)    ≡⟨ kd-⌈⌉-weaken⋆ m ⟩
  kd ⌈ k ⌉                       ∎
  where

------------------------------------------------------------------------
-- Encoding of SK terms into types

-- The encoding uses 7 type variables:
--
--  2 nullary operators encoding the combinators S and K,
--  1 binary operator encoding application,
--  2 ternary operators encoding the S reduction/expansion laws,
--  2 binary operators encoding the K reduction/expansion laws.
--
-- We define some pattern synonyms for readability of definitions.

|Γ| = 7

pattern x₀ = zero
pattern x₁ = suc zero
pattern x₂ = suc (suc zero)
pattern x₃ = suc (suc (suc zero))
pattern x₄ = suc (suc (suc (suc zero)))
pattern x₅ = suc (suc (suc (suc (suc zero))))
pattern x₆ = suc (suc (suc (suc (suc (suc zero)))))

module _ {n} where

  -- Shorthands to help with the encodings

  v₀ : Elim (1 + n)
  v₀ = var∙ x₀

  v₁ : Elim (2 + n)
  v₁ = var∙ x₁

  v₂ : Elim (3 + n)
  v₂ = var∙ x₂

module EncodingWeakened {n} m where

  -- NOTE. Here we assume (m + 3) variables in context, with the names
  -- of S, K and App being the first three.

  infixl 9 _⊛_

  encS : Elim (m + (3 + n))
  encS = var∙ (raise m x₂)

  encK : Elim (m + (3 + n))
  encK = var∙ (raise m x₁)

  _⊛_ : (a b : Elim (m + (3 + n))) → Elim (m + (3 + n))
  a ⊛ b = var (raise m x₀) ∙ (a ∷ b ∷ [])

  -- Encoding of SK terms into raw types with (m + 3) free variables.

  encode : SKTerm → Elim (m + (3 + n))
  encode S       = encS
  encode K       = encK
  encode (s · t) = (encode s) ⊛ (encode t)

module Encoding = EncodingWeakened {0} 4

module _ {n} where

  -- Operator kinds for combinator terms.

  kdS : Kind Elim (0 + n)
  kdS = ⌜*⌝

  kdK : Kind Elim (1 + n)
  kdK = ⌜*⌝

  kdApp : Kind Elim (2 + n)
  kdApp = Π ⌜*⌝ (Π ⌜*⌝ ⌜*⌝)

  -- Operator kinds reduction/expansion laws.

  kdSRed : Kind Elim (3 + n)
  kdSRed = Π ⌜*⌝ (Π ⌜*⌝ (Π ⌜*⌝
    (encS ⊛ v₂ ⊛ v₁ ⊛ v₀ ⋯ v₂ ⊛ v₀ ⊛ (v₁ ⊛ v₀))))
    where open EncodingWeakened (3 + 0)

  kdKRed : Kind Elim (4 + n)
  kdKRed = Π ⌜*⌝ (Π ⌜*⌝
    (encK ⊛ v₁ ⊛ v₀ ⋯ v₁))
    where open EncodingWeakened (2 + 1)

  kdSExp : Kind Elim (5 + n)
  kdSExp = Π ⌜*⌝ (Π ⌜*⌝ (Π ⌜*⌝
    (v₂ ⊛ v₀ ⊛ (v₁ ⊛ v₀) ⋯ encS ⊛ v₂ ⊛ v₁ ⊛ v₀)))
    where open EncodingWeakened (3 + 2)

  kdKExp : Kind Elim (6 + n)
  kdKExp = Π ⌜*⌝ (Π ⌜*⌝
    (v₁ ⋯ encK ⊛ v₁ ⊛ v₀))
    where open EncodingWeakened (2 + 3)

-- The context for the SK encoding (aka the signature)

Γ-SK : Ctx 3
Γ-SK = kd kdApp ∷ kd kdK ∷ kd kdS ∷ []

Γ-SK? : Ctx |Γ|
Γ-SK? = kd kdKExp ∷ kd kdSExp ∷ kd kdKRed ∷ kd kdSRed ∷ Γ-SK

⌞Γ-SK?⌟ : TermCtx.Ctx |Γ|
⌞Γ-SK?⌟ = ⌞ Γ-SK? ⌟Ctx

module _ where
  open Encoding
  private Γ-nf = nfCtx ⌞Γ-SK?⌟

  -- Encoded SK terms are in normal form.

  nf-encode : ∀ t → nf Γ-nf ⌞ encode t ⌟ ≡ encode t
  nf-encode S       = refl
  nf-encode K       = refl
  nf-encode (s · t) =
    cong₂ _⊛_ (begin
        weakenElim (nf Γ-nf ⌞ encode s ⌟) /⟨ ★ ⟩ sub (nf Γ-nf ⌞ encode t ⌟)
      ≡⟨ /Var-wk-↑⋆-hsub-vanishes 0 (nf Γ-nf ⌞ encode s ⌟) ⟩
        nf Γ-nf ⌞ encode s ⌟
      ≡⟨ nf-encode s ⟩
        encode s
      ∎) (nf-encode t)

------------------------------------------------------------------------
-- Canonical operator kinding of encodings

module KindedEncodingWeakened {m} (E : CtxExt 3 m)
                              (Γ-ctx : E ++ Γ-SK ctx) where

  open EncodingWeakened {0} m

  private Γ = E ++ Γ-SK

  -- Kinded encodings of the SK terms

  Ne∈-S : Γ ⊢Ne encS ∈ ⌜*⌝
  Ne∈-S = ∈-∙ (⇉-var _ Γ-ctx (lookup-raise-* E ★ refl)) ⇉-[]

  Ne∈-K : Γ ⊢Ne encK ∈ ⌜*⌝
  Ne∈-K = ∈-∙ (⇉-var _ Γ-ctx (lookup-raise-* E ★ refl)) ⇉-[]

  Ne∈-⊛ : ∀ {a b} → Γ ⊢Ne a ∈ ⌜*⌝ → Γ ⊢Ne b ∈ ⌜*⌝ → Γ ⊢Ne a ⊛ b ∈ ⌜*⌝
  Ne∈-⊛ a∈* b∈* =
    ∈-∙ (⇉-var _ Γ-ctx (lookup-raise-* E (★ ⇒ ★ ⇒ ★) refl))
        (⇉-∷ (Nf⇇-ne a∈*) (kd-⌜*⌝ Γ-ctx)
             (⇉-∷ (Nf⇇-ne b∈*) (kd-⌜*⌝ Γ-ctx) ⇉-[]))

  Ne∈-encode : (t : SKTerm) → Γ ⊢Ne encode t ∈ ⌜*⌝
  Ne∈-encode S       = Ne∈-S
  Ne∈-encode K       = Ne∈-K
  Ne∈-encode (s · t) = Ne∈-⊛ (Ne∈-encode s) (Ne∈-encode t)

-- Another shorthand

Ne∈-var : ∀ {n} {Γ : Ctx n} {k} x →
          Γ ctx → lookup Γ x ≡ kd k → Γ ⊢Ne var∙ x ∈ k
Ne∈-var x Γ-ctx Γ[x]≡k = ∈-∙ (⇉-var x Γ-ctx Γ[x]≡k) ⇉-[]

-- The signatures Γ-SK and Γ-SK? are well-formed

kdS-kd : [] ⊢ kdS kd
kdS-kd = kd-⌜*⌝ []

Γ₁-ctx : kd kdS ∷ [] ctx
Γ₁-ctx = wf-kd kdS-kd ∷ []

kdK-kd : kd kdS ∷ [] ⊢ kdK kd
kdK-kd = kd-⌜*⌝ Γ₁-ctx

Γ₂-ctx : kd kdK ∷ kd kdS ∷ [] ctx
Γ₂-ctx = wf-kd kdK-kd ∷ Γ₁-ctx

kdApp-kd : kd kdK ∷ kd kdS ∷ [] ⊢ kdApp kd
kdApp-kd = kd-Π *₂-kd (kd-Π *₃-kd (kd-⌜*⌝ (wf-kd *₃-kd ∷ Γ₃-ctx′)))
  where
    *₂-kd   = kd-⌜*⌝ Γ₂-ctx
    Γ₃-ctx′ = wf-kd *₂-kd ∷ Γ₂-ctx
    *₃-kd   = kd-⌜*⌝ Γ₃-ctx′

Γ-SK-ctx : Γ-SK ctx
Γ-SK-ctx = wf-kd kdApp-kd ∷ Γ₂-ctx

kdSRed-kd : Γ-SK ⊢ kdSRed kd
kdSRed-kd = kd-Π *₃-kd (kd-Π *₄-kd (kd-Π *₅-kd (kd-⋯
  (⇉-s-i (Ne∈-⊛ (Ne∈-⊛ (Ne∈-⊛ Ne∈-S (Ne∈-var x₂ Γ₆-ctx′ refl))
                       (Ne∈-var x₁ Γ₆-ctx′ refl)) (Ne∈-var x₀ Γ₆-ctx′ refl)))
  (⇉-s-i (Ne∈-⊛ (Ne∈-⊛ (Ne∈-var x₂ Γ₆-ctx′ refl) (Ne∈-var x₀ Γ₆-ctx′ refl))
                (Ne∈-⊛ (Ne∈-var x₁ Γ₆-ctx′ refl) (Ne∈-var x₀ Γ₆-ctx′ refl)))))))
  where
    *₃-kd   = kd-⌜*⌝ Γ-SK-ctx
    Γ₄-ctx′ = wf-kd *₃-kd ∷ Γ-SK-ctx
    *₄-kd   = kd-⌜*⌝ Γ₄-ctx′
    Γ₅-ctx′ = wf-kd *₄-kd ∷ Γ₄-ctx′
    *₅-kd   = kd-⌜*⌝ Γ₅-ctx′
    Γ₆-ctx′ = wf-kd *₅-kd ∷ Γ₅-ctx′

    open KindedEncodingWeakened (kd ⌜*⌝ ∷ kd ⌜*⌝ ∷ kd ⌜*⌝ ∷ []) Γ₆-ctx′

Γ₄-ctx : kd kdSRed ∷ Γ-SK ctx
Γ₄-ctx = wf-kd kdSRed-kd ∷ Γ-SK-ctx

kdKRed-kd : kd kdSRed ∷ Γ-SK ⊢ kdKRed kd
kdKRed-kd = (kd-Π *₄-kd (kd-Π *₅-kd (kd-⋯
  (⇉-s-i (Ne∈-⊛ (Ne∈-⊛ Ne∈-K (Ne∈-var x₁ Γ₆-ctx′ refl))
                (Ne∈-var x₀ Γ₆-ctx′ refl)))
  (⇉-s-i (Ne∈-var x₁ Γ₆-ctx′ refl)))))
  where
    *₄-kd   = kd-⌜*⌝ Γ₄-ctx
    Γ₅-ctx′ = wf-kd *₄-kd ∷ Γ₄-ctx
    *₅-kd   = kd-⌜*⌝ Γ₅-ctx′
    Γ₆-ctx′ = wf-kd *₅-kd ∷ Γ₅-ctx′

    open KindedEncodingWeakened (kd ⌜*⌝ ∷ kd ⌜*⌝ ∷ kd kdSRed ∷ []) Γ₆-ctx′

Γ₅-ctx : kd kdKRed ∷ kd kdSRed ∷ Γ-SK ctx
Γ₅-ctx = wf-kd kdKRed-kd ∷ Γ₄-ctx

kdSExp-kd : kd kdKRed ∷ kd kdSRed ∷ Γ-SK ⊢ kdSExp kd
kdSExp-kd = kd-Π *₅-kd (kd-Π *₆-kd (kd-Π *₇-kd (kd-⋯
  (⇉-s-i (Ne∈-⊛ (Ne∈-⊛ (Ne∈-var x₂ Γ₈-ctx′ refl) (Ne∈-var x₀ Γ₈-ctx′ refl))
                (Ne∈-⊛ (Ne∈-var x₁ Γ₈-ctx′ refl) (Ne∈-var x₀ Γ₈-ctx′ refl))))
  (⇉-s-i (Ne∈-⊛ (Ne∈-⊛ (Ne∈-⊛ Ne∈-S (Ne∈-var x₂ Γ₈-ctx′ refl))
                       (Ne∈-var x₁ Γ₈-ctx′ refl))
                (Ne∈-var x₀ Γ₈-ctx′ refl))))))
  where
    *₅-kd   = kd-⌜*⌝ Γ₅-ctx
    Γ₆-ctx′ = wf-kd *₅-kd ∷ Γ₅-ctx
    *₆-kd   = kd-⌜*⌝ Γ₆-ctx′
    Γ₇-ctx′ = wf-kd *₆-kd ∷ Γ₆-ctx′
    *₇-kd   = kd-⌜*⌝ Γ₇-ctx′
    Γ₈-ctx′ = wf-kd *₇-kd ∷ Γ₇-ctx′

    open KindedEncodingWeakened
      (kd ⌜*⌝ ∷ kd ⌜*⌝ ∷ kd ⌜*⌝ ∷ kd kdKRed ∷ kd kdSRed ∷ []) Γ₈-ctx′

Γ₆-ctx : kd kdSExp ∷ kd kdKRed ∷ kd kdSRed ∷ Γ-SK ctx
Γ₆-ctx = wf-kd kdSExp-kd ∷ Γ₅-ctx

kdKExp-kd : kd kdSExp ∷ kd kdKRed ∷ kd kdSRed ∷ Γ-SK ⊢ kdKExp kd
kdKExp-kd = (kd-Π *₆-kd (kd-Π *₇-kd (kd-⋯
  (⇉-s-i (Ne∈-var x₁ Γ₈-ctx′ refl))
  (⇉-s-i (Ne∈-⊛ (Ne∈-⊛ Ne∈-K (Ne∈-var x₁ Γ₈-ctx′ refl))
                (Ne∈-var x₀ Γ₈-ctx′ refl))))))
  where
    *₆-kd   = kd-⌜*⌝ Γ₆-ctx
    Γ₇-ctx′ = wf-kd *₆-kd ∷ Γ₆-ctx
    *₇-kd   = kd-⌜*⌝ Γ₇-ctx′
    Γ₈-ctx′ = wf-kd *₇-kd ∷ Γ₇-ctx′

    open KindedEncodingWeakened
      (kd ⌜*⌝ ∷ kd ⌜*⌝ ∷ kd kdSExp ∷ kd kdKRed ∷ kd kdSRed ∷ []) Γ₈-ctx′

Γ-SK?-ctx : Γ-SK? ctx
Γ-SK?-ctx = wf-kd kdKExp-kd ∷ Γ₆-ctx

module KindedEncoding =
  KindedEncodingWeakened
    (kd kdKExp ∷ kd kdSExp ∷ kd kdKRed ∷ kd kdSRed ∷ []) Γ-SK?-ctx

------------------------------------------------------------------------
-- Encoding of SK term equality in canonical subtyping

open Encoding
open KindedEncoding

-- Some helper lemmas.

wk-hsub-helper : ∀ {n} (a b c : Elim n) →
  (weakenElim (weakenElim a) /⟨ ★ ⟩ sub b ↑) [ c ∈ ★ ] ≡ a
wk-hsub-helper a b c = begin
    (weakenElim (weakenElim a) /⟨ ★ ⟩ sub b ↑) [ c ∈ ★ ]
  ≡⟨ cong (λ a → (a /⟨ ★ ⟩ sub b ↑) [ c ∈ ★ ]) (ELV.wk-commutes a) ⟩
    (weakenElim a Elim/Var V.wk V.↑ /⟨ ★ ⟩ sub b ↑) [ c ∈ ★ ]
  ≡⟨ cong (_[ c ∈ ★ ]) (/Var-wk-↑⋆-hsub-vanishes 1 (weakenElim a)) ⟩
    weakenElim a [ c ∈ ★ ]
  ≡⟨ /Var-wk-↑⋆-hsub-vanishes 0 a ⟩
    a
  ∎
  where
    module EL  = TermLikeLemmas termLikeLemmasElim
    module ELV = LiftAppLemmas EL.varLiftAppLemmas
    module V   = VarSubst

-- Admissible kinding and subtyping rules for construction the encoded
-- SK derivations.

<:-⊛ : ∀ {a₁ a₂ b₁ b₂} → Γ-SK? ⊢ a₁ ≃ a₂ ⇇ ⌜*⌝ → Γ-SK? ⊢ b₁ ≃ b₂ ⇇ ⌜*⌝ →
       Γ-SK? ⊢ a₁ ⊛ b₁ <: a₂ ⊛ b₂
<:-⊛ a₁≃a₂ b₁≃b₂ = <:-∙ (⇉-var _ Γ-SK?-ctx refl) (≃-∷ a₁≃a₂ (≃-∷ b₁≃b₂ ≃-[]))

Ne∈-Sᵣ : ∀ {a b c} →
         Γ-SK? ⊢Ne a ∈ ⌜*⌝ → Γ-SK? ⊢Ne b ∈ ⌜*⌝ → Γ-SK? ⊢Ne c ∈ ⌜*⌝ →
         Γ-SK? ⊢Ne var x₃ ∙ (a ∷ b ∷ c ∷ []) ∈
                   encS ⊛ a ⊛ b ⊛ c ⋯ a ⊛ c ⊛ (b ⊛ c)
Ne∈-Sᵣ {a} {b} {c} a∈* b∈* c∈* =
  ∈-∙ (⇉-var _ Γ-SK?-ctx refl)
      (⇉-∷ (Nf⇇-ne a∈*) *-kd
           (⇉-∷ (Nf⇇-ne b∈*) *-kd (⇉-∷ (Nf⇇-ne c∈*) *-kd ⇉-[]′)))
  where
    *-kd = kd-⌜*⌝ Γ-SK?-ctx
    a≡⟨⟨a/wk⟩/wk⟩[b][c] = wk-hsub-helper a b c
    b≡⟨b/wk⟩[c] = /Var-wk-↑⋆-hsub-vanishes 0 b
    ⇉-[]′ =
      subst₂ (λ a′ b′ →
        Γ-SK? ⊢ encS ⊛ a′ ⊛ b′ ⊛ c ⋯ a′ ⊛ c ⊛ (b′ ⊛ c) ⇉∙ [] ⇉
                encS ⊛ a ⊛ b ⊛ c ⋯ a ⊛ c ⊛ (b ⊛ c))
        (sym a≡⟨⟨a/wk⟩/wk⟩[b][c]) (sym b≡⟨b/wk⟩[c]) ⇉-[]

<:-Sᵣ : ∀ {a b c} →
        Γ-SK? ⊢Ne a ∈ ⌜*⌝ → Γ-SK? ⊢Ne b ∈ ⌜*⌝ → Γ-SK? ⊢Ne c ∈ ⌜*⌝ →
        Γ-SK? ⊢ encS ⊛ a ⊛ b ⊛ c <: a ⊛ c ⊛ (b ⊛ c)
<:-Sᵣ a∈* b∈* c∈* =
  <:-trans (<:-⟨| (Ne∈-Sᵣ a∈* b∈* c∈*)) (<:-|⟩ (Ne∈-Sᵣ a∈* b∈* c∈*))

Ne∈-Kᵣ : ∀ {a b} → Γ-SK? ⊢Ne a ∈ ⌜*⌝ → Γ-SK? ⊢Ne b ∈ ⌜*⌝ →
         Γ-SK? ⊢Ne var x₂ ∙ (a ∷ b ∷ []) ∈ encK ⊛ a ⊛ b ⋯ a
Ne∈-Kᵣ {a} {b} a∈* b∈* =
  ∈-∙ (⇉-var _ Γ-SK?-ctx refl)
      (⇉-∷ (Nf⇇-ne a∈*) *-kd
           (⇉-∷ (Nf⇇-ne b∈*) *-kd ⇉-[]′))
  where
    *-kd  = kd-⌜*⌝ Γ-SK?-ctx
    ⇉-[]′ =
      subst (λ a′ → Γ-SK? ⊢ encK ⊛ a′ ⊛ b ⋯ a′ ⇉∙ [] ⇉ encK ⊛ a ⊛ b ⋯ a)
            (sym (/Var-wk-↑⋆-hsub-vanishes 0 a)) ⇉-[]

<:-Kᵣ : ∀ {a b} → Γ-SK? ⊢Ne a ∈ ⌜*⌝ →
        Γ-SK? ⊢Ne b ∈ ⌜*⌝ → Γ-SK? ⊢ encK ⊛ a ⊛ b <: a
<:-Kᵣ a∈* b∈* = <:-trans (<:-⟨| (Ne∈-Kᵣ a∈* b∈*)) (<:-|⟩ (Ne∈-Kᵣ a∈* b∈*))

Ne∈-Sₑ : ∀ {a b c} →
         Γ-SK? ⊢Ne a ∈ ⌜*⌝ → Γ-SK? ⊢Ne b ∈ ⌜*⌝ → Γ-SK? ⊢Ne c ∈ ⌜*⌝ →
         Γ-SK? ⊢Ne var x₁ ∙ (a ∷ b ∷ c ∷ []) ∈
                   a ⊛ c ⊛ (b ⊛ c) ⋯ encS ⊛ a ⊛ b ⊛ c
Ne∈-Sₑ {a} {b} {c} a∈* b∈* c∈* =
  ∈-∙ (⇉-var _ Γ-SK?-ctx refl)
      (⇉-∷ (Nf⇇-ne a∈*) *-kd
           (⇉-∷ (Nf⇇-ne b∈*) *-kd (⇉-∷ (Nf⇇-ne c∈*) *-kd ⇉-[]′)))
  where
    *-kd = kd-⌜*⌝ Γ-SK?-ctx
    a≡⟨⟨a/wk⟩/wk⟩[b][c] = wk-hsub-helper a b c
    b≡⟨b/wk⟩[c] = /Var-wk-↑⋆-hsub-vanishes 0 b
    ⇉-[]′ =
      subst₂ (λ a′ b′ →
        Γ-SK? ⊢ a′ ⊛ c ⊛ (b′ ⊛ c) ⋯ encS ⊛ a′ ⊛ b′ ⊛ c ⇉∙ [] ⇉
                a ⊛ c ⊛ (b ⊛ c) ⋯ encS ⊛ a ⊛ b ⊛ c)
        (sym a≡⟨⟨a/wk⟩/wk⟩[b][c]) (sym b≡⟨b/wk⟩[c]) ⇉-[]

<:-Sₑ : ∀ {a b c} →
        Γ-SK? ⊢Ne a ∈ ⌜*⌝ → Γ-SK? ⊢Ne b ∈ ⌜*⌝ → Γ-SK? ⊢Ne c ∈ ⌜*⌝ →
        Γ-SK? ⊢ a ⊛ c ⊛ (b ⊛ c) <: encS ⊛ a ⊛ b ⊛ c
<:-Sₑ a∈* b∈* c∈* =
  <:-trans (<:-⟨| (Ne∈-Sₑ a∈* b∈* c∈*)) (<:-|⟩ (Ne∈-Sₑ a∈* b∈* c∈*))

Ne∈-Kₑ : ∀ {a b} → Γ-SK? ⊢Ne a ∈ ⌜*⌝ → Γ-SK? ⊢Ne b ∈ ⌜*⌝ →
         Γ-SK? ⊢Ne var x₀ ∙ (a ∷ b ∷ []) ∈ a ⋯ encK ⊛ a ⊛ b
Ne∈-Kₑ {a} {b} a∈* b∈* =
  ∈-∙ (⇉-var _ Γ-SK?-ctx refl)
      (⇉-∷ (Nf⇇-ne a∈*) *-kd
           (⇉-∷ (Nf⇇-ne b∈*) *-kd ⇉-[]′))
  where
    *-kd  = kd-⌜*⌝ Γ-SK?-ctx
    ⇉-[]′ =
      subst (λ a′ → Γ-SK? ⊢ a′ ⋯ encK ⊛ a′ ⊛ b ⇉∙ [] ⇉ a ⋯ encK ⊛ a ⊛ b)
            (sym (/Var-wk-↑⋆-hsub-vanishes 0 a)) ⇉-[]

<:-Kₑ : ∀ {a b} → Γ-SK? ⊢Ne a ∈ ⌜*⌝ →
        Γ-SK? ⊢Ne b ∈ ⌜*⌝ → Γ-SK? ⊢ a <: encK ⊛ a ⊛ b
<:-Kₑ a∈* b∈* = <:-trans (<:-⟨| (Ne∈-Kₑ a∈* b∈*)) (<:-|⟩ (Ne∈-Kₑ a∈* b∈*))

-- Encoding of SK term equality in canonical subtyping

mutual

  <:-encode : ∀ {s t} → s ≡SK t → Γ-SK? ⊢ encode s <: encode t
  <:-encode (≡-refl {t})         = <:-reflNf⇉ (⇉-s-i (Ne∈-encode t))
  <:-encode (≡-trans s≡t t≡u)    = <:-trans (<:-encode s≡t) (<:-encode t≡u)
  <:-encode (≡-sym t≡s)          = :>-encode t≡s
  <:-encode (≡-Sred {s} {t} {u}) =
    <:-Sᵣ (Ne∈-encode s) (Ne∈-encode t) (Ne∈-encode u)
  <:-encode (≡-Kred {s} {t})     = <:-Kᵣ (Ne∈-encode s) (Ne∈-encode t)
  <:-encode (≡-· s₁≡t₁ s₂≡t₂)    = <:-⊛ (≃-encode s₁≡t₁) (≃-encode s₂≡t₂)

  :>-encode : ∀ {s t} → s ≡SK t → Γ-SK? ⊢ encode t <: encode s
  :>-encode (≡-refl {t})         = <:-reflNf⇉ (⇉-s-i (Ne∈-encode t))
  :>-encode (≡-trans s≡t t≡u)    = <:-trans (:>-encode t≡u) (:>-encode s≡t)
  :>-encode (≡-sym t≡s)          = <:-encode t≡s
  :>-encode (≡-Sred {s} {t} {u}) =
    <:-Sₑ (Ne∈-encode s) (Ne∈-encode t) (Ne∈-encode u)
  :>-encode (≡-Kred {s} {t})     = <:-Kₑ (Ne∈-encode s) (Ne∈-encode t)
  :>-encode (≡-· s₁≡t₁ s₂≡t₂)    =
    <:-⊛ (≃-sym (≃-encode s₁≡t₁)) (≃-sym (≃-encode s₂≡t₂))

  ≃-encode : ∀ {s t} → s ≡SK t → Γ-SK? ⊢ encode s ≃ encode t ⇇ ⌜*⌝
  ≃-encode {s} {t} s≡t =
    let es⇇* = Nf⇇-ne (Ne∈-encode s)
        et⇇* = Nf⇇-ne (Ne∈-encode t)
    in <:-antisym (kd-⌜*⌝ Γ-SK?-ctx)
                  (<:-⇇ es⇇* et⇇* (<:-encode s≡t))
                  (<:-⇇ et⇇* es⇇* (:>-encode s≡t))

<:⇇-encode : ∀ {s t} → s ≡SK t → Γ-SK? ⊢ encode s <: encode t ⇇ ⌜*⌝
<:⇇-encode {s} {t} s≡t =
  <:-⇇ (Nf⇇-ne (Ne∈-encode s)) (Nf⇇-ne (Ne∈-encode t)) (<:-encode s≡t)

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.OrderedCommMonoid.Instances where

open import Cubical.Foundations.Prelude

open import Cubical.Algebra.OrderedCommMonoid.Base

open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order

ℕ≤+ : OrderedCommMonoid ℓ-zero ℓ-zero
ℕ≤+ .fst = ℕ
ℕ≤+ .snd .OrderedCommMonoidStr._≤_ = _≤_
ℕ≤+ .snd .OrderedCommMonoidStr._·_ = _+_
ℕ≤+ .snd .OrderedCommMonoidStr.ε = 0
ℕ≤+ .snd .OrderedCommMonoidStr.isOrderedCommMonoid =
  makeIsOrderedCommMonoid
         isSetℕ
         +-assoc +-zero (λ _ → refl) +-comm
         (λ _ _ → isProp≤) (λ _ → ≤-refl) (λ _ _ _ → ≤-trans) (λ _ _ → ≤-antisym)
         (λ _ _ _ → ≤-+k) (λ _ _ _ → ≤-k+)

ℕ≤· : OrderedCommMonoid ℓ-zero ℓ-zero
ℕ≤· .fst = ℕ
ℕ≤· .snd .OrderedCommMonoidStr._≤_ = _≤_
ℕ≤· .snd .OrderedCommMonoidStr._·_ = _·_
ℕ≤· .snd .OrderedCommMonoidStr.ε = 1
ℕ≤· .snd .OrderedCommMonoidStr.isOrderedCommMonoid =
  makeIsOrderedCommMonoid
        isSetℕ
        ·-assoc ·-identityʳ ·-identityˡ ·-comm
        (λ _ _ → isProp≤) (λ _ → ≤-refl) (λ _ _ _ → ≤-trans) (λ _ _ → ≤-antisym)
        (λ _ _ _ → ≤-·k) lmono
  where lmono : (x y z : ℕ) → x ≤ y → z · x ≤ z · y
        lmono x y z x≤y = subst ((z · x) ≤_) (·-comm y z) (subst (_≤ (y · z)) (·-comm x z) (≤-·k x≤y))

ext: agda

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module _ where

open import Common.Prelude
open import Common.Reflection
open import Common.Equality

record Foo (A : Set) : Set where
  field
    foo : A → Nat

open Foo {{...}}

instance
  FooNat : Foo Nat
  foo {{FooNat}} n = n

  FooBool : Foo Bool
  foo {{FooBool}} true  = 1
  foo {{FooBool}} false = 0

macro
  do-foo : ∀ {A} {{_ : Foo A}} → A → Tactic
  do-foo x = give (lit (nat (foo x)))

test₁ : do-foo 5 ≡ 5
test₁ = refl

test₂ : do-foo false ≡ 0
test₂ = refl

macro
  lastHidden : {n : Nat} → Tactic
  lastHidden {n} = give (lit (nat n))

test₃ : lastHidden {4} ≡ 4
test₃ = refl

macro
  hiddenTerm : {a : Term} → Tactic
  hiddenTerm {a} = give a

test₄ : hiddenTerm {4} ≡ 4
test₄ = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of membership of vectors based on propositional equality.
------------------------------------------------------------------------

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

module Data.Vec.Membership.Propositional.Properties where

open import Data.Fin using (Fin; zero; suc)
open import Data.Product as Prod using (_,_; ∃; _×_; -,_)
open import Data.Vec hiding (here; there)
open import Data.Vec.Relation.Unary.Any using (here; there)
open import Data.List using ([]; _∷_)
open import Data.List.Relation.Unary.Any using (here; there)
open import Data.Vec.Relation.Unary.Any using (Any; here; there)
open import Data.Vec.Membership.Propositional
open import Data.List.Membership.Propositional
  using () renaming (_∈_ to _∈ₗ_)
open import Function using (_∘_; id)
open import Relation.Unary using (Pred)
open import Relation.Binary.PropositionalEquality using (refl)

------------------------------------------------------------------------
-- lookup

module _ {a} {A : Set a} where

  ∈-lookup : ∀ {n} i (xs : Vec A n) → lookup xs i ∈ xs
  ∈-lookup zero    (x ∷ xs) = here refl
  ∈-lookup (suc i) (x ∷ xs) = there (∈-lookup i xs)

------------------------------------------------------------------------
-- map

module _ {a b} {A : Set a} {B : Set b} (f : A → B) where

  ∈-map⁺ : ∀ {m v} {xs : Vec A m} → v ∈ xs → f v ∈ map f xs
  ∈-map⁺ (here refl)  = here refl
  ∈-map⁺ (there x∈xs) = there (∈-map⁺ x∈xs)

------------------------------------------------------------------------
-- _++_

module _ {a} {A : Set a} {v : A} where

  ∈-++⁺ˡ : ∀ {m n} {xs : Vec A m} {ys : Vec A n} → v ∈ xs → v ∈ xs ++ ys
  ∈-++⁺ˡ (here refl)  = here refl
  ∈-++⁺ˡ (there x∈xs) = there (∈-++⁺ˡ x∈xs)

  ∈-++⁺ʳ : ∀ {m n} (xs : Vec A m) {ys : Vec A n} → v ∈ ys → v ∈ xs ++ ys
  ∈-++⁺ʳ []       x∈ys = x∈ys
  ∈-++⁺ʳ (x ∷ xs) x∈ys = there (∈-++⁺ʳ xs x∈ys)

------------------------------------------------------------------------
-- tabulate

module _ {a} {A : Set a} where

  ∈-tabulate⁺ : ∀ {n} (f : Fin n → A) i → f i ∈ tabulate f
  ∈-tabulate⁺ f zero    = here refl
  ∈-tabulate⁺ f (suc i) = there (∈-tabulate⁺ (f ∘ suc) i)

------------------------------------------------------------------------
-- allFin

∈-allFin⁺ : ∀ {n} (i : Fin n) → i ∈ allFin n
∈-allFin⁺ = ∈-tabulate⁺ id

------------------------------------------------------------------------
-- allPairs

module _ {a b} {A : Set a} {B : Set b} where

  ∈-allPairs⁺ : ∀ {m n x y} {xs : Vec A m} {ys : Vec B n} →
               x ∈ xs → y ∈ ys → (x , y) ∈ allPairs xs ys
  ∈-allPairs⁺ {xs = x ∷ xs} (here refl) = ∈-++⁺ˡ ∘ ∈-map⁺ (x ,_)
  ∈-allPairs⁺ {xs = x ∷ _} (there x∈xs) =
    ∈-++⁺ʳ (map (x ,_) _) ∘ ∈-allPairs⁺ x∈xs

------------------------------------------------------------------------
-- toList

module _ {a} {A : Set a} {v : A} where

  ∈-toList⁺ : ∀ {n} {xs : Vec A n} → v ∈ xs → v ∈ₗ toList xs
  ∈-toList⁺ (here refl) = here refl
  ∈-toList⁺ (there x∈)  = there (∈-toList⁺ x∈)

  ∈-toList⁻ : ∀ {n} {xs : Vec A n} → v ∈ₗ toList xs → v ∈ xs
  ∈-toList⁻ {xs = []}     ()
  ∈-toList⁻ {xs = x ∷ xs} (here refl)  = here refl
  ∈-toList⁻ {xs = x ∷ xs} (there v∈xs) = there (∈-toList⁻ v∈xs)

------------------------------------------------------------------------
-- fromList

module _ {a} {A : Set a} {v : A} where

  ∈-fromList⁺ : ∀ {xs} → v ∈ₗ xs → v ∈ fromList xs
  ∈-fromList⁺ (here refl) = here refl
  ∈-fromList⁺ (there x∈)  = there (∈-fromList⁺ x∈)

  ∈-fromList⁻ : ∀ {xs} → v ∈ fromList xs → v ∈ₗ xs
  ∈-fromList⁻ {[]}    ()
  ∈-fromList⁻ {_ ∷ _} (here refl)  = here refl
  ∈-fromList⁻ {_ ∷ _} (there v∈xs) = there (∈-fromList⁻ v∈xs)

------------------------------------------------------------------------
-- Relationship to Any

module _ {a p} {A : Set a} {P : Pred A p} where

  fromAny : ∀ {n} {xs : Vec A n} → Any P xs → ∃ λ x → x ∈ xs × P x
  fromAny (here px) = -, here refl , px
  fromAny (there v) = Prod.map₂ (Prod.map₁ there) (fromAny v)

  toAny : ∀ {n x} {xs : Vec A n} → x ∈ xs → P x → Any P xs
  toAny (here refl) px = here px
  toAny (there v)   px = there (toAny v px)


text:
module Issue357a where

module M (X : Set) where

  data R : Set where
    r : X → R

postulate
  P Q : Set
  q   : Q

open M P
open M.R

works : M.R Q → Q
works (M.R.r q) = q

fails : M.R Q → Q
fails (r q) = q


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

open import Algebra.Structures.Bundles.Field
import Algebra.Linear.Structures.Bundles.FiniteDimensional as FDB

module Algebra.Linear.Space.FiniteDimensional.Product
       {k ℓᵏ} (K : Field k ℓᵏ)
       {n a₁ ℓ₁} (V₁-space : FDB.FiniteDimensional K a₁ ℓ₁ n)
       {p a₂ ℓ₂} (V₂-space : FDB.FiniteDimensional K a₂ ℓ₂ p)
       where

open import Algebra.Linear.Structures.VectorSpace K
open import Algebra.Linear.Structures.Bundles as VS
open import Algebra.Linear.Structures.FiniteDimensional K

open import Algebra.Linear.Morphism.Bundles K

open VectorSpaceField

open FDB.FiniteDimensional V₁-space
  using ()
  renaming
  ( Carrier       to V₁
  ; _≈_           to _≈₁_
  ; isEquivalence to ≈₁-isEquiv
  ; refl          to ≈₁-refl
  ; sym           to ≈₁-sym
  ; trans         to ≈₁-trans
  ; reflexive     to ≈₁-reflexive
  ; _+_           to _+₁_
  ; _∙_           to _∙₁_
  ; -_            to -₁_
  ; 0#            to 0₁
  ; +-identityˡ    to +₁-identityˡ
  ; +-identityʳ    to +₁-identityʳ
  ; +-identity    to +₁-identity
  ; +-cong        to +₁-cong
  ; +-assoc       to +₁-assoc
  ; +-comm        to +₁-comm
  ; *ᵏ-∙-compat   to *ᵏ-∙₁-compat
  ; ∙-+-distrib   to ∙₁-+₁-distrib
  ; ∙-+ᵏ-distrib  to ∙₁-+ᵏ-distrib
  ; ∙-cong        to ∙₁-cong
  ; ∙-identity    to ∙₁-identity
  ; ∙-absorbˡ      to ∙₁-absorbˡ
  ; ∙-absorbʳ      to ∙₁-absorbʳ
  ; -‿cong        to -₁‿cong
  ; -‿inverseˡ    to -₁‿inverseˡ
  ; -‿inverseʳ    to -₁‿inverseʳ
  ; vectorSpace   to vectorSpace₁
  ; embed         to embed₁
  )

open FDB.FiniteDimensional V₂-space
  using ()
  renaming
  ( Carrier       to V₂
  ; _≈_           to _≈₂_
  ; isEquivalence to ≈₂-isEquiv
  ; refl          to ≈₂-refl
  ; sym           to ≈₂-sym
  ; trans         to ≈₂-trans
  ; reflexive     to ≈₂-reflexive
  ; _+_           to _+₂_
  ; _∙_           to _∙₂_
  ; -_            to -₂_
  ; 0#            to 0₂
  ; +-identityˡ    to +₂-identityˡ
  ; +-identityʳ    to +₂-identityʳ
  ; +-identity    to +₂-identity
  ; +-cong        to +₂-cong
  ; +-assoc       to +₂-assoc
  ; +-comm        to +₂-comm
  ; *ᵏ-∙-compat   to *ᵏ-∙₂-compat
  ; ∙-+-distrib   to ∙₂-+₂-distrib
  ; ∙-+ᵏ-distrib  to ∙₂-+ᵏ-distrib
  ; ∙-cong        to ∙₂-cong
  ; ∙-identity    to ∙₂-identity
  ; ∙-absorbˡ      to ∙₂-absorbˡ
  ; ∙-absorbʳ      to ∙₂-absorbʳ
  ; -‿cong        to -₂‿cong
  ; -‿inverseˡ    to -₂‿inverseˡ
  ; -‿inverseʳ    to -₂‿inverseʳ
  ; vectorSpace   to vectorSpace₂
  ; embed         to embed₂
  )

open LinearIsomorphism embed₁
  using ()
  renaming
  ( ⟦_⟧        to ⟦_⟧₁
  ; ⟦⟧-cong    to ⟦⟧₁-cong
  ; injective  to ⟦⟧₁-injective
  ; surjective to ⟦⟧₁-surjective
  ; +-homo     to +₁-homo
  ; ∙-homo     to ∙₁-homo
  ; 0#-homo    to 0₁-homo
  )

open LinearIsomorphism embed₂
  using ()
  renaming
  ( ⟦_⟧        to ⟦_⟧₂
  ; ⟦⟧-cong    to ⟦⟧₂-cong
  ; injective  to ⟦⟧₂-injective
  ; surjective to ⟦⟧₂-surjective
  ; +-homo     to +₂-homo
  ; ∙-homo     to ∙₂-homo
  ; 0#-homo    to 0₂-homo
  )

open import Data.Product
import Algebra.Linear.Construct.ProductSpace K vectorSpace₁ vectorSpace₂ as PS
open VS.VectorSpace PS.vectorSpace
  renaming
    ( refl  to ≈-refl
    ; sym   to ≈-sym
    ; trans to ≈-trans
    )

open import Algebra.Linear.Construct.Vector K
  using
    ( ++-cong
    ; ++-identityˡ
    ; ++-split
    ; +-distrib-++
    ; ∙-distrib-++
    ; 0++0≈0
    )
  renaming
    ( _≈_         to _≈v_
    ; ≈-refl      to ≈v-refl
    ; ≈-sym       to ≈v-sym
    ; ≈-trans     to ≈v-trans
    ; ≈-reflexive to ≈v-reflexive
    ; _+_         to _+v_
    ; _∙_         to _∙v_
    ; 0#          to 0v
    ; +-cong      to +v-cong
    ; setoid      to vec-setoid
    ; vectorSpace to vector-vectorSpace
    )

open import Data.Nat using (ℕ) renaming (_+_ to _+ℕ_)

open import Relation.Binary.PropositionalEquality as P
  using (_≡_; subst; subst-subst-sym)
  renaming
  ( refl  to ≡-refl
  ; sym   to ≡-sym
  ; trans to ≡-trans
  )

open import Data.Vec
open import Algebra.Morphism.Definitions (V₁ × V₂) (Vec K' (n +ℕ p)) _≈v_
open import Algebra.Linear.Morphism.Definitions K (V₁ × V₂) (Vec K' (n +ℕ p)) _≈v_
import Relation.Binary.Morphism.Definitions (V₁ × V₂) (Vec K' (n +ℕ p)) as R
open import Function
open import Relation.Binary.EqReasoning (vec-setoid (n +ℕ p))

⟦_⟧ : V₁ × V₂ -> Vec K' (n +ℕ p)
⟦ (u , v) ⟧ = ⟦ u ⟧₁ ++ ⟦ v ⟧₂

⟦⟧-cong : R.Homomorphic₂ PS._≈_ _≈v_ ⟦_⟧
⟦⟧-cong (r₁ , r₂) = ++-cong (⟦⟧₁-cong r₁) (⟦⟧₂-cong r₂)

+-homo : Homomorphic₂ ⟦_⟧ _+_ _+v_
+-homo (x₁ , x₂) (y₁ , y₂) =
    begin
      ⟦ (x₁ , x₂) + (y₁ , y₂) ⟧
    ≡⟨⟩
      ⟦ x₁ +₁ y₁ ⟧₁ ++ ⟦ x₂ +₂ y₂ ⟧₂
    ≈⟨ ++-cong (+₁-homo x₁ y₁) (+₂-homo x₂ y₂) ⟩
      (⟦ x₁ ⟧₁ +v ⟦ y₁ ⟧₁) ++ (⟦ x₂ ⟧₂ +v ⟦ y₂ ⟧₂)
    ≈⟨ ≈v-sym (+-distrib-++ ⟦ x₁ ⟧₁ ⟦ x₂ ⟧₂ ⟦ y₁ ⟧₁ ⟦ y₂ ⟧₂) ⟩
      (⟦ x₁ ⟧₁ ++ ⟦ x₂ ⟧₂) +v (⟦ y₁ ⟧₁ ++ ⟦ y₂ ⟧₂)
    ≈⟨ +v-cong ≈v-refl ≈v-refl ⟩
       ⟦ x₁ , x₂ ⟧ +v ⟦ y₁ , y₂ ⟧
    ∎

0#-homo : Homomorphic₀ ⟦_⟧ 0# 0v
0#-homo =
  begin
    ⟦ 0# ⟧
  ≡⟨⟩
    ⟦ 0₁ ⟧₁ ++ ⟦ 0₂ ⟧₂
  ≈⟨ ++-cong 0₁-homo 0₂-homo ⟩
    (0v {n}) ++ (0v {p})
  ≈⟨ 0++0≈0 {n} {p} ⟩
    0v {n +ℕ p}
  ∎

∙-homo : ScalarHomomorphism ⟦_⟧ _∙_ _∙v_
∙-homo c (x₁ , x₂) =
  begin
    ⟦ c ∙ (x₁ , x₂) ⟧
  ≈⟨ ++-cong (∙₁-homo c x₁) (∙₂-homo c x₂) ⟩
    (c ∙v ⟦ x₁ ⟧₁) ++ (c ∙v ⟦ x₂ ⟧₂)
  ≈⟨ ≈v-sym (∙-distrib-++ c ⟦ x₁ ⟧₁ ⟦ x₂ ⟧₂) ⟩
    c ∙v ⟦ x₁ , x₂ ⟧
  ∎

⟦⟧-injective : Injective PS._≈_ (_≈v_ {n +ℕ p}) ⟦_⟧
⟦⟧-injective {x₁ , x₂} {y₁ , y₂} r =
  let (r₁ , r₂) = ++-split r
  in ⟦⟧₁-injective r₁ , ⟦⟧₂-injective r₂

⟦⟧-surjective : Surjective PS._≈_ (_≈v_ {n +ℕ p}) ⟦_⟧
⟦⟧-surjective y =
  let (x₁ , x₂ , r) = splitAt n y
      (u , r₁) = ⟦⟧₁-surjective x₁
      (v , r₂) = ⟦⟧₂-surjective x₂
  in  (u , v) , ≈v-trans (++-cong r₁ r₂) (≈v-sym (≈v-reflexive r))

embed : LinearIsomorphism PS.vectorSpace (vector-vectorSpace {n +ℕ p})
embed = record
  { ⟦_⟧ = ⟦_⟧
  ; isLinearIsomorphism = record
    { isLinearMonomorphism = record
      { isLinearMap = record
        { isAbelianGroupMorphism = record
          { gp-homo = record
            { mn-homo = record
              { sm-homo = record
                { ⟦⟧-cong = ⟦⟧-cong
                ; ∙-homo = +-homo
                }
              ; ε-homo = 0#-homo
              }
            }
          }
        ; ∙-homo = ∙-homo
        }
      ; injective = ⟦⟧-injective
      }
    ; surjective = ⟦⟧-surjective
    }
  }

isFiniteDimensional : IsFiniteDimensional _≈_ _+_ _∙_ -_ 0# (n +ℕ p)
isFiniteDimensional = record
  { isVectorSpace = isVectorSpace
  ; embed         = embed
  }

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


text:
module Numeral.Sign.Oper where

open import Data.Boolean
open import Numeral.Sign

-- Negation
−_ : (+|−) → (+|−)
− (➕) = (➖)
− (➖) = (➕)

-- Addition
_+_ : (+|−) → (+|−) → (+|0|−)
(➕) + (➕) = (➕)
(➖) + (➖) = (➖)
(➕) + (➖) = (𝟎)
(➖) + (➕) = (𝟎)

-- Multiplication
_⨯_ : (+|−) → (+|−) → (+|−)
(➕) ⨯ (➕) = (➕)
(➖) ⨯ (➖) = (➕)
(➕) ⨯ (➖) = (➖)
(➖) ⨯ (➕) = (➖)

_⋚_ : (+|−) → (+|−) → (+|0|−)
➕ ⋚ ➕ = 𝟎
➕ ⋚ ➖ = ➕
➖ ⋚ ➕ = ➖
➖ ⋚ ➖ = 𝟎

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

module FinEquivCat where

-- We will define a rig category whose objects are Fin types and whose
-- morphisms are type equivalences; and where the equivalence of
-- morphisms ≋ is extensional

open import Level using () renaming (zero to lzero; suc to lsuc)

open import Data.Fin using (Fin; zero; suc)
open import Data.Nat using (ℕ; _+_; _*_)
open import Data.Unit using ()
open import Data.Sum using (_⊎_; inj₁; inj₂) renaming (map to map⊎)
open import Data.Product
  using (_,_; proj₁; proj₂;_×_; Σ; uncurry)
  renaming (map to map×)
import Function as F using (_∘_; id)

import Relation.Binary.PropositionalEquality as P
  using (refl; trans; cong)

open import Categories.Category using (Category)
open import Categories.Groupoid using (Groupoid)
open import Categories.Monoidal using (Monoidal)
open import Categories.Monoidal.Helpers using (module MonoidalHelperFunctors)
open import Categories.Bifunctor using (Bifunctor)
open import Categories.NaturalIsomorphism using (NaturalIsomorphism)
open import Categories.Monoidal.Braided using (Braided)
open import Categories.Monoidal.Symmetric using (Symmetric)
open import Categories.RigCategory
  using (RigCategory; module BimonoidalHelperFunctors)

open import Equiv using (id≃; sym≃; _∼_; sym∼; _●_)
open import EquivEquiv
  using (_≋_; eq; id≋; sym≋; trans≋; _◎_; ●-assoc; lid≋; rid≋;
         linv≋; rinv≋; module _≋_)

open import FinEquivTypeEquiv
  using (_fin≃_; module PlusE; module TimesE; module PlusTimesE)
open PlusE using (_+F_; unite+; unite+r; uniti+; uniti+r;
                  swap+; sswap+; assocl+; assocr+)
open TimesE using (_*F_; unite*; uniti*; unite*r; uniti*r;
                  swap*; sswap*; assocl*; assocr*)
open PlusTimesE using (distz; factorz; distzr; factorzr;
                       dist; factor; distl; factorl)
open import FinEquivEquivPlus using (
    [id+id]≋id; +●≋●+; _+≋_;
    unite₊-nat; unite₊r-nat; uniti₊-nat; uniti₊r-nat;
    assocr₊-nat; assocl₊-nat; unite-assocr₊-coh; assocr₊-coh;
    swap₊-nat; sswap₊-nat; assocr₊-swap₊-coh; assocl₊-swap₊-coh)
open import FinEquivEquivTimes using (
    id*id≋id; *●≋●*; _*≋_;
    unite*-nat; unite*r-nat; uniti*-nat; uniti*r-nat;
    assocr*-nat; assocl*-nat; unite-assocr*-coh; assocr*-coh;
    swap*-nat; sswap*-nat; assocr*-swap*-coh; assocl*-swap*-coh)
open import FinEquivEquivPlusTimes using (
    distl-nat; factorl-nat; dist-nat; factor-nat;
    distzr-nat; factorzr-nat; distz-nat; factorz-nat;
    A×[B⊎C]≃[A×C]⊎[A×B];
    [A⊎B]×C≃[C×A]⊎[C×B];
    [A⊎B⊎C]×D≃[A×D⊎B×D]⊎C×D;
    A×B×[C⊎D]≃[A×B]×C⊎[A×B]×D;
    [A⊎B]×[C⊎D]≃[[A×C⊎B×C]⊎A×D]⊎B×D;
    0×0≃0;
    0×[A⊎B]≃0;
    0×1≃0;
    A×0≃0;
    0×A×B≃0;
    A×0×B≃0;
    A×[0+B]≃A×B;
    1×[A⊎B]≃A⊎B)

------------------------------------------------------------------------------
-- Fin and type equivalences are a category
-- note how all of the 'higher structure' (i.e. ≋ equations) are all
-- generic, i.e. they are true of all equivalences, not just _fin≃_.

FinEquivCat : Category lzero lzero lzero
FinEquivCat = record
  { Obj = ℕ
  ; _⇒_ = _fin≃_
  ; _≡_ = _≋_
  ; id = id≃
  ; _∘_ = _●_
  ; assoc = λ { {f = f} {g} {h} → ●-assoc {f = f} {g} {h} }
  ; identityˡ = lid≋
  ; identityʳ = rid≋
  ; equiv = record { refl = id≋ ; sym = sym≋ ; trans = trans≋ }
  ; ∘-resp-≡ = _◎_
  }

FinEquivGroupoid : Groupoid FinEquivCat
FinEquivGroupoid = record
  { _⁻¹ = sym≃
  ; iso = λ { {f = A≃B} → record
    { isoˡ = linv≋ A≃B
    ; isoʳ = rinv≋ A≃B
    } }
  }

-- The additive structure is monoidal

⊎-bifunctor : Bifunctor FinEquivCat FinEquivCat FinEquivCat
⊎-bifunctor = record
  { F₀ = uncurry _+_
  ; F₁ = uncurry _+F_
  ; identity = [id+id]≋id
  ; homomorphism = +●≋●+
  ; F-resp-≡ = uncurry _+≋_
  }

module ⊎h = MonoidalHelperFunctors FinEquivCat ⊎-bifunctor 0

0⊎x≡x : NaturalIsomorphism ⊎h.id⊗x ⊎h.x
0⊎x≡x = record
  { F⇒G = record
    { η = λ _ → unite+
    ; commute = λ _ → unite₊-nat }
  ; F⇐G = record
    { η = λ _ → uniti+
    ; commute = λ _ →  uniti₊-nat }
  ; iso = λ _ → record
    { isoˡ = linv≋ unite+
    ; isoʳ = rinv≋ unite+
    }
  }

x⊎0≡x : NaturalIsomorphism ⊎h.x⊗id ⊎h.x
x⊎0≡x = record
  { F⇒G = record
    { η = λ _ → unite+r
    ; commute = λ _ → unite₊r-nat }
  ; F⇐G = record
    { η = λ _ → uniti+r
    ; commute = λ _ → uniti₊r-nat
    }
  ; iso = λ X → record
    { isoˡ = linv≋ unite+r
    ; isoʳ = rinv≋ unite+r
    }
  }

[x⊎y]⊎z≡x⊎[y⊎z] : NaturalIsomorphism ⊎h.[x⊗y]⊗z ⊎h.x⊗[y⊗z]
[x⊎y]⊎z≡x⊎[y⊎z] = record
  { F⇒G = record
    { η = λ X → assocr+ {m = X zero}
    ; commute = λ _ → assocr₊-nat
    }
  ; F⇐G = record
    { η = λ X → assocl+ {m = X zero}
    ; commute = λ _ → assocl₊-nat
    }
  ; iso = λ X → record
    { isoˡ = linv≋ assocr+
    ; isoʳ = rinv≋ assocr+
    }
  }

CPM⊎ : Monoidal FinEquivCat
CPM⊎ = record
  { ⊗ = ⊎-bifunctor
   ; id = 0
   ; identityˡ = 0⊎x≡x
   ; identityʳ = x⊎0≡x
   ; assoc = [x⊎y]⊎z≡x⊎[y⊎z]
   ; triangle = unite-assocr₊-coh
   ; pentagon = assocr₊-coh
   }

-- The multiplicative structure is monoidal

×-bifunctor : Bifunctor FinEquivCat FinEquivCat FinEquivCat
×-bifunctor = record
  { F₀ = uncurry _*_
  ; F₁ = uncurry _*F_
  ; identity = id*id≋id
  ; homomorphism = *●≋●*
  ; F-resp-≡ = uncurry _*≋_
  }

module ×h = MonoidalHelperFunctors FinEquivCat ×-bifunctor 1

1×y≡y : NaturalIsomorphism ×h.id⊗x ×h.x
1×y≡y = record
  { F⇒G = record
    { η = λ _ → unite*
    ; commute = λ _ → unite*-nat
    }
  ; F⇐G = record
    { η = λ _ → uniti*
    ; commute = λ _ → uniti*-nat
    }
  ; iso = λ X → record
    { isoˡ = linv≋ unite*
    ; isoʳ = rinv≋ unite*
    }
  }

y×1≡y : NaturalIsomorphism ×h.x⊗id ×h.x
y×1≡y = record
  { F⇒G = record
    { η = λ X → unite*r
    ;  commute = λ _ → unite*r-nat
    }
  ; F⇐G = record
    { η = λ X → uniti*r
    ; commute = λ _ → uniti*r-nat
    }
  ; iso = λ X → record
    { isoˡ = linv≋ unite*r
    ; isoʳ = rinv≋ unite*r
    }
  }

[x×y]×z≡x×[y×z] : NaturalIsomorphism ×h.[x⊗y]⊗z ×h.x⊗[y⊗z]
[x×y]×z≡x×[y×z] = record
  { F⇒G = record
    { η = λ X → assocr* {m = X zero}
    ; commute = λ _ → assocr*-nat }
  ; F⇐G = record
    { η = λ X → assocl* {m = X zero}
    ; commute = λ _ → assocl*-nat }
  ; iso = λ X → record
    { isoˡ = linv≋ assocr*
    ; isoʳ = rinv≋ assocr* }
  }

CPM× : Monoidal FinEquivCat
CPM× = record
  { ⊗ = ×-bifunctor
  ; id = 1
  ; identityˡ = 1×y≡y
  ; identityʳ = y×1≡y
  ; assoc = [x×y]×z≡x×[y×z]
  ; triangle = unite-assocr*-coh
  ; pentagon = assocr*-coh
  }

-- The monoidal structures are symmetric

x⊎y≈y⊎x : NaturalIsomorphism ⊎h.x⊗y ⊎h.y⊗x
x⊎y≈y⊎x = record
  { F⇒G = record
    { η = λ X → swap+ {m = X zero}
    ; commute = λ _ → swap₊-nat
    }
  ; F⇐G = record
    { η = λ X → sswap+ {m = X zero} {n = X (suc zero)}
    ; commute = λ _ → sswap₊-nat
    }
  ; iso = λ X → record
    { isoˡ = linv≋ swap+
    ; isoʳ = rinv≋ swap+
    }
  }

BM⊎ : Braided CPM⊎
BM⊎ = record
  { braid = x⊎y≈y⊎x
  ; hexagon₁ = assocr₊-swap₊-coh
  ; hexagon₂ = assocl₊-swap₊-coh
  }

x×y≈y×x : NaturalIsomorphism ×h.x⊗y ×h.y⊗x
x×y≈y×x = record
  { F⇒G = record
    { η = λ X → swap* {m = X zero}
    ; commute = λ _ → swap*-nat
    }
  ; F⇐G = record
    { η = λ X → sswap* {m = X zero}
    ; commute = λ _ → sswap*-nat
    }
  ; iso = λ X → record
    { isoˡ = linv≋ swap*
    ; isoʳ = rinv≋ swap*
    }
  }

BM× : Braided CPM×
BM× = record
  { braid = x×y≈y×x
  ; hexagon₁ = assocr*-swap*-coh
  ; hexagon₂ = assocl*-swap*-coh
  }

SBM⊎ : Symmetric BM⊎
SBM⊎ = record { symmetry = linv≋ sswap+ }

SBM× : Symmetric BM×
SBM× = record { symmetry = linv≋ sswap* }

-- And finally the multiplicative structure distributes over the
-- additive one

module r = BimonoidalHelperFunctors BM⊎ BM×

x⊗[y⊕z]≡[x⊗y]⊕[x⊗z] : NaturalIsomorphism r.x⊗[y⊕z] r.[x⊗y]⊕[x⊗z]
x⊗[y⊕z]≡[x⊗y]⊕[x⊗z] = record
  { F⇒G = record
    { η = λ X → distl {m = X zero}
    ; commute = λ _ → distl-nat
    }
  ; F⇐G = record
    { η = λ X → factorl {m = X zero}
    ; commute = λ _ → factorl-nat
    }
  ; iso = λ X → record { isoˡ = linv≋ distl
                       ; isoʳ = rinv≋ distl }
  }

[x⊕y]⊗z≡[x⊗z]⊕[y⊗z] : NaturalIsomorphism r.[x⊕y]⊗z r.[x⊗z]⊕[y⊗z]
[x⊕y]⊗z≡[x⊗z]⊕[y⊗z] = record
  { F⇒G = record
    { η = λ X → dist {m = X zero}
    ; commute = λ _ → dist-nat
    }
  ; F⇐G = record
    { η = λ X → factor {m = X zero}
    ; commute = λ _ → factor-nat
    }
  ; iso = λ X → record { isoˡ = linv≋ dist
                       ; isoʳ = rinv≋ dist }
  }

x⊗0≡0 : NaturalIsomorphism r.x⊗0 r.0↑
x⊗0≡0 = record
  { F⇒G = record
    { η = λ X → distzr {m = X zero}
    ; commute = λ _ → distzr-nat
    }
  ; F⇐G = record
    { η = λ X → factorzr {n = X zero}
    ; commute = λ _ → factorzr-nat
    }
  ; iso = λ X → record
    { isoˡ = linv≋ distzr
    ; isoʳ = rinv≋ distzr
    }
  }

0⊗x≡0 : NaturalIsomorphism r.0⊗x r.0↑
0⊗x≡0 = record
  { F⇒G = record
    { η = λ X → distz {m = X zero}
    ; commute = λ _ → distz-nat
    }
  ; F⇐G = record
    { η = λ X → factorz {m = X zero}
    ; commute = λ _ → factorz-nat
    }
  ; iso = λ X → record
    { isoˡ = linv≋ distz
    ; isoʳ = rinv≋ distz
    }
  }

TERig : RigCategory SBM⊎ SBM×
TERig = record
  { distribₗ = x⊗[y⊕z]≡[x⊗y]⊕[x⊗z]
  ; distribᵣ = [x⊕y]⊗z≡[x⊗z]⊕[y⊗z]
  ; annₗ = 0⊗x≡0
  ; annᵣ = x⊗0≡0
  ; laplazaI = A×[B⊎C]≃[A×C]⊎[A×B]
  ; laplazaII = [A⊎B]×C≃[C×A]⊎[C×B]
  ; laplazaIV = [A⊎B⊎C]×D≃[A×D⊎B×D]⊎C×D
  ; laplazaVI = A×B×[C⊎D]≃[A×B]×C⊎[A×B]×D
  ; laplazaIX = [A⊎B]×[C⊎D]≃[[A×C⊎B×C]⊎A×D]⊎B×D
  ; laplazaX = 0×0≃0
  ; laplazaXI = 0×[A⊎B]≃0
  ; laplazaXIII = 0×1≃0
  ; laplazaXV = A×0≃0
  ; laplazaXVI = 0×A×B≃0
  ; laplazaXVII = A×0×B≃0
  ; laplazaXIX = A×[0+B]≃A×B
  ; laplazaXXIII = 1×[A⊎B]≃A⊎B
  }

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

module Classical where

open import Prelude
open import Relation.Nullary.Stable using (Stable) public
open import Relation.Nullary.Decidable.Properties using (Dec→Stable) public

Classical : Type a → Type a
Classical A = ¬ ¬ A

pure : A → Classical A
pure x k = k x

_>>=_ : Classical A → (A → Classical B) → Classical B
xs >>= f = λ k → xs λ x → f x k

_<*>_ : Classical (A → B) → Classical A → Classical B
fs <*> xs = λ k → fs λ f → xs λ x → k (f x)

lem : {A : Type a} → Classical (Dec A)
lem k = k (no (k ∘ yes))

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------
-- Bi-invertibility with erased proofs
------------------------------------------------------------------------

-- The development is based on the presentation of bi-invertibility
-- (for types and functions) and related things in the HoTT book, but
-- adapted to a setting with erasure.

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

open import Equality
open import Prelude as P hiding (id; _∘_; [_,_])

-- The code is parametrised by something like a "raw" category.

module Bi-invertibility.Erased
  {e⁺}
  (eq : ∀ {a p} → Equality-with-J a p e⁺)
  {o h}
  (Obj : Type o)
  (Hom : Obj → Obj → Type h)
  (id : {A : Obj} → Hom A A)
  (_∘′_ : {A B C : Obj} → Hom B C → Hom A B → Hom A C)
  where

open import Bi-invertibility eq Obj Hom id _∘′_ as Bi
  using (Has-left-inverse; Has-right-inverse; Is-bi-invertible;
         Has-quasi-inverse; _≊_; _≅_)
open Derived-definitions-and-properties eq
open import Equivalence eq as Eq using (_≃_)
open import Equivalence.Erased eq as EEq using (_≃ᴱ_)
open import Equivalence.Erased.Contractible-preimages eq as ECP
  using (Contractibleᴱ)
open import Erased.Without-box-cong eq
open import Function-universe eq as F hiding (id; _∘_)
open import Logical-equivalence using (_⇔_)
open import H-level eq
open import H-level.Closure eq
open import Preimage eq
open import Surjection eq using (_↠_)

private
  variable
    A B : Obj
    f   : Hom A B

  infixr 9 _∘_

  _∘_ : {A B C : Obj} → Hom B C → Hom A B → Hom A C
  _∘_ = _∘′_

-- Has-left-inverseᴱ f means that f has a left inverse. The proof is
-- erased.

Has-left-inverseᴱ : @0 Hom A B → Type h
Has-left-inverseᴱ f = ∃ λ f⁻¹ → Erased (f⁻¹ ∘ f ≡ id)

-- Has-right-inverseᴱ f means that f has a right inverse. The proof is
-- erased.

Has-right-inverseᴱ : @0 Hom A B → Type h
Has-right-inverseᴱ f = ∃ λ f⁻¹ → Erased (f ∘ f⁻¹ ≡ id)

-- Is-bi-invertibleᴱ f means that f has a left inverse and a (possibly
-- distinct) right inverse. The proofs are erased.

Is-bi-invertibleᴱ : @0 Hom A B → Type h
Is-bi-invertibleᴱ f =
  Has-left-inverseᴱ f × Has-right-inverseᴱ f

-- Has-quasi-inverseᴱ f means that f has a left inverse that is also a
-- right inverse. The proofs are erased.

Has-quasi-inverseᴱ : @0 Hom A B → Type h
Has-quasi-inverseᴱ f =
  ∃ λ f⁻¹ → Erased (f ∘ f⁻¹ ≡ id × f⁻¹ ∘ f ≡ id)

-- Some notions of isomorphism or equivalence.

infix 4 _≊ᴱ_ _≅ᴱ_

_≊ᴱ_ : Obj → Obj → Type h
A ≊ᴱ B = ∃ λ (f : Hom A B) → Is-bi-invertibleᴱ f

_≅ᴱ_ : Obj → Obj → Type h
A ≅ᴱ B = ∃ λ (f : Hom A B) → Has-quasi-inverseᴱ f

-- Morphisms with quasi-inverses are bi-invertible.

Has-quasi-inverseᴱ→Is-bi-invertibleᴱ :
  (@0 f : Hom A B) → Has-quasi-inverseᴱ f → Is-bi-invertibleᴱ f
Has-quasi-inverseᴱ→Is-bi-invertibleᴱ _ (f⁻¹ , [ f∘f⁻¹≡id , f⁻¹∘f≡id ]) =
    (f⁻¹ , [ f⁻¹∘f≡id ])
  , (f⁻¹ , [ f∘f⁻¹≡id ])

≅ᴱ→≊ᴱ : A ≅ᴱ B → A ≊ᴱ B
≅ᴱ→≊ᴱ = ∃-cong λ f → Has-quasi-inverseᴱ→Is-bi-invertibleᴱ f

-- Some conversion functions.

Has-left-inverse→Has-left-inverseᴱ :
  Has-left-inverse f → Has-left-inverseᴱ f
Has-left-inverse→Has-left-inverseᴱ = Σ-map P.id [_]→

@0 Has-left-inverse≃Has-left-inverseᴱ :
  Has-left-inverse f ≃ Has-left-inverseᴱ f
Has-left-inverse≃Has-left-inverseᴱ {f = f} =
  (∃ λ f⁻¹ →         f⁻¹ ∘ f ≡ id )  ↔⟨ (∃-cong λ _ → inverse $ erased Erased↔) ⟩□
  (∃ λ f⁻¹ → Erased (f⁻¹ ∘ f ≡ id))  □

Has-right-inverse→Has-right-inverseᴱ :
  Has-right-inverse f → Has-right-inverseᴱ f
Has-right-inverse→Has-right-inverseᴱ = Σ-map P.id [_]→

@0 Has-right-inverse≃Has-right-inverseᴱ :
  Has-right-inverse f ≃ Has-right-inverseᴱ f
Has-right-inverse≃Has-right-inverseᴱ {f = f} =
  (∃ λ f⁻¹ →         f ∘ f⁻¹ ≡ id )  ↔⟨ (∃-cong λ _ → inverse $ erased Erased↔) ⟩□
  (∃ λ f⁻¹ → Erased (f ∘ f⁻¹ ≡ id))  □

Is-bi-invertible→Is-bi-invertibleᴱ :
  Is-bi-invertible f → Is-bi-invertibleᴱ f
Is-bi-invertible→Is-bi-invertibleᴱ =
  Σ-map Has-left-inverse→Has-left-inverseᴱ
        Has-right-inverse→Has-right-inverseᴱ

@0 Is-bi-invertible≃Is-bi-invertibleᴱ :
  Is-bi-invertible f ≃ Is-bi-invertibleᴱ f
Is-bi-invertible≃Is-bi-invertibleᴱ {f = f} =
  Has-left-inverse  f × Has-right-inverse  f  ↝⟨ Has-left-inverse≃Has-left-inverseᴱ ×-cong
                                                 Has-right-inverse≃Has-right-inverseᴱ ⟩□
  Has-left-inverseᴱ f × Has-right-inverseᴱ f  □

Has-quasi-inverse→Has-quasi-inverseᴱ :
  Has-quasi-inverse f → Has-quasi-inverseᴱ f
Has-quasi-inverse→Has-quasi-inverseᴱ = Σ-map P.id [_]→

@0 Has-quasi-inverse≃Has-quasi-inverseᴱ :
  Has-quasi-inverse f ≃ Has-quasi-inverseᴱ f
Has-quasi-inverse≃Has-quasi-inverseᴱ {f = f} =
  (∃ λ f⁻¹ →         f ∘ f⁻¹ ≡ id × f⁻¹ ∘ f ≡ id )  ↔⟨ (∃-cong λ _ → inverse $ erased Erased↔) ⟩□
  (∃ λ f⁻¹ → Erased (f ∘ f⁻¹ ≡ id × f⁻¹ ∘ f ≡ id))  □

≊→≊ᴱ : A ≊ B → A ≊ᴱ B
≊→≊ᴱ = Σ-map P.id Is-bi-invertible→Is-bi-invertibleᴱ

@0 ≊≃≊ᴱ : (A ≊ B) ≃ (A ≊ᴱ B)
≊≃≊ᴱ {A = A} {B = B} =
  (∃ λ (f : Hom A B) → Is-bi-invertible  f)  ↝⟨ (∃-cong λ _ → Is-bi-invertible≃Is-bi-invertibleᴱ) ⟩□
  (∃ λ (f : Hom A B) → Is-bi-invertibleᴱ f)  □

≅→≅ᴱ : A ≅ B → A ≅ᴱ B
≅→≅ᴱ = Σ-map P.id Has-quasi-inverse→Has-quasi-inverseᴱ

@0 ≅≃≅ᴱ : (A ≅ B) ≃ (A ≅ᴱ B)
≅≃≅ᴱ {A = A} {B = B} =
  (∃ λ (f : Hom A B) → Has-quasi-inverse  f)  ↝⟨ (∃-cong λ _ → Has-quasi-inverse≃Has-quasi-inverseᴱ) ⟩□
  (∃ λ (f : Hom A B) → Has-quasi-inverseᴱ f)  □

-- The remaining code relies on some further assumptions, similar to
-- those of a precategory. However, note that Hom A B is not required
-- to be a set (some properties require Hom A A to be a set for some
-- A).

module More
  (@0 left-identity  : {A B : Obj} (f : Hom A B) → id ∘ f ≡ f)
  (@0 right-identity : {A B : Obj} (f : Hom A B) → f ∘ id ≡ f)
  (@0 associativity  : {A B C D : Obj}
                       (f : Hom C D) (g : Hom B C) (h : Hom A B) →
                       f ∘ (g ∘ h) ≡ (f ∘ g) ∘ h)
  where

  -- A workaround for Agda's lack of erased modules.

  private

    record Proofs : Type (o ⊔ h) where
      field
        lid : {A B : Obj} (f : Hom A B) → id ∘ f ≡ f
        rid : {A B : Obj} (f : Hom A B) → f ∘ id ≡ f
        ass : {A B C D : Obj}
              (f : Hom C D) (g : Hom B C) (h : Hom A B) →
              f ∘ (g ∘ h) ≡ (f ∘ g) ∘ h

    @0 proofs : Proofs
    proofs .Proofs.lid = left-identity
    proofs .Proofs.rid = right-identity
    proofs .Proofs.ass = associativity

    module BiM (p : Proofs) =
      Bi.More
        (Proofs.lid p)
        (Proofs.rid p)
        (Proofs.ass p)

  -- Bi-invertible morphisms have quasi-inverses.

  Is-bi-invertibleᴱ→Has-quasi-inverseᴱ :
    Is-bi-invertibleᴱ f → Has-quasi-inverseᴱ f
  Is-bi-invertibleᴱ→Has-quasi-inverseᴱ
    {f = f} ((f⁻¹₁ , [ f⁻¹₁∘f≡id ]) , (f⁻¹₂ , [ f∘f⁻¹₂≡id ])) =
      (f⁻¹₁ ∘ f ∘ f⁻¹₂)
    , [ (f ∘ f⁻¹₁ ∘ f ∘ f⁻¹₂    ≡⟨ cong (f ∘_) $ associativity _ _ _ ⟩
         f ∘ (f⁻¹₁ ∘ f) ∘ f⁻¹₂  ≡⟨ cong (λ f′ → f ∘ f′ ∘ f⁻¹₂) f⁻¹₁∘f≡id ⟩
         f ∘ id ∘ f⁻¹₂          ≡⟨ cong (f ∘_) $ left-identity _ ⟩
         f ∘ f⁻¹₂               ≡⟨ f∘f⁻¹₂≡id ⟩∎
         id                     ∎)
      , ((f⁻¹₁ ∘ f ∘ f⁻¹₂) ∘ f  ≡⟨ cong (λ f′ → (f⁻¹₁ ∘ f′) ∘ f) f∘f⁻¹₂≡id ⟩
         (f⁻¹₁ ∘ id) ∘ f        ≡⟨ cong (_∘ f) $ right-identity _ ⟩
         f⁻¹₁ ∘ f               ≡⟨ f⁻¹₁∘f≡id ⟩∎
         id                     ∎)
      ]

  -- Has-left-inverseᴱ f is contractible (with an erased proof) if f
  -- has a quasi-inverse (with erased proofs).

  Contractibleᴱ-Has-left-inverseᴱ :
    {@0 f : Hom A B} →
    Has-quasi-inverseᴱ f → Contractibleᴱ (Has-left-inverseᴱ f)
  Contractibleᴱ-Has-left-inverseᴱ
    {f = f} (f⁻¹ , [ f∘f⁻¹≡id , f⁻¹∘f≡id ]) =
    ECP.Contractibleᴱ-⁻¹ᴱ
      (_∘ f)
      (_∘ f⁻¹)
      (λ g →
         (g ∘ f⁻¹) ∘ f  ≡⟨ sym $ associativity _ _ _ ⟩
         g ∘ f⁻¹ ∘ f    ≡⟨ cong (g ∘_) f⁻¹∘f≡id ⟩
         g ∘ id         ≡⟨ right-identity _ ⟩∎
         g              ∎)
      (λ g →
         (g ∘ f) ∘ f⁻¹  ≡⟨ sym $ associativity _ _ _ ⟩
         g ∘ f ∘ f⁻¹    ≡⟨ cong (g ∘_) f∘f⁻¹≡id ⟩
         g ∘ id         ≡⟨ right-identity _ ⟩∎
         g              ∎)
      id

  -- Has-right-inverseᴱ f is contractible (with an erased proof) if f
  -- has a quasi-inverse (with erased proofs).

  Contractibleᴱ-Has-right-inverseᴱ :
    {@0 f : Hom A B} →
    Has-quasi-inverseᴱ f → Contractibleᴱ (Has-right-inverseᴱ f)
  Contractibleᴱ-Has-right-inverseᴱ
    {f = f} (f⁻¹ , [ f∘f⁻¹≡id , f⁻¹∘f≡id ]) =
    ECP.Contractibleᴱ-⁻¹ᴱ
      (f ∘_)
      (f⁻¹ ∘_)
      (λ g →
         f ∘ f⁻¹ ∘ g    ≡⟨ associativity _ _ _ ⟩
         (f ∘ f⁻¹) ∘ g  ≡⟨ cong (_∘ g) f∘f⁻¹≡id ⟩
         id ∘ g         ≡⟨ left-identity _ ⟩∎
         g              ∎)
      (λ g →
         f⁻¹ ∘ f ∘ g    ≡⟨ associativity _ _ _ ⟩
         (f⁻¹ ∘ f) ∘ g  ≡⟨ cong (_∘ g) f⁻¹∘f≡id ⟩
         id ∘ g         ≡⟨ left-identity _ ⟩∎
         g              ∎)
      id

  -- Is-bi-invertibleᴱ f is a proposition (in erased contexts).

  @0 Is-bi-invertibleᴱ-propositional :
    (f : Hom A B) → Is-proposition (Is-bi-invertibleᴱ f)
  Is-bi-invertibleᴱ-propositional f =     $⟨ BiM.Is-bi-invertible-propositional proofs f ⟩
    Is-proposition (Is-bi-invertible  f)  ↝⟨ H-level-cong _ 1 Is-bi-invertible≃Is-bi-invertibleᴱ ⦂ (_ → _) ⟩
    Is-proposition (Is-bi-invertibleᴱ f)  □

  -- If Hom A A is a set, where A is the domain of f, then
  -- Has-quasi-inverseᴱ f is a proposition (in erased contexts).

  @0 Has-quasi-inverseᴱ-propositional-domain :
    {f : Hom A B} →
    Is-set (Hom A A) →
    Is-proposition (Has-quasi-inverseᴱ f)
  Has-quasi-inverseᴱ-propositional-domain {f = f} s =
                                           $⟨ BiM.Has-quasi-inverse-propositional-domain proofs s ⟩
    Is-proposition (Has-quasi-inverse  f)  ↝⟨ H-level-cong _ 1 Has-quasi-inverse≃Has-quasi-inverseᴱ ⦂ (_ → _) ⟩□
    Is-proposition (Has-quasi-inverseᴱ f)  □

  -- If Hom B B is a set, where B is the codomain of f, then
  -- Has-quasi-inverseᴱ f is a proposition (in erased contexts).

  @0 Has-quasi-inverseᴱ-propositional-codomain :
    {f : Hom A B} →
    Is-set (Hom B B) →
    Is-proposition (Has-quasi-inverseᴱ f)
  Has-quasi-inverseᴱ-propositional-codomain {f = f} s =
                                           $⟨ BiM.Has-quasi-inverse-propositional-codomain proofs s ⟩
    Is-proposition (Has-quasi-inverse  f)  ↝⟨ H-level-cong _ 1 Has-quasi-inverse≃Has-quasi-inverseᴱ ⦂ (_ → _) ⟩□
    Is-proposition (Has-quasi-inverseᴱ f)  □

  -- There is a logical equivalence between Has-quasi-inverseᴱ f and
  -- Is-bi-invertibleᴱ f.

  Has-quasi-inverseᴱ⇔Is-bi-invertibleᴱ :
    Has-quasi-inverseᴱ f ⇔ Is-bi-invertibleᴱ f
  Has-quasi-inverseᴱ⇔Is-bi-invertibleᴱ = record
    { to   = Has-quasi-inverseᴱ→Is-bi-invertibleᴱ _
    ; from = Is-bi-invertibleᴱ→Has-quasi-inverseᴱ
    }

  -- There is a logical equivalence between A ≅ᴱ B and A ≊ᴱ B.

  ≅ᴱ⇔≊ᴱ : (A ≅ᴱ B) ⇔ (A ≊ᴱ B)
  ≅ᴱ⇔≊ᴱ = ∃-cong λ _ → Has-quasi-inverseᴱ⇔Is-bi-invertibleᴱ

  -- Is-bi-invertibleᴱ and Has-quasi-inverseᴱ are equivalent (with
  -- erased proofs) for morphisms with domain A for which Hom A A is a
  -- set.

  Is-bi-invertibleᴱ≃ᴱHas-quasi-inverseᴱ-domain :
    {f : Hom A B} →
    @0 Is-set (Hom A A) →
    Is-bi-invertibleᴱ f ≃ᴱ Has-quasi-inverseᴱ f
  Is-bi-invertibleᴱ≃ᴱHas-quasi-inverseᴱ-domain s = EEq.⇔→≃ᴱ
    (Is-bi-invertibleᴱ-propositional _)
    (Has-quasi-inverseᴱ-propositional-domain s)
    (_⇔_.from Has-quasi-inverseᴱ⇔Is-bi-invertibleᴱ)
    (_⇔_.to   Has-quasi-inverseᴱ⇔Is-bi-invertibleᴱ)

  -- Is-bi-invertibleᴱ and Has-quasi-inverseᴱ are equivalent (with
  -- erased proofs) for morphisms with codomain B for which Hom B B is
  -- a set.

  Is-bi-invertibleᴱ≃ᴱHas-quasi-inverseᴱ-codomain :
    {f : Hom A B} →
    @0 Is-set (Hom B B) →
    Is-bi-invertibleᴱ f ≃ᴱ Has-quasi-inverseᴱ f
  Is-bi-invertibleᴱ≃ᴱHas-quasi-inverseᴱ-codomain s = EEq.⇔→≃ᴱ
    (Is-bi-invertibleᴱ-propositional _)
    (Has-quasi-inverseᴱ-propositional-codomain s)
    (_⇔_.from Has-quasi-inverseᴱ⇔Is-bi-invertibleᴱ)
    (_⇔_.to   Has-quasi-inverseᴱ⇔Is-bi-invertibleᴱ)

  -- A ≊ᴱ B and A ≅ᴱ B are equivalent (with erased proofs) if Hom A A
  -- is a set.

  ≊ᴱ≃ᴱ≅ᴱ-domain :
    @0 Is-set (Hom A A) →
    (A ≊ᴱ B) ≃ᴱ (A ≅ᴱ B)
  ≊ᴱ≃ᴱ≅ᴱ-domain s =
    ∃-cong λ _ → Is-bi-invertibleᴱ≃ᴱHas-quasi-inverseᴱ-domain s

  -- A ≊ᴱ B and A ≅ᴱ B are equivalent (with erased proofs) if Hom B B
  -- is a set.

  ≊ᴱ≃ᴱ≅ᴱ-codomain :
    @0 Is-set (Hom B B) →
    (A ≊ᴱ B) ≃ᴱ (A ≅ᴱ B)
  ≊ᴱ≃ᴱ≅ᴱ-codomain s =
    ∃-cong λ _ → Is-bi-invertibleᴱ≃ᴱHas-quasi-inverseᴱ-codomain s

  -- An equality characterisation lemma for _≊ᴱ_.

  @0 equality-characterisation-≊ᴱ :
    (f g : A ≊ᴱ B) → (f ≡ g) ≃ (proj₁ f ≡ proj₁ g)
  equality-characterisation-≊ᴱ f g =
    f ≡ g                              ↝⟨ inverse $ Eq.≃-≡ (inverse ≊≃≊ᴱ) ⟩
    _≃_.from ≊≃≊ᴱ f ≡ _≃_.from ≊≃≊ᴱ g  ↝⟨ BiM.equality-characterisation-≊ proofs _ _ ⟩□
    proj₁ f ≡ proj₁ g                  □

  -- Two equality characterisation lemmas for _≅ᴱ_.

  @0 equality-characterisation-≅ᴱ-domain :
    Is-set (Hom A A) →
    (f g : A ≅ᴱ B) → (f ≡ g) ≃ (proj₁ f ≡ proj₁ g)
  equality-characterisation-≅ᴱ-domain s f g =
    f ≡ g                              ↝⟨ inverse $ Eq.≃-≡ (inverse ≅≃≅ᴱ) ⟩
    _≃_.from ≅≃≅ᴱ f ≡ _≃_.from ≅≃≅ᴱ g  ↝⟨ BiM.equality-characterisation-≅-domain proofs s _ _ ⟩□
    proj₁ f ≡ proj₁ g                  □

  @0 equality-characterisation-≅ᴱ-codomain :
    Is-set (Hom B B) →
    (f g : A ≅ᴱ B) → (f ≡ g) ≃ (proj₁ f ≡ proj₁ g)
  equality-characterisation-≅ᴱ-codomain s f g =
    f ≡ g                              ↝⟨ inverse $ Eq.≃-≡ (inverse ≅≃≅ᴱ) ⟩
    _≃_.from ≅≃≅ᴱ f ≡ _≃_.from ≅≃≅ᴱ g  ↝⟨ BiM.equality-characterisation-≅-codomain proofs s _ _ ⟩□
    proj₁ f ≡ proj₁ g                  □

  -- If f : Hom A B has a quasi-inverse, then Has-quasi-inverseᴱ f is
  -- equivalent to id ≡ id (in erased contexts), where id stands for
  -- either the identity at A or at B.

  @0 Has-quasi-inverseᴱ≃id≡id-domain :
    {f : Hom A B} →
    Has-quasi-inverseᴱ f →
    Has-quasi-inverseᴱ f ≃ (id ≡ id {A = A})
  Has-quasi-inverseᴱ≃id≡id-domain {f = f} q-inv =
    Has-quasi-inverseᴱ f  ↝⟨ inverse Has-quasi-inverse≃Has-quasi-inverseᴱ ⟩
    Has-quasi-inverse f   ↝⟨ BiM.Has-quasi-inverse≃id≡id-domain proofs (_≃_.from Has-quasi-inverse≃Has-quasi-inverseᴱ q-inv) ⟩□
    id ≡ id               □

  @0 Has-quasi-inverseᴱ≃id≡id-codomain :
    {f : Hom A B} →
    Has-quasi-inverseᴱ f →
    Has-quasi-inverseᴱ f ≃ (id ≡ id {A = B})
  Has-quasi-inverseᴱ≃id≡id-codomain {f = f} q-inv =
    Has-quasi-inverseᴱ f  ↝⟨ inverse Has-quasi-inverse≃Has-quasi-inverseᴱ ⟩
    Has-quasi-inverse f   ↝⟨ BiM.Has-quasi-inverse≃id≡id-codomain proofs (_≃_.from Has-quasi-inverse≃Has-quasi-inverseᴱ q-inv) ⟩□
    id ≡ id               □

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
------------------------------------------------------------------------------
-- The gcd is divisible by any common divisor (using equational reasoning)
------------------------------------------------------------------------------

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

module FOTC.Program.GCD.Partial.DivisibleI where

open import FOTC.Base
open import FOTC.Base.PropertiesI
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Divisibility.NotBy0
open import FOTC.Data.Nat.Divisibility.NotBy0.PropertiesI
open import FOTC.Data.Nat.Induction.NonAcc.LexicographicI
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.EliminationPropertiesI
open import FOTC.Data.Nat.Inequalities.PropertiesI
open import FOTC.Data.Nat.PropertiesI
open import FOTC.Program.GCD.Partial.ConversionRulesI
open import FOTC.Program.GCD.Partial.Definitions
open import FOTC.Program.GCD.Partial.GCD

------------------------------------------------------------------------------
-- The gcd 0 (succ n) is Divisible.
gcd-0S-Divisible : ∀ {n} → N n → Divisible zero (succ₁ n) (gcd zero (succ₁ n))
gcd-0S-Divisible {n} _ c _ (c∣0 , c∣Sn) = subst (_∣_ c) (sym (gcd-0S n)) c∣Sn

------------------------------------------------------------------------------
-- The gcd (succ₁ n) 0 is Divisible.
gcd-S0-Divisible : ∀ {n} → N n → Divisible (succ₁ n) zero (gcd (succ₁ n) zero)
gcd-S0-Divisible {n} _ c _ (c∣Sn , c∣0) = subst (_∣_ c) (sym (gcd-S0 n)) c∣Sn

------------------------------------------------------------------------------
-- The gcd (succ₁ m) (succ₁ n) when succ₁ m > succ₁ n is Divisible.
gcd-S>S-Divisible :
  ∀ {m n} → N m → N n →
  (Divisible (succ₁ m ∸ succ₁ n) (succ₁ n) (gcd (succ₁ m ∸ succ₁ n) (succ₁ n))) →
  succ₁ m > succ₁ n →
  Divisible (succ₁ m) (succ₁ n) (gcd (succ₁ m) (succ₁ n))
gcd-S>S-Divisible {m} {n} Nm Nn acc Sm>Sn c Nc (c∣Sm , c∣Sn) =
{-
Proof:
   ----------------- (Hip.)
     c | m    c | n
   ---------------------- (Thm.)   -------- (Hip.)
       c | (m ∸ n)                   c | n
     ------------------------------------------ (IH)
              c | gcd m (n ∸ m)                          m > n
             --------------------------------------------------- (gcd def.)
                             c | gcd m n
-}
 subst (_∣_ c) (sym (gcd-S>S m n Sm>Sn)) (acc c Nc (c|Sm-Sn , c∣Sn))
 where
 c|Sm-Sn : c ∣ succ₁ m ∸ succ₁ n
 c|Sm-Sn = x∣y→x∣z→x∣y∸z Nc (nsucc Nm) (nsucc Nn) c∣Sm c∣Sn

------------------------------------------------------------------------------
-- The gcd (succ₁ m) (succ₁ n) when succ₁ m ≯ succ₁ n is Divisible.
gcd-S≯S-Divisible :
  ∀ {m n} → N m → N n →
  (Divisible (succ₁ m) (succ₁ n ∸ succ₁ m) (gcd (succ₁ m) (succ₁ n ∸ succ₁ m))) →
  succ₁ m ≯ succ₁ n →
  Divisible (succ₁ m) (succ₁ n) (gcd (succ₁ m) (succ₁ n))
gcd-S≯S-Divisible {m} {n} Nm Nn acc Sm≯Sn c Nc (c∣Sm , c∣Sn) =
{-
Proof
                            ----------------- (Hip.)
                                c | m    c | n
        -------- (Hip.)       ---------------------- (Thm.)
         c | m                      c | n ∸ m
     ------------------------------------------ (IH)
              c | gcd m (n ∸ m)                          m ≯ n
             --------------------------------------------------- (gcd def.)
                             c | gcd m n
-}

  subst (_∣_ c) (sym (gcd-S≯S m n Sm≯Sn)) (acc c Nc (c∣Sm , c|Sn-Sm))
  where
  c|Sn-Sm : c ∣ succ₁ n ∸ succ₁ m
  c|Sn-Sm = x∣y→x∣z→x∣y∸z Nc (nsucc Nn) (nsucc Nm) c∣Sn c∣Sm

------------------------------------------------------------------------------
-- The gcd m n when m > n is Divisible.
gcd-x>y-Divisible :
  ∀ {m n} → N m → N n →
  (∀ {o p} → N o → N p → Lexi o p m n → x≢0≢y o p →
             Divisible o p (gcd o p)) →
  m > n →
  x≢0≢y m n →
  Divisible m n (gcd m n)
gcd-x>y-Divisible nzero nzero _ _ ¬0≡0∧0≡0 _ _  = ⊥-elim (¬0≡0∧0≡0 (refl , refl))
gcd-x>y-Divisible nzero (nsucc Nn) _ 0>Sn _ _ _ = ⊥-elim (0>x→⊥ (nsucc Nn) 0>Sn)
gcd-x>y-Divisible (nsucc Nm) nzero _ _ _  c Nc  = gcd-S0-Divisible Nm c Nc
gcd-x>y-Divisible (nsucc {m} Nm) (nsucc {n} Nn) ah Sm>Sn _ c Nc =
  gcd-S>S-Divisible Nm Nn ih Sm>Sn c Nc
  where
  -- Inductive hypothesis.
  ih : Divisible (succ₁ m ∸ succ₁ n) (succ₁ n) (gcd (succ₁ m ∸ succ₁ n) (succ₁ n))
  ih = ah {succ₁ m ∸ succ₁ n}
          {succ₁ n}
          (∸-N (nsucc Nm) (nsucc Nn))
          (nsucc Nn)
          ([Sx∸Sy,Sy]<[Sx,Sy] Nm Nn)
          (λ p → ⊥-elim (S≢0 (∧-proj₂ p)))

------------------------------------------------------------------------------
-- The gcd m n when m ≯ n is Divisible.
gcd-x≯y-Divisible :
  ∀ {m n} → N m → N n →
  (∀ {o p} → N o → N p → Lexi o p m n → x≢0≢y o p →
             Divisible o p (gcd o p)) →
  m ≯ n →
  x≢0≢y m n →
  Divisible m n (gcd m n)
gcd-x≯y-Divisible nzero nzero _ _ h _ _   = ⊥-elim (h (refl , refl))
gcd-x≯y-Divisible nzero (nsucc Nn) _ _  _  c Nc  = gcd-0S-Divisible Nn c Nc
gcd-x≯y-Divisible (nsucc _) nzero _ Sm≯0 _ _ _  = ⊥-elim (S≯0→⊥ Sm≯0)
gcd-x≯y-Divisible (nsucc {m} Nm) (nsucc {n} Nn) ah Sm≯Sn _ c Nc =
  gcd-S≯S-Divisible Nm Nn ih Sm≯Sn c Nc
  where
  -- Inductive hypothesis.
  ih : Divisible (succ₁ m) (succ₁ n ∸ succ₁ m) (gcd (succ₁ m) (succ₁ n ∸ succ₁ m))
  ih = ah {succ₁ m}
          {succ₁ n ∸ succ₁ m}
          (nsucc Nm)
          (∸-N (nsucc Nn) (nsucc Nm))
          ([Sx,Sy∸Sx]<[Sx,Sy] Nm Nn)
          (λ p → ⊥-elim (S≢0 (∧-proj₁ p)))

------------------------------------------------------------------------------
-- The gcd is Divisible.
gcdDivisible : ∀ {m n} → N m → N n → x≢0≢y m n → Divisible m n (gcd m n)
gcdDivisible = Lexi-wfind A h
  where
  A : D → D → Set
  A i j = x≢0≢y i j → Divisible i j (gcd i j)

  h : ∀ {i j} → N i → N j → (∀ {k l} → N k → N l → Lexi k l i j → A k l) →
      A i j
  h Ni Nj ah = case (gcd-x>y-Divisible Ni Nj ah)
                    (gcd-x≯y-Divisible Ni Nj ah)
                    (x>y∨x≯y Ni Nj)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module Control.Category where

open import Level using (suc; _⊔_)
open import Relation.Binary hiding (_⇒_)
open import Relation.Binary.PropositionalEquality

-- Module HomSet provides notation A ⇒ B for the Set of morphisms
-- from between objects A and B and names _≈_ and ≈-refl/sym/trans
-- for the equality of morphisms.

module HomSet {o h e} {Obj : Set o} (Hom : Obj → Obj → Setoid h e) where

  _⇒_ : (A B : Obj) → Set h
  A ⇒ B = Setoid.Carrier (Hom A B)

  module _ {A B : Obj} where
    open Setoid (Hom A B) public
      using (_≈_)
      renaming ( isEquivalence to ≈-equiv
               ; refl          to ≈-refl
               ; sym           to ≈-sym
               ; trans         to ≈-trans
               )
{-
  _≈_ : {A B : Obj} → Rel (A ⇒ B) e
  _≈_ {A = A}{B = B} = Setoid._≈_ (Hom A B)

  ≈-equiv : {A B : Obj}  → IsEquivalence (Setoid._≈_ (Hom A B))
  ≈-equiv {A = A}{B = B} = Setoid.isEquivalence (Hom A B)

  ≈-refl  : {A B : Obj}  → Reflexive _≈_
  ≈-refl  {A = A}{B = B} = Setoid.refl (Hom A B)

  ≈-sym   : {A B : Obj}  → Symmetric _≈_
  ≈-sym   {A = A}{B = B} = Setoid.sym (Hom A B)

  ≈-trans : {A B : Obj}  → Transitive _≈_
  ≈-trans {A = A}{B = B} = Setoid.trans (Hom A B)
-}

-- Category operations: identity and composition.

-- Module T-CategoryOps Hom provides the types of
-- identity and composition (forward and backward).

module T-CategoryOps {o h e} {Obj : Set o} (Hom : Obj → Obj → Setoid h e) where

  open HomSet Hom

  T-id = ∀ {A}                            → A ⇒ A
  T-⟫  = ∀ {A B C} (f : A ⇒ B) (g : B ⇒ C) → A ⇒ C
  T-∘  = ∀ {A B C} (g : B ⇒ C) (f : A ⇒ B) → A ⇒ C

-- Record CategoryOps Hom can be instantiated to implement
-- identity and composition for category Hom.

record CategoryOps {o h e} {Obj : Set o} (Hom : Obj → Obj → Setoid h e)
    : Set (o ⊔ h ⊔ e)
  where
  open T-CategoryOps Hom

  infixl 9 _⟫_
  infixr 9 _∘_

  field
    id : T-id
    _⟫_ : T-⟫

  _∘_ : T-∘
  g ∘ f = f ⟫ g

-- Category laws: left and right identity and composition.

-- Module T-CategoryLaws ops provides the types of the laws
-- for the category operations ops.

module T-CategoryLaws {o h e} {Obj : Set o} {Hom : Obj → Obj → Setoid h e}
    (ops : CategoryOps Hom)
  where
  open HomSet Hom public
  open T-CategoryOps Hom public
  open CategoryOps ops public

  T-id-first = ∀ {A B} {g : A ⇒ B} →

    (id ⟫ g) ≈ g

  T-id-last  = ∀ {A B} {f : A ⇒ B} →

    (f ⟫ id) ≈ f

  T-∘-assoc  = ∀ {A B C D} (f : A ⇒ B) {g : B ⇒ C} {h : C ⇒ D} →

    ((f ⟫ g) ⟫ h) ≈ (f ⟫ (g ⟫ h))

  T-∘-cong = ∀ {A B C} {f f′ : A ⇒ B} {g g′ : B ⇒ C} →
    f ≈ f′ → g ≈ g′ → (f ⟫ g) ≈ (f′ ⟫ g′)

-- Record CategoryLaws ops can be instantiated to prove the laws of the
-- category operations (identity and compositions).

record CategoryLaws {o h e} {Obj : Set o} {Hom : Obj → Obj → Setoid h e}
    (ops : CategoryOps Hom) : Set (o ⊔ h ⊔ e)
  where
  open T-CategoryLaws ops

  field
    id-first : T-id-first
    id-last  : T-id-last
    ∘-assoc  : T-∘-assoc
    ∘-cong   : T-∘-cong

-- Record IsCategory Hom contains the data (operations and laws) to make
-- Hom a category.

record IsCategory {o h e} {Obj : Set o} (Hom : Obj → Obj → Setoid h e) : Set (o ⊔ h ⊔ e) where

  field
    ops  : CategoryOps Hom
    laws : CategoryLaws ops

  open HomSet        Hom public
  open CategoryOps   ops public
  open CategoryLaws laws public

-- The category: packaging objects, morphisms, and laws.

record Category o h e : Set (suc (o ⊔ h ⊔ e)) where
   field
     {Obj}      : Set o
     Hom        : Obj → Obj → Setoid h e
     isCategory : IsCategory Hom

   open IsCategory isCategory public

-- Initial object

record IsInitial {o h e} {Obj : Set o} (Hom : Obj → Obj → Setoid h e) (Initial : Obj) : Set (h ⊔ o ⊔ e) where
  open HomSet Hom
  open T-CategoryOps Hom
  field
    initial           : ∀ {A}                   → Initial ⇒ A
    initial-universal : ∀ {A} {f : Initial ⇒ A} → f ≈ initial

-- Terminal object

record IsFinal {o h e} {Obj : Set o} (Hom : Obj → Obj → Setoid h e) (Final : Obj) : Set (h ⊔ o ⊔ e) where
  open HomSet Hom
  open T-CategoryOps Hom
  field
    final           : ∀ {A}                 → A ⇒ Final
    final-universal : ∀ {A} {f : A ⇒ Final} → f ≈ final

max_stars_repo_name: andreasabel/cubical

max_issues_repo_name: andreasabel/cubical

max_forks_repo_name: andreasabel/cubical


text:
module Cats.Category.Cat.Facts.Initial where

open import Cats.Category
open import Cats.Category.Cat using (Cat)
open import Cats.Category.Zero using (Zero)
open import Cats.Functor

module _ {lo la l≈} where

  open Category (Cat lo la l≈)

  Zero-Initial : IsInitial (Zero lo la l≈)
  Zero-Initial X = ∃!-intro f _ f-Unique
    where
      f : Functor (Zero lo la l≈) X
      f = record
          { fobj = λ()
          ; fmap = λ{}
          ; fmap-resp = λ{}
          ; fmap-id = λ{}
          ; fmap-∘ = λ{}
          }

      f-Unique : IsUnique f
      f-Unique f′ = record
          { iso = λ{}
          ; forth-natural = λ{}
          }

instance
  hasInitial : ∀ lo la l≈ → HasInitial (Cat lo la l≈)
  hasInitial lo la l≈ = record
      { Zero = Zero lo la l≈
      ; isInitial = Zero-Initial
      }

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
module Issue361 where

data _==_ {A : Set}(a : A) : A -> Set where
  refl : a == a

postulate
  A : Set
  a b : A
  F : A -> Set

record R (a : A) : Set where
  constructor c
  field
    p : A

beta : (x : A) -> R.p {b} (c {b} x) == x
beta x = refl

lemma : (r : R a) -> R.p {b} (c {b} (R.p {a} r)) == R.p {a} r
lemma r = beta (R.p {a} r)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
open import lib

module rtn (gratr2-nt : Set) where

gratr2-rule : Set
gratr2-rule =  maybe string × maybe string × maybe gratr2-nt × 𝕃 (gratr2-nt ⊎ char)

record gratr2-rtn : Set where
  field
    start : gratr2-nt
    _eq_ : gratr2-nt → gratr2-nt → 𝔹
    gratr2-start : gratr2-nt → 𝕃 gratr2-rule
    gratr2-return : maybe gratr2-nt → 𝕃 gratr2-rule

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
------------------------------------------------------------------------
-- Definitions of combinatorial functions on integers
------------------------------------------------------------------------

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

module Math.Combinatorics.IntegerFunction where

open import Data.Nat hiding (_*_)
open import Data.Integer

import Math.Combinatorics.Function as ℕF

[-1]^_ : ℕ → ℤ
[-1]^ 0               = + 1
[-1]^ 1               = - (+ 1)
[-1]^ ℕ.suc (ℕ.suc n) = [-1]^ n

------------------------------------------------------------------------
-- Permutation, Falling factorial
-- P n k = n * (n - 1) * ... * (n - k + 1)  (k terms)

P : ℤ → ℕ → ℤ
P (+ n)      k = + (ℕF.P n k)
P (-[1+ n ]) k = [-1]^ k * (+ ℕF.Poch (ℕ.suc n) k)


text:
open import Agda.Builtin.Unit
open import Agda.Builtin.List
open import Agda.Builtin.Reflection

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

macro
  tac : Term → TC ⊤
  tac hole =
    unify hole
      (def (quote id)
         (arg (arg-info visible (modality relevant quantity-ω))
              (var 0 []) ∷
          []))

test : {A : Set} → A → A
test x = {!tac!}

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
{-# OPTIONS --safe #-}
module Squaring where

open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Product
open import Data.Bool hiding (_≤_;_<_)
open import Data.Nat.Properties

open ≡-Reasoning

div-mod2 : ℕ → ℕ × Bool
div-mod2 0 = 0 , false
div-mod2 (suc 0) = 0 , true
div-mod2 (suc (suc n)) = let q , r = div-mod2 n in suc q , r

-- The first argument (k) helps Agda to prove
-- that the function terminates
pow-sqr-aux : ℕ → ℕ → ℕ → ℕ
pow-sqr-aux 0 _ _ = 1
pow-sqr-aux _ _ 0 = 1
pow-sqr-aux (suc k) b e with div-mod2 e
... | e' , false = pow-sqr-aux k (b * b) e'
... | e' , true = b * pow-sqr-aux k (b * b) e'

pow-sqr : ℕ → ℕ → ℕ
pow-sqr b e = pow-sqr-aux e b e

div-mod2-spec : ∀ n → let q , r = div-mod2 n in 2 * q + (if r then 1 else 0) ≡ n
div-mod2-spec 0 = refl
div-mod2-spec 1 = refl
div-mod2-spec (suc (suc n)) with div-mod2 n | div-mod2-spec n
... | q , r | eq rewrite +-suc q (q + 0) | eq = refl

div-mod2-lt : ∀ n → 0 < n → proj₁ (div-mod2 n) < n
div-mod2-lt 0 lt = lt
div-mod2-lt 1 lt = lt
div-mod2-lt 2 lt = s≤s (s≤s z≤n)
div-mod2-lt (suc (suc (suc n))) lt with
  div-mod2 (suc n) | div-mod2-lt (suc n) (s≤s z≤n)
... | q , r | ih = ≤-step (s≤s ih)

pow-lemma : ∀ b e → (b * b) ^ e ≡ b ^ (2 * e)
pow-lemma b e = begin
  (b * b) ^ e ≡⟨ cong (λ t → (b * t) ^ e) (sym (*-identityʳ b)) ⟩
  (b ^ 2) ^ e ≡⟨ ^-*-assoc b 2 e ⟩
  b ^ (2 * e) ∎

pow-sqr-lemma : ∀ k b e → e ≤ k → pow-sqr-aux k b e ≡ b ^ e
pow-sqr-lemma 0 _ 0 _ = refl
pow-sqr-lemma (suc k) _ 0 _ = refl
pow-sqr-lemma (suc k) b (suc e) (s≤s le) with
  div-mod2 (suc e) | div-mod2-spec (suc e) | div-mod2-lt (suc e) (s≤s z≤n)
... | e' , false | eq | lt = begin
  pow-sqr-aux k (b * b) e' ≡⟨ pow-sqr-lemma k (b * b) e' (≤-trans (≤-pred lt) le) ⟩
  (b * b) ^ e' ≡⟨ pow-lemma b e' ⟩
  b ^ (2 * e') ≡⟨ cong (b ^_) (trans (sym (+-identityʳ (e' + (e' + 0)))) eq) ⟩
  b ^ suc e ∎
... | e' , true | eq | lt = cong (b *_) (begin
  pow-sqr-aux k (b * b) e' ≡⟨ pow-sqr-lemma k (b * b) e' (≤-trans (≤-pred lt) le) ⟩
  (b * b) ^ e' ≡⟨ pow-lemma b e' ⟩
  b ^ (2 * e') ≡⟨ cong (b ^_) (suc-injective (trans (+-comm 1 _) eq)) ⟩
  b ^ e ∎)

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


text:
module TemporalOps.StrongMonad where

open import CategoryTheory.Instances.Reactive
open import CategoryTheory.Functor
open import CategoryTheory.Monad
open import CategoryTheory.Comonad
open import CategoryTheory.NatTrans
open import CategoryTheory.BCCCs
open import CategoryTheory.CartesianStrength

open import TemporalOps.Next
open import TemporalOps.Delay
open import TemporalOps.Diamond
open import TemporalOps.Diamond.Join
open import TemporalOps.Box
open import TemporalOps.Common.Other
open import TemporalOps.Common.Compare
open import TemporalOps.Common.Rewriting
open import TemporalOps.OtherOps

open import Relation.Binary.PropositionalEquality as ≡ hiding (inspect)
open import Data.Product
open import Data.Sum
open import Data.Nat hiding (_*_)
open import Data.Nat.Properties
            using (+-identityʳ ; +-comm ; +-suc ; +-assoc)

open import Holes.Term using (⌞_⌟)
open import Holes.Cong.Propositional

open Monad M-◇
open Comonad W-□
private module F-◇ = Functor F-◇
private module F-□ = Functor F-□
open ≡.≡-Reasoning

◇-□-Strong : WStrongMonad ℝeactive-cart M-◇ W-cart-□
◇-□-Strong = record
    { st = st-◇
    ; st-nat₁ = st-nat₁-◇
    ; st-nat₂ = st-nat₂-◇
    ; st-λ = st-λ-◇
    ; st-α = st-α-◇
    ; st-η = refl
    ; st-μ = λ{A}{B}{n}{a} -> st-μ-◇ {A}{B}{n}{a}
    }
    where
    open Functor F-◇ renaming (fmap to ◇-f ; omap to ◇-o)
    open Functor F-□ renaming (fmap to □-f ; omap to □-o)
    private module ▹ᵏ-C k = CartesianFunctor (F-cart-delay k)
    private module ▹ᵏ-F k = Functor (F-delay k)
    private module ▹-F = Functor F-▹
    private module ▹-C = CartesianFunctor (F-cart-▹)
    private module □-C = CartesianFunctor (F-cart-□)
    private module □-CW = CartesianComonad (W-cart-□)
    private module □-▹ᵏ k = _⟹_ (□-to-▹ᵏ k)

    st-◇ : ∀(A B : τ) -> □ A ⊗ ◇ B ⇴ ◇ (□ A ⊗ B)
    st-◇ A B n (□A , (k , a)) = k , ▹ᵏ-C.m k (□ A) B n (□-▹ᵏ.at k (□ A) n (δ.at A k □A) , a)

    st-nat₁-◇ : ∀{A B C : τ} (f : A ⇴ B)
             -> ◇-f (□-f f * id) ∘ st-◇ A C ≈ st-◇ B C ∘ □-f f * id
    st-nat₁-◇ {A} {B} {C} f {n} {□A , k , a}
        rewrite ▹ᵏ-C.m-nat₁ k (□-f f)
                {n} {(□-▹ᵏ.at k (□ A) n (δ.at A k □A)) , a}
              | (□-▹ᵏ.nat-cond k {□ A} {□ B} {□-f f} {n} {δ.at A k □A})
        = refl

    st-nat₂-◇ : ∀{A B C : τ} (f : A ⇴ B)
             -> ◇-f (id * f) ∘ st-◇ C A ≈ st-◇ C B ∘ id * ◇-f f
    st-nat₂-◇ {A} {B} {C} f {n} {□C , k , a}
        rewrite ▹ᵏ-C.m-nat₂ k f {n} {□-▹ᵏ.at k (□ C) n (δ.at C k □C) , a} = refl

    st-λ-◇ : ∀{A} -> ◇-f π₂ ∘ st-◇ ⊤ A ≈ π₂
    st-λ-◇ {A} {n} {□⊤ , (k , a)} =
        begin
            ◇-f π₂ n (st-◇ ⊤ A n (□⊤ , (k , a)))
        ≡⟨⟩
            ◇-f π₂ n (k , ▹ᵏ-C.m k (□ ⊤) A n (□-▹ᵏ.at k (□ ⊤) n (δ.at ⊤ n □⊤) , a))
        ≡⟨⟩
            k , ▹ᵏ-F.fmap k π₂ n (▹ᵏ-C.m k (□ ⊤) A n (□-▹ᵏ.at k (□ ⊤) n (δ.at ⊤ n □⊤) , a))
        ≡⟨ cong (λ x -> k , x) lemma ⟩
            k , a
        ∎
        where
        lemma : ▹ᵏ-F.fmap k π₂ ∘ ▹ᵏ-C.m k (□ ⊤) A ≈ π₂
        lemma {n} {t , b} =
            begin
                ▹ᵏ-F.fmap k π₂ n (▹ᵏ-C.m k (□ ⊤) A n (t , b))
            ≡⟨⟩
                ▹ᵏ-F.fmap k π₂ n (▹ᵏ-C.m k (□ ⊤) A n (⌞ t ⌟ , b))
            ≡⟨ cong! (▹ᵏ-F.fmap-id k {□ ⊤}{n}{t}) ⟩
                ▹ᵏ-F.fmap k π₂ n (▹ᵏ-C.m k (□ ⊤) A n (▹ᵏ-F.fmap k ⌞ id ⌟ n t , b))
            ≡⟨⟩
                ▹ᵏ-F.fmap k π₂ n (▹ᵏ-C.m k (□ ⊤) A n (⌞ ▹ᵏ-F.fmap k (u ∘ ε.at ⊤) n t ⌟ , b))
            ≡⟨ cong! (▹ᵏ-F.fmap-∘ k) ⟩
                ▹ᵏ-F.fmap k π₂ n (▹ᵏ-C.m k (□ ⊤) A n (▹ᵏ-F.fmap k u n (▹ᵏ-F.fmap k (ε.at ⊤) n t) , b))
            ≡⟨ cong (▹ᵏ-F.fmap k π₂ n) (sym (▹ᵏ-C.m-nat₁ k u)) ⟩
                ▹ᵏ-F.fmap k π₂ n (▹ᵏ-F.fmap k (u * id) n (▹ᵏ-C.m k ⊤ A n (▹ᵏ-F.fmap k (ε.at ⊤) n t , b)))
            ≡⟨ sym (▹ᵏ-F.fmap-∘ k) ⟩
                ▹ᵏ-F.fmap k (π₂ ∘ u * id) n (▹ᵏ-C.m k ⊤ A n (▹ᵏ-F.fmap k (ε.at ⊤) n t , b))
            ≡⟨⟩
                ▹ᵏ-F.fmap k π₂ n (▹ᵏ-C.m k ⊤ A n (⌞ ▹ᵏ-F.fmap k (ε.at ⊤) n t ⌟ , b))
            ≡⟨ cong! (⊤-eq k n t) ⟩
                ▹ᵏ-F.fmap k π₂ n (▹ᵏ-C.m k ⊤ A n (▹ᵏ-C.u k n top.tt , b))
            ≡⟨ ▹ᵏ-C.unital-left k ⟩
                b
            ∎
            where
            ⊤-eq : ∀ k n t -> ▹ᵏ-F.fmap k (ε.at ⊤) n t ≡ ▹ᵏ-C.u k n top.tt
            ⊤-eq zero n t = refl
            ⊤-eq (suc k) zero t = refl
            ⊤-eq (suc k) (suc n) t = ⊤-eq k n t

    st-α-◇ : ∀{A B C : τ}
          -> st-◇ A (□ B ⊗ C) ∘ id * st-◇ B C ∘ assoc-right ∘ m⁻¹ A B * id
           ≈ ◇-f (assoc-right ∘ m⁻¹ A B * id) ∘ st-◇ (A ⊗ B) C
    st-α-◇ {A} {B} {C} {n} {□A⊗B , (k , a)} =
        begin
            st-◇ A (□ B ⊗ C) n
                (□-f π₁ n □A⊗B , st-◇ B C n (□-f π₂ n □A⊗B , (k , a)))
        ≡⟨ cong (λ x → k , x) (
            begin
                ▹ᵏ-C.m k (□ A) (□ B ⊗ C) n
                    ( □-▹ᵏ.at k (□ A) n (δ.at A k (□-f π₁ n □A⊗B))
                    , ▹ᵏ-C.m k (□ B) C n (□-▹ᵏ.at k (□ B) n (δ.at B n (□-f π₂ n □A⊗B)) , a))
            ≡⟨⟩ -- Naturality and definitional equality
                ▹ᵏ-C.m k (□ A) (□ B ⊗ C) n
                    ((id {delay □ A by k} * ▹ᵏ-C.m k (□ B) C) n (assoc-right {delay □ A by k} {delay □ B by k} {delay C by k} n
                        (((□-▹ᵏ.at k (□ A) * □-▹ᵏ.at k (□ B)) n
                            ((δ.at A * δ.at B) n (m⁻¹ A B n □A⊗B)))
                        , a)))
            ≡⟨ ▹ᵏ-C.associative k  ⟩
                ▹ᵏ-F.fmap k assoc-right n
                    (▹ᵏ-C.m k (□ A ⊗ □ B) C n
                        ( ⌞ ▹ᵏ-C.m k (□ A) (□ B) n
                            ((□-▹ᵏ.at k (□ A) * □-▹ᵏ.at k (□ B)) n
                                ((δ.at A * δ.at B) n (m⁻¹ A B n □A⊗B))) ⌟
                        , a))
            ≡⟨ cong! (lemma k) ⟩
                ▹ᵏ-F.fmap k assoc-right n
                    (▹ᵏ-C.m k (□ A ⊗ □ B) C n
                        ( □-▹ᵏ.at k (□ A ⊗ □ B) n
                            (□-C.m (□ A) (□ B) n ((δ.at A * δ.at B) n (m⁻¹ A B n □A⊗B)))
                        , a))
            ≡⟨⟩
                ▹ᵏ-F.fmap k assoc-right n
                    (▹ᵏ-C.m k (□ A ⊗ □ B) C n
                        ( ⌞ □-▹ᵏ.at k (□ A ⊗ □ B) n
                            (□-f (m⁻¹ A B) n (δ.at (A ⊗ B) k □A⊗B)) ⌟
                        , a))
            ≡⟨ cong! (□-▹ᵏ.nat-cond k {f = m⁻¹ A B} {n} {δ.at (A ⊗ B) k □A⊗B}) ⟩
                ▹ᵏ-F.fmap k assoc-right n
                    ⌞ (▹ᵏ-C.m k (□ A ⊗ □ B) C n
                        (▹ᵏ-F.fmap k (m⁻¹ A B) n
                            (□-▹ᵏ.at k (□ (A ⊗ B)) n (δ.at (A ⊗ B) k □A⊗B))
                        , a)) ⌟
            ≡⟨ cong! (▹ᵏ-C.m-nat₁ k (m⁻¹ A B) {n}
                        {(□-▹ᵏ.at k (□ (A ⊗ B)) n (δ.at (A ⊗ B) k □A⊗B)) , a}) ⟩
                ▹ᵏ-F.fmap k assoc-right n
                    (▹ᵏ-F.fmap k (m⁻¹ A B * id) n (▹ᵏ-C.m k (□ (A ⊗ B)) C n
                        (□-▹ᵏ.at k (□ (A ⊗ B)) n (δ.at (A ⊗ B) k □A⊗B) , a)))
            ≡⟨ sym (▹ᵏ-F.fmap-∘ k) ⟩
                ▹ᵏ-F.fmap k (assoc-right ∘ m⁻¹ A B * id) n
                    (▹ᵏ-C.m k (□ (A ⊗ B)) C n (□-▹ᵏ.at k (□ (A ⊗ B)) n (δ.at (A ⊗ B) k □A⊗B) , a))
            ≡⟨⟩

                ▹ᵏ-F.fmap k (assoc-right ∘ m⁻¹ A B * id) n
                    (▹ᵏ-C.m k (□ (A ⊗ B)) C n (□-▹ᵏ.at k (□ (A ⊗ B)) n (δ.at (A ⊗ B) k □A⊗B) , a))
            ∎
        ) ⟩
            ◇-f (assoc-right ∘ m⁻¹ A B * id) n (st-◇ (A ⊗ B) C n (□A⊗B , (k , a)))
        ∎
        where
        lemma : ∀ k -> ▹ᵏ-C.m k (□ A) (□ B) ∘ □-▹ᵏ.at k (□ A) * □-▹ᵏ.at k (□ B)
                     ≈ □-▹ᵏ.at k (□ A ⊗ □ B) ∘ □-C.m (□ A) (□ B)
        lemma zero = refl
        lemma (suc k) {zero} {□□A , □□B} = refl
        lemma (suc k) {suc n} {□□A , □□B} = lemma k

    st-μ-◇ : ∀{A B : τ}
          -> μ.at (□ A ⊗ B) ∘ ◇-f (st-◇ A B) ∘ st-◇ A (◇ B)
           ≈ st-◇ A B ∘ (id * μ.at B)
    st-μ-◇ {A} {B} {n} {□A , (k , a)} with inspect (compareLeq k n)
    st-μ-◇ {A} {B} {.(k + l)} {□A , k , a} | snd==[ .k + l ] with≡ pf =
        begin
            μ.at (□ A ⊗ B) (k + l) (◇-f (st-◇ A B) (k + l) (st-◇ A (◇ B) (k + l) (□A , (k , a))))
        ≡⟨⟩
            μ-compare (□ A ⊗ B) (k + l) k
                (▹ᵏ-F.fmap k (st-◇ A B) (k + l)
                    (▹ᵏ-C.m k (□ A) (◇ B) (k + l)
                        (□-▹ᵏ.at k (□ A) (k + l) (δ.at A (k + l) □A) , a)))
                            (⌞ compareLeq k (k + l) ⌟)
        ≡⟨ cong! pf ⟩
            μ-compare (□ A ⊗ B) (k + l) k
                (▹ᵏ-F.fmap k (st-◇ A B) (k + l)
                    (▹ᵏ-C.m k (□ A) (◇ B) (k + l)
                        (□-▹ᵏ.at k (□ A) (k + l) (δ.at A (k + l) □A) , a)))
                            (snd==[ k + l ])
        ≡⟨⟩
            μ-shift k l
                (rew (delay-+-left0 k l)
                    (▹ᵏ-F.fmap k (st-◇ A B) (k + l)
                        (▹ᵏ-C.m k (□ A) (◇ B) (k + l)
                            ( □-▹ᵏ.at k (□ A) (k + l) (δ.at A (k + l) □A)
                            , a))))
        ≡⟨ cong (μ-shift k l) (fmap-delay-+-n+0 k l) ⟩
            μ-shift k l
                (st-◇ A B l
                    (rew (delay-+-left0 k l)
                        (▹ᵏ-C.m k (□ A) (◇ B) (k + l)
                            ( □-▹ᵏ.at k (□ A) (k + l) (δ.at A (k + l) □A)
                            , a))))
        ≡⟨ cong (λ x → μ-shift k l (st-◇ A B l x)) (m-delay-+-n+0 k l) ⟩
            μ-shift k l
                (st-◇ A B l
                    ( rew (delay-+-left0 k l) (□-▹ᵏ.at k (□ A) (k + l) (δ.at A (k + l) □A))
                    , rew (delay-+-left0 k l) a))
        ≡⟨ cong (λ x → μ-shift k l (st-◇ A B l (x , _))) (rew-□-left0 k l) ⟩
            μ-shift k l (st-◇ A B l (□A , rew (delay-+-left0 k l) a))
         ≡⟨ lemma k l (rew (delay-+-left0 k l) a) ⟩
            st-◇ A B (k + l) (□A , μ-shift k l (rew (delay-+-left0 k l) a))
        ≡⟨⟩
            st-◇ A B (k + l) (□A , μ-compare B (k + l) k a (⌞ snd==[ k + l ] ⌟))
        ≡⟨ cong! pf ⟩
            st-◇ A B (k + l) (□A , μ.at B (k + l) (k , a))
        ∎
        where
        rew-□-left0 : ∀ k l
             -> rew (delay-+-left0 k l) (□-▹ᵏ.at k (□ A) (k + l) (δ.at A (k + l) □A))
              ≡ □A
        rew-□-left0 zero l = refl
        rew-□-left0 (suc k) l = rew-□-left0 k l

        rew-□ : ∀ k l m
             -> rew (sym (delay-+ k m l)) (□-▹ᵏ.at m (□ A) l (δ.at A m □A))
              ≡ □-▹ᵏ.at (k + m) (□ A) (k + l) (δ.at A (k + m) □A)
        rew-□ zero l m = refl
        rew-□ (suc k) l m = rew-□ k l m

        lemma : ∀ k l a
             -> μ-shift k l (st-◇ A B l (□A , a))
              ≡ st-◇ A B (k + l) (□A , μ-shift k l a)
        lemma k l (m , a) =
            begin
                μ-shift k l (st-◇ A B l (□A , (m , a)))
            ≡⟨⟩
                k + m , rew (sym (delay-+ k m l)) (▹ᵏ-C.m m (□ A) B l (□-▹ᵏ.at m (□ A) l (δ.at A m □A) , a))
            ≡⟨ cong (λ x -> _ , x) (m-delay-+-sym k l m) ⟩
                k + m , ▹ᵏ-C.m (k + m) (□ A) B (k + l)
                            ( rew (sym (delay-+ k m l)) (□-▹ᵏ.at m (□ A) l (δ.at A m □A))
                            , rew (sym (delay-+ k m l)) a)
            ≡⟨ cong (λ x → _ , ▹ᵏ-C.m (k + m) (□ A) B (k + l) (x , _)) (rew-□ k l m) ⟩
                k + m , ▹ᵏ-C.m (k + m) (□ A) B (k + l)
                            ( □-▹ᵏ.at (k + m) (□ A) (k + l) (δ.at A (k + m) □A)
                            , rew (sym (delay-+ k m l)) a)
            ≡⟨⟩
                st-◇ A B (k + l) (□A , (k + m , rew (sym (delay-+ k m l)) a))
            ∎

    st-μ-◇ {A} {B} {.n} {□A , .(n + suc l) , a} | fst==suc[ n + l ] with≡ pf =
        begin
            μ.at (□ A ⊗ B) n (◇-f (st-◇ A B) n (st-◇ A (◇ B) n (□A , (n + suc l , a))))
        ≡⟨⟩
            μ-compare (□ A ⊗ B) n (n + suc l)
                (▹ᵏ-F.fmap (n + suc l) (st-◇ A B) n
                    (▹ᵏ-C.m (n + suc l) (□ A) (◇ B) n
                    (□-▹ᵏ.at (n + suc l) (□ A) n
                    (δ.at A (n + suc l) □A) , a)))
                    (⌞ compareLeq (n + suc l) n ⌟)
        ≡⟨ cong! pf ⟩
            μ-compare (□ A ⊗ B) n (n + suc l)
                (▹ᵏ-F.fmap (n + suc l) (st-◇ A B) n
                    (▹ᵏ-C.m (n + suc l) (□ A) (◇ B) n
                    (□-▹ᵏ.at (n + suc l) (□ A) n
                    (δ.at A (n + suc l) □A) , a)))
                    (fst==suc[ n + l ])
        ≡⟨⟩
            n + suc l , rew (delay-⊤ n l) top.tt
        ≡⟨ cong (λ x -> _ , x) (lemma n l) ⟩
            n + suc l , ▹ᵏ-C.m (n + suc l) (□ A) B n (□-▹ᵏ.at (n + suc l) (□ A) n (δ.at A (n + suc l) □A) , rew (delay-⊤ n l) top.tt)
        ≡⟨⟩
            st-◇ A B n (□A , μ-compare B n (n + suc l) a (⌞ fst==suc[ n + l ] ⌟))
        ≡⟨ cong! pf ⟩
            st-◇ A B n (□A , μ.at B n ((n + suc l) , a))
        ∎
        where
        lemma : ∀ n l
             -> rew (delay-⊤ n l) top.tt
              ≡ ▹ᵏ-C.m (n + suc l) (□ A) B n (□-▹ᵏ.at (n + suc l) (□ A) n (δ.at A (n + suc l) □A)
                                            , rew (delay-⊤ n l) top.tt)
        lemma zero l = refl
        lemma (suc n) l = lemma n l

open WStrongMonad ◇-□-Strong public

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
module Numeral.Natural.Relation.Order.Existence where

import      Lvl
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Proofs
import      Numeral.Natural.Relation.Order as [≤def]
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Relator.Ordering
open import Structure.Function
open import Structure.Function.Domain
open import Syntax.Function
open import Syntax.Transitivity

_≤_ : ℕ → ℕ → Stmt
_≤_ a b = ∃{Obj = ℕ}(n ↦ a + n ≡ b)

_<_ : ℕ → ℕ → Stmt
_<_ a b = (𝐒(a) ≤ b)

open From-[≤][<] (_≤_) (_<_) public

[≤]-with-[𝐒] : ∀{a b : ℕ} → (a ≤ b) → (𝐒(a) ≤ 𝐒(b))
[≤]-with-[𝐒] {a} {b} ([∃]-intro n ⦃ f ⦄) =
  [∃]-intro n ⦃
    𝐒(a) + n 🝖[ _≡_ ]-[ [+]-stepₗ {a} {n} ]
    𝐒(a + n) 🝖[ _≡_ ]-[ congruence₁(𝐒) f ]
    𝐒(b) 🝖-end
  ⦄

[≤]-equivalence : ∀{x y} → (x ≤ y) ↔ (x [≤def].≤ y)
[≤]-equivalence{x}{y} = [↔]-intro (l{x}{y}) (r{x}{y}) where
  l : ∀{x y} → (x ≤ y) ← (x [≤def].≤ y)
  l{𝟎}   {y}    ([≤def].min)      = [∃]-intro(y) ⦃ [≡]-intro ⦄
  l{𝐒(x)}{𝟎}    ()
  l{𝐒(x)}{𝐒(y)} ([≤def].succ proof) = [≤]-with-[𝐒] {x}{y} (l{x}{y} (proof))

  r : ∀{x y} → (x ≤ y) → (x [≤def].≤ y)
  r{𝟎}   {y}    ([∃]-intro(z) ⦃ 𝟎+z≡y   ⦄) = [≤def].min
  r{𝐒(x)}{𝟎}    ([∃]-intro(z) ⦃ ⦄)
  r{𝐒(x)}{𝐒(y)} ([∃]-intro(z) ⦃ 𝐒x+z≡𝐒y ⦄) = [≤def].succ (r{x}{y} ([∃]-intro(z) ⦃ injective(𝐒)(𝐒x+z≡𝐒y) ⦄))


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Greatest common divisor
------------------------------------------------------------------------

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

module Data.Nat.GCD where

open import Data.Nat.Base
open import Data.Nat.Divisibility
open import Data.Nat.DivMod
open import Data.Nat.GCD.Lemmas
open import Data.Nat.Properties
open import Data.Nat.Induction
  using (Acc; acc; <′-Rec; <′-recBuilder; <-wellFounded)
open import Data.Product
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
open import Function
open import Induction using (build)
open import Induction.Lexicographic using (_⊗_; [_⊗_])
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≢_; subst; cong)
open import Relation.Nullary using (Dec)
open import Relation.Nullary.Negation using (contradiction)
import Relation.Nullary.Decidable as Dec

------------------------------------------------------------------------
-- Definition

-- Calculated via Euclid's algorithm. In order to show progress,
-- avoiding the initial step where the first argument may increase, it
-- is necessary to first define a version `gcd′` which assumes that the
-- first argument is strictly smaller than the second. The full `gcd`
-- function then compares the two arguments and applies `gcd′`
-- accordingly.

gcd′ : ∀ m n → Acc _<_ m → n < m → ℕ
gcd′ m zero        _         _   = m
gcd′ m n@(suc n-1) (acc rec) n<m = gcd′ n (m % n) (rec _ n<m) (m%n<n m n-1)

gcd : ℕ → ℕ → ℕ
gcd m n with <-cmp m n
... | tri< m<n _ _ = gcd′ n m (<-wellFounded n) m<n
... | tri≈ _ _ _   = m
... | tri> _ _ n<m = gcd′ m n (<-wellFounded m) n<m

------------------------------------------------------------------------
-- Core properties of gcd′

gcd′[m,n]∣m,n : ∀ {m n} rec n<m → gcd′ m n rec n<m ∣ m × gcd′ m n rec n<m ∣ n
gcd′[m,n]∣m,n {m} {zero}  rec       n<m = ∣-refl , m ∣0
gcd′[m,n]∣m,n {m} {suc n} (acc rec) n<m
  with gcd′[m,n]∣m,n (rec _ n<m) (m%n<n m n)
... | gcd∣n , gcd∣m%n = ∣n∣m%n⇒∣m gcd∣n gcd∣m%n , gcd∣n

gcd′-greatest : ∀ {m n c} rec n<m → c ∣ m → c ∣ n → c ∣ gcd′ m n rec n<m
gcd′-greatest {m} {zero}  rec       n<m c∣m c∣n = c∣m
gcd′-greatest {m} {suc n} (acc rec) n<m c∣m c∣n =
  gcd′-greatest (rec _ n<m) (m%n<n m n) c∣n (%-presˡ-∣ c∣m c∣n)

------------------------------------------------------------------------
-- Core properties of gcd

gcd[m,n]∣m : ∀ m n → gcd m n ∣ m
gcd[m,n]∣m m n with <-cmp m n
... | tri< n<m _ _ = proj₂ (gcd′[m,n]∣m,n {n} {m} _ _)
... | tri≈ _ _ _   = ∣-refl
... | tri> _ _ m<n = proj₁ (gcd′[m,n]∣m,n {m} {n} _ _)

gcd[m,n]∣n : ∀ m n → gcd m n ∣ n
gcd[m,n]∣n m n with <-cmp m n
... | tri< n<m _    _ = proj₁ (gcd′[m,n]∣m,n {n} {m} _ _)
... | tri≈ _ P.refl _ = ∣-refl
... | tri> _ _    m<n = proj₂ (gcd′[m,n]∣m,n {m} {n} _ _)

gcd-greatest : ∀ {m n c} → c ∣ m → c ∣ n → c ∣ gcd m n
gcd-greatest {m} {n} c∣m c∣n with <-cmp m n
... | tri< n<m _ _ = gcd′-greatest _ _ c∣n c∣m
... | tri≈ _ _ _   = c∣m
... | tri> _ _ m<n = gcd′-greatest _ _ c∣m c∣n

------------------------------------------------------------------------
-- Other properties

-- Note that all other properties of `gcd` should be inferable from the
-- 3 core properties above.

gcd[0,0]≡0 : gcd 0 0 ≡ 0
gcd[0,0]≡0 = ∣-antisym (gcd 0 0 ∣0) (gcd-greatest (0 ∣0) (0 ∣0))

gcd[m,n]≢0 : ∀ m n → m ≢ 0 ⊎ n ≢ 0 → gcd m n ≢ 0
gcd[m,n]≢0 m n (inj₁ m≢0) eq = m≢0 (0∣⇒≡0 (subst (_∣ m) eq (gcd[m,n]∣m m n)))
gcd[m,n]≢0 m n (inj₂ n≢0) eq = n≢0 (0∣⇒≡0 (subst (_∣ n) eq (gcd[m,n]∣n m n)))

gcd[m,n]≡0⇒m≡0 : ∀ {m n} → gcd m n ≡ 0 → m ≡ 0
gcd[m,n]≡0⇒m≡0 {zero}  {n} eq = P.refl
gcd[m,n]≡0⇒m≡0 {suc m} {n} eq = contradiction eq (gcd[m,n]≢0 (suc m) n (inj₁ λ()))

gcd[m,n]≡0⇒n≡0 : ∀ m {n} → gcd m n ≡ 0 → n ≡ 0
gcd[m,n]≡0⇒n≡0 m {zero}  eq = P.refl
gcd[m,n]≡0⇒n≡0 m {suc n} eq = contradiction eq (gcd[m,n]≢0 m (suc n) (inj₂ λ()))

gcd-comm : ∀ m n → gcd m n ≡ gcd n m
gcd-comm m n = ∣-antisym
  (gcd-greatest (gcd[m,n]∣n m n) (gcd[m,n]∣m m n))
  (gcd-greatest (gcd[m,n]∣n n m) (gcd[m,n]∣m n m))

gcd-universality : ∀ {m n g} →
                   (∀ {d} → d ∣ m × d ∣ n → d ∣ g) →
                   (∀ {d} → d ∣ g → d ∣ m × d ∣ n) →
                   g ≡ gcd m n
gcd-universality {m} {n} forwards backwards with backwards ∣-refl
... | back₁ , back₂ = ∣-antisym
  (gcd-greatest back₁ back₂)
  (forwards (gcd[m,n]∣m m n , gcd[m,n]∣n m n))

-- This could be simplified with some nice backwards/forwards reasoning
-- after the new function hierarchy is up and running.
gcd[cm,cn]/c≡gcd[m,n] : ∀ c m n {≢0} → (gcd (c * m) (c * n) / c) {≢0} ≡ gcd m n
gcd[cm,cn]/c≡gcd[m,n] c@(suc c-1) m n = gcd-universality forwards backwards
  where
  forwards : ∀ {d : ℕ} → d ∣ m × d ∣ n → d ∣ gcd (c * m) (c * n) / c
  forwards {d} (d∣m , d∣n) = m*n∣o⇒n∣o/m c d (gcd-greatest (*-monoʳ-∣ c d∣m) (*-monoʳ-∣ c d∣n))

  backwards : ∀ {d : ℕ} → d ∣ gcd (c * m) (c * n) / c → d ∣ m × d ∣ n
  backwards {d} d∣gcd[cm,cn]/c with m∣n/o⇒o*m∣n (gcd-greatest (m∣m*n m) (m∣m*n n)) d∣gcd[cm,cn]/c
  ... | cd∣gcd[cm,n] =
    *-cancelˡ-∣ c-1 (∣-trans cd∣gcd[cm,n] (gcd[m,n]∣m (c * m) _)) ,
    *-cancelˡ-∣ c-1 (∣-trans cd∣gcd[cm,n] (gcd[m,n]∣n (c * m) _))

c*gcd[m,n]≡gcd[cm,cn] : ∀ c m n → c * gcd m n ≡ gcd (c * m) (c * n)
c*gcd[m,n]≡gcd[cm,cn] zero        m n = P.sym gcd[0,0]≡0
c*gcd[m,n]≡gcd[cm,cn] c@(suc c-1) m n = begin
  c * gcd m n                   ≡⟨ cong (c *_) (P.sym (gcd[cm,cn]/c≡gcd[m,n] c m n)) ⟩
  c * (gcd (c * m) (c * n) / c) ≡⟨ m*[n/m]≡n (gcd-greatest (m∣m*n m) (m∣m*n n)) ⟩
  gcd (c * m) (c * n)           ∎
  where open P.≡-Reasoning

gcd[m,n]≤n : ∀ m n → gcd m (suc n) ≤ suc n
gcd[m,n]≤n m n = ∣⇒≤ (gcd[m,n]∣n m (suc n))

n/gcd[m,n]≢0 : ∀ m n {n≢0 : Dec.False (n ≟ 0)} {gcd≢0} → (n / gcd m n) {gcd≢0} ≢ 0
n/gcd[m,n]≢0 m n@(suc n-1) {n≢0} {gcd≢0} = m<n⇒n≢0 (m≥n⇒m/n>0 {n} {gcd m n} {gcd≢0} (gcd[m,n]≤n m n-1))

------------------------------------------------------------------------
-- A formal specification of GCD

module GCD where

  -- Specification of the greatest common divisor (gcd) of two natural
  -- numbers.

  record GCD (m n gcd : ℕ) : Set where
    constructor is
    field
      -- The gcd is a common divisor.
      commonDivisor : gcd ∣ m × gcd ∣ n

      -- All common divisors divide the gcd, i.e. the gcd is the
      -- greatest common divisor according to the partial order _∣_.
      greatest : ∀ {d} → d ∣ m × d ∣ n → d ∣ gcd

  open GCD public

  -- The gcd is unique.

  unique : ∀ {d₁ d₂ m n} → GCD m n d₁ → GCD m n d₂ → d₁ ≡ d₂
  unique d₁ d₂ = ∣-antisym (GCD.greatest d₂ (GCD.commonDivisor d₁))
                           (GCD.greatest d₁ (GCD.commonDivisor d₂))

  -- The gcd relation is "symmetric".

  sym : ∀ {d m n} → GCD m n d → GCD n m d
  sym g = is (swap $ GCD.commonDivisor g) (GCD.greatest g ∘ swap)

  -- The gcd relation is "reflexive".

  refl : ∀ {n} → GCD n n n
  refl = is (∣-refl , ∣-refl) proj₁

  -- The GCD of 0 and n is n.

  base : ∀ {n} → GCD 0 n n
  base {n} = is (n ∣0 , ∣-refl) proj₂

  -- If d is the gcd of n and k, then it is also the gcd of n and
  -- n + k.

  step : ∀ {n k d} → GCD n k d → GCD n (n + k) d
  step g with GCD.commonDivisor g
  step {n} {k} {d} g | (d₁ , d₂) = is (d₁ , ∣m∣n⇒∣m+n d₁ d₂) greatest′
    where
    greatest′ : ∀ {d′} → d′ ∣ n × d′ ∣ n + k → d′ ∣ d
    greatest′ (d₁ , d₂) = GCD.greatest g (d₁ , ∣m+n∣m⇒∣n d₂ d₁)

open GCD public using (GCD) hiding (module GCD)

-- The function gcd fulfils the conditions required of GCD

gcd-GCD : ∀ m n → GCD m n (gcd m n)
gcd-GCD m n = record
  { commonDivisor = gcd[m,n]∣m m n , gcd[m,n]∣n m n
  ; greatest      = uncurry′ gcd-greatest
  }

-- Calculates the gcd of the arguments.

mkGCD : ∀ m n → ∃ λ d → GCD m n d
mkGCD m n = gcd m n , gcd-GCD m n

-- gcd as a proposition is decidable

gcd? : (m n d : ℕ) → Dec (GCD m n d)
gcd? m n d =
  Dec.map′ (λ { P.refl → gcd-GCD m n }) (GCD.unique (gcd-GCD m n))
           (gcd m n ≟ d)

GCD-* : ∀ {m n d c} → GCD (m * suc c) (n * suc c) (d * suc c) → GCD m n d
GCD-* (GCD.is (dc∣nc , dc∣mc) dc-greatest) =
  GCD.is (*-cancelʳ-∣ _ dc∣nc , *-cancelʳ-∣ _ dc∣mc)
  λ {_} → *-cancelʳ-∣ _ ∘ dc-greatest ∘ map (*-monoˡ-∣ _) (*-monoˡ-∣ _)

GCD-/ : ∀ {m n d c} {≢0} → c ∣ m → c ∣ n → c ∣ d →
        GCD m n d → GCD ((m / c) {≢0}) ((n / c) {≢0}) ((d / c) {≢0})
GCD-/ {m} {n} {d} {c@(suc c-1)}
  (divides p P.refl) (divides q P.refl) (divides r P.refl) gcd
  rewrite m*n/n≡m p c {_} | m*n/n≡m q c {_} | m*n/n≡m r c {_} = GCD-* gcd

GCD-/gcd : ∀ m n {≢0} → GCD ((m / gcd m n) {≢0}) ((n / gcd m n) {≢0}) 1
GCD-/gcd m n {≢0} rewrite P.sym (n/n≡1 (gcd m n) {≢0}) =
  GCD-/ {≢0 = ≢0} (gcd[m,n]∣m m n) (gcd[m,n]∣n m n) ∣-refl (gcd-GCD m n)

------------------------------------------------------------------------
-- Calculating the gcd

-- The calculation also proves Bézout's lemma.

module Bézout where

  module Identity where

    -- If m and n have greatest common divisor d, then one of the
    -- following two equations is satisfied, for some numbers x and y.
    -- The proof is "lemma" below (Bézout's lemma).
    --
    -- (If this identity was stated using integers instead of natural
    -- numbers, then it would not be necessary to have two equations.)

    data Identity (d m n : ℕ) : Set where
      +- : (x y : ℕ) (eq : d + y * n ≡ x * m) → Identity d m n
      -+ : (x y : ℕ) (eq : d + x * m ≡ y * n) → Identity d m n

    -- Various properties about Identity.

    sym : ∀ {d} → Symmetric (Identity d)
    sym (+- x y eq) = -+ y x eq
    sym (-+ x y eq) = +- y x eq

    refl : ∀ {d} → Identity d d d
    refl = -+ 0 1 P.refl

    base : ∀ {d} → Identity d 0 d
    base = -+ 0 1 P.refl

    private
      infixl 7 _⊕_

      _⊕_ : ℕ → ℕ → ℕ
      m ⊕ n = 1 + m + n

    step : ∀ {d n k} → Identity d n k → Identity d n (n + k)
    step {d} {n} (+-  x  y       eq) with compare x y
    ... | equal x     = +- (2 * x)     x       (lem₂ d x   eq)
    ... | less x i    = +- (2 * x ⊕ i) (x ⊕ i) (lem₃ d x   eq)
    ... | greater y i = +- (2 * y ⊕ i) y       (lem₄ d y n eq)
    step {d} {n} (-+  x  y       eq) with compare x y
    ... | equal x     = -+ (2 * x)     x       (lem₅ d x   eq)
    ... | less x i    = -+ (2 * x ⊕ i) (x ⊕ i) (lem₆ d x   eq)
    ... | greater y i = -+ (2 * y ⊕ i) y       (lem₇ d y n eq)

  open Identity public using (Identity; +-; -+) hiding (module Identity)

  module Lemma where

    -- This type packs up the gcd, the proof that it is a gcd, and the
    -- proof that it satisfies Bézout's identity.

    data Lemma (m n : ℕ) : Set where
      result : (d : ℕ) (g : GCD m n d) (b : Identity d m n) → Lemma m n

    -- Various properties about Lemma.

    sym : Symmetric Lemma
    sym (result d g b) = result d (GCD.sym g) (Identity.sym b)

    base : ∀ d → Lemma 0 d
    base d = result d GCD.base Identity.base

    refl : ∀ d → Lemma d d
    refl d = result d GCD.refl Identity.refl

    stepˡ : ∀ {n k} → Lemma n (suc k) → Lemma n (suc (n + k))
    stepˡ {n} {k} (result d g b) =
      subst (Lemma n) (+-suc n k) $
        result d (GCD.step g) (Identity.step b)

    stepʳ : ∀ {n k} → Lemma (suc k) n → Lemma (suc (n + k)) n
    stepʳ = sym ∘ stepˡ ∘ sym

  open Lemma public using (Lemma; result) hiding (module Lemma)

  -- Bézout's lemma proved using some variant of the extended
  -- Euclidean algorithm.

  lemma : (m n : ℕ) → Lemma m n
  lemma m n = build [ <′-recBuilder ⊗ <′-recBuilder ] P gcd″ (m , n)
    where
    P : ℕ × ℕ → Set
    P (m , n) = Lemma m n

    gcd″ : ∀ p → (<′-Rec ⊗ <′-Rec) P p → P p
    gcd″ (zero  , n                 ) rec = Lemma.base n
    gcd″ (suc m , zero              ) rec = Lemma.sym (Lemma.base (suc m))
    gcd″ (suc m , suc n             ) rec with compare m n
    ... | equal .m     = Lemma.refl (suc m)
    ... | less .m k    = Lemma.stepˡ $ proj₁ rec (suc k) (lem₁ k m)
                      -- "gcd (suc m) (suc k)"
    ... | greater .n k = Lemma.stepʳ $ proj₂ rec (suc k) (lem₁ k n) (suc n)
                      -- "gcd (suc k) (suc n)"

  -- Bézout's identity can be recovered from the GCD.

  identity : ∀ {m n d} → GCD m n d → Identity d m n
  identity {m} {n} g with lemma m n
  ... | result d g′ b with GCD.unique g g′
  ...   | P.refl = b