text:
------------------------------------------------------------------------
-- Typing of pure type systems (PTS)
------------------------------------------------------------------------

module Pts.Typing where

open import Data.Fin using (Fin; zero)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Fin.Substitution.Typed
open import Data.Nat using (ℕ; _+_)
open import Data.Product using (_,_; ∃; _×_; proj₂)
open import Data.Star using (ε; _◅_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Vec.All using (lookup₂)
open import Function using (flip)
open import Relation.Binary
import Relation.Binary.PropositionalEquality as PropEq

open import Pts.Core public
open import Pts.Syntax using (module SubstApp)
open import Pts.Reduction.Full

------------------------------------------------------------------------
-- Typing derivations.
--
-- The presentation of the typing rules below follows that of Pollak
-- (1994) rather than that of Barendregt (1992) in that it uses a
-- separate well-formedness judgment "Γ wf" for contexts in favor of
-- an explicit weakening rule.  The well-formedness judgment is used
-- to strengthen the variable and sort typing rules.  For the
-- remaining rules, well-formedness of contexts is an invariant (as e
-- witnessed by the "wt-wf" Lemma below).
--
-- References:
--
--  * H. P. Barendregt, Lambda Calculi with Types, chapter 2 of the
--    Handbook of Logic in Computer Science (vol. 2), Oxford
--    University Press, 1992.
--
--  * R. Pollack, The Theory of LEGO: A Proof Checker for the Extended
--    Calculus of Constructions, Ph.D. thesis, University of
--    Edinburgh, 1994

-- Definitions and lemmas are parametrized by a given PTS instance.
module Typing (pts : PTS) where
  open PTS pts
  open Ctx
  open Syntax
  open Substitution using (_[_])

  infixl 9 _·_
  infix  4 _wf _⊢_∈_

  mutual

    -- Well-formed contexts.
    _wf : ∀ {n} → Ctx n → Set
    Γ wf = WfCtx._wf _⊢_∈_ Γ

    -- Typing derivations.
    data _⊢_∈_ {n} (Γ : Ctx n) : Term n → Term n → Set where
      var    : ∀ x                         → Γ wf → Γ ⊢ var x   ∈ lookup x Γ
      axiom  : ∀ {s₁ s₂} (a : Axiom s₁ s₂) → Γ wf → Γ ⊢ sort s₁ ∈ sort s₂
      Π      : ∀ {s₁ s₂ s₃ a b} (r : Rule s₁ s₂ s₃)  →
               Γ ⊢ a ∈ sort s₁  → a ∷ Γ ⊢ b ∈ sort s₂ → Γ ⊢ Π a b ∈ sort s₃
      ƛ      : ∀ {a t b s}      →
               a ∷ Γ ⊢ t ∈ b    → Γ ⊢ Π a b ∈ sort s  → Γ ⊢ ƛ a t ∈ Π a b
      _·_    : ∀ {f a b t}      →
               Γ ⊢ f ∈ Π a b    → Γ ⊢ t ∈ a  → Γ ⊢ f · t ∈ b [ t ]
      conv   : ∀ {t a b s}      → Γ ⊢ t ∈ a  →
               Γ ⊢ b ∈ sort s   → a ≡β b     → Γ ⊢ t ∈ b

  open WfCtx _⊢_∈_ public hiding (_wf; _⊢_wf)

------------------------------------------------------------------------
-- Properties of typings

module _ {pts} where
  open PTS    pts
  open Syntax
  open Ctx
  open Typing pts

  -- Contexts of typings are well-formed.
  wt-wf : ∀ {n} {Γ : Ctx n} {t a} → Γ ⊢ t ∈ a → Γ wf
  wt-wf (var x Γ-wf)       = Γ-wf
  wt-wf (axiom a Γ-wf)     = Γ-wf
  wt-wf (Π r a∈s₁ b∈s₂)    = wt-wf a∈s₁
  wt-wf (ƛ t∈b Πab∈s)      = wt-wf Πab∈s
  wt-wf (f∈Πab · t∈a)      = wt-wf f∈Πab
  wt-wf (conv t∈a b∈s a≡b) = wt-wf t∈a

  -- Contexts of well-formed types are well-formed.
  wf-wf : ∀ {n} {Γ : Ctx n} {a} → (∃ λ s → Γ ⊢ a ∈ sort s) → Γ wf
  wf-wf (_ , a∈s) = wt-wf a∈s

  private
    module Sβ {n} where
      open Setoid (≡β-setoid {Sort} {n}) public using (refl; trans; sym)

  -- A generation lemma for sorts.
  sort-gen : ∀ {n} {Γ : Ctx n} {s a} → Γ ⊢ sort s ∈ a →
             ∃ λ s′ →  Axiom s s′ × a ≡β sort s′
  sort-gen (axiom ax Γ-wf)      = _ , ax , Sβ.refl
  sort-gen (conv s∈a b∈s₁ a≡b) =
    let s₂ , ax , a≡s₂ = sort-gen s∈a
    in s₂ , ax , Sβ.trans (Sβ.sym a≡b) a≡s₂

  -- A generation lemma for product typings.
  Π-gen : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢ Π a b ∈ c →
          ∃ λ s₁ → ∃ λ s₂ → ∃ λ s₃ → Rule s₁ s₂ s₃ ×
            Γ ⊢ a ∈ sort s₁ × a ∷ Γ ⊢ b ∈ sort s₂ × c ≡β sort s₃
  Π-gen (Π r a∈s₁ b∈s₂)          = _ , _ , _ , r , a∈s₁ , b∈s₂ , Sβ.refl
  Π-gen (conv Πab∈c₁ c₂∈s c₁≡c₂) =
    let s₁ , s₂ , s₃ , r , a∈s₁ , b∈s₂ , c₁≡s₃ = Π-gen Πab∈c₁
    in s₁ , s₂ , s₃ , r , a∈s₁ , b∈s₂ , Sβ.trans (Sβ.sym c₁≡c₂) c₁≡s₃

  -- A generation lemma for abstractions.
  ƛ-gen : ∀ {n} {Γ : Ctx n} {a t c} → Γ ⊢ ƛ a t ∈ c →
          ∃ λ s → ∃ λ b → Γ ⊢ Π a b ∈ sort s × a ∷ Γ ⊢ t ∈ b × c ≡β Π a b
  ƛ-gen (ƛ t∈b Πab∈s)            = _ , _ , Πab∈s , t∈b , Sβ.refl
  ƛ-gen (conv λat∈c₁ c₂∈s c₁≡c₂) =
    let s , b , Πab∈s , t∈b , c₁≡Πab = ƛ-gen λat∈c₁
    in s , b , Πab∈s , t∈b , Sβ.trans (Sβ.sym c₁≡c₂) c₁≡Πab

  ----------------------------------------------------------------------
  -- Well-typed substitutions (i.e. substitution lemmas)

  -- A shorthand for typings of Ts.
  TermTyping : (ℕ → Set) → Set₁
  TermTyping T = Typing Term T Term

  -- Term-typed substitutions.
  module TermTypedSub {T} (l : Lift T Term) (_⊢T_∈_ : TermTyping T) where
    typedSub : TypedSub Term Term T
    typedSub = record
      { _⊢_∈_       = _⊢T_∈_
      ; _⊢_wf       = WfCtx._⊢_wf _⊢_∈_
      ; application = record { _/_    = SubstApp._/_ Sort l }
      ; weakenOps   = record { weaken = Substitution.weaken }
      }

    open TypedSub typedSub public hiding (_⊢_∈_)

  -- Typed liftings from Ts to Terms.
  LiftToTermTyped : ∀ {T} → Lift T Term → TermTyping T → Set
  LiftToTermTyped l _⊢T_∈_ = LiftTyped l typedSub _⊢_∈_
    where open TermTypedSub l _⊢T_∈_ using (typedSub)

  -- Application of well-typed substitutions to terms.
  record TypedSubstApp {T} l {_⊢T_∈_ : TermTyping T}
                       (lt : LiftToTermTyped l _⊢T_∈_) : Set where
    open LiftTyped lt
    open Substitution using (_[_])
    open PropEq hiding ([_])
    private
      module A = SubstApp Sort l
      module L = Lift l

    -- Substitutions commute.
    field /-sub-↑ : ∀ {m n} a b (σ : Sub T m n) →
                    a [ b ] A./ σ ≡ (a A./ σ L.↑) [ b A./ σ ]

    open BetaSubstApp (record { /-sub-↑ = /-sub-↑ }) hiding (/-sub-↑)
    open TermTypedSub l _⊢T_∈_ hiding (_/_)

    infixl 8 _/_

    -- Substitutions preserve well-typedness of terms.
    _/_ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {t a σ} →
          Γ ⊢ t ∈ a → Γ ⇒ Δ ⊢ σ → Δ ⊢ t A./ σ ∈ a A./ σ
    var x Γ-wf            / (σ-wt , _) = lift (lookup₂ x σ-wt)
    axiom a Γ-wf          / (_ , Δ-wf) = axiom a Δ-wf
    Π r a∈s₁ b∈s₂         / σ-wt =
      Π r (a∈s₁ / σ-wt) (b∈s₂ / σ-wt ↑ (_ , a∈s₁ / σ-wt))
    ƛ t∈b Πab∈s           / σ-wt =
      let _ , _ , _ , _ , a/σ∈s , _ = Π-gen (Πab∈s / σ-wt) in
      ƛ (t∈b / σ-wt ↑ (_ , a/σ∈s)) (Πab∈s / σ-wt)
    _·_ {b = b} f∈Πab t∈a / σ-wt =
      subst (_⊢_∈_ _ _) (sym (/-sub-↑ b _ _)) ((f∈Πab / σ-wt) · (t∈a / σ-wt))
    conv t∈a b∈s a≡b      / σ-wt = conv (t∈a / σ-wt) (b∈s / σ-wt) (a≡b /≡β _)

  -- Typed variable substitutions (renamings).
  module TypedRenaming where
    open Substitution
      using (termSubst; varLiftAppLemmas; varLiftSubLemmas)
    open TermSubst     termSubst        using  (varLift)
    open LiftAppLemmas varLiftAppLemmas hiding (lift)

    typedVarSubst : TypedVarSubst (WfCtx._⊢_wf _⊢_∈_)
    typedVarSubst = record
      { application = AppLemmas.application appLemmas
      ; weakenOps   = Ctx.weakenOps
      ; id-vanishes = id-vanishes
      ; /-⊙         = /-⊙
      ; /-wk        = PropEq.refl
      ; wf-wf       = wf-wf
      }
    open TypedVarSubst typedVarSubst public

    -- Liftings from variables to typed terms.
    liftTyped : LiftTyped varLift typedSub _⊢_∈_
    liftTyped = record
      { simpleTyped  = simpleTyped
      ; lift         = lift
      }
      where
        lift : ∀ {n} {Γ : Ctx n} {x a} → Γ ⊢Var x ∈ a → Γ ⊢ var x ∈ a
        lift (var x Γ-wf) = var x Γ-wf

    open LiftSubLemmas varLiftSubLemmas

    typedSubstApp : TypedSubstApp varLift liftTyped
    typedSubstApp = record { /-sub-↑ = /-sub-↑ }

  -- Typed term substitutions in terms.
  module TypedSubstitution where
    open Substitution using (simple; termSubst)
    open SimpleExt simple using (extension)
    open TermSubst termSubst using (termLift)
    open TermTypedSub termLift _⊢_∈_ public using (typedSub; _⇒_⊢_)
    open TypedRenaming using (_⇒_⊢Var_)
    private
      module U = Substitution
      module V = TypedRenaming
      module L = ExtAppLemmas U.appLemmas

    infixl 8 _/Var_ _/_

    -- Renaming preserves well-typedness.
    _/Var_ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a b σ} →
             Γ ⊢ a ∈ b → Γ ⇒ Δ ⊢Var σ → Δ ⊢ a U./Var σ ∈ b U./Var σ
    _/Var_ = TypedSubstApp._/_ V.typedSubstApp

    -- Weakening preserves well-typedness.
    weaken : ∀ {n} {Γ : Ctx n} {a b c s} → Γ ⊢ a ∈ b → Γ ⊢ c ∈ sort s →
             (c ∷ Γ) ⊢ (U.weaken a) ∈ (U.weaken b)
    weaken a∈b c∈s = a∈b /Var V.wk (_ , c∈s)

    -- Extensions of typed term substitutions.
    extensionTyped : ExtensionTyped extension typedSub
    extensionTyped = record
      { weaken   = λ { (_ , c∈s) a∈b → weaken a∈b c∈s }
      ; weaken-/ = ExtLemmas₄.weaken-/ L.lemmas₄
      ; wt-wf    = wt-wf
      }

    -- Simple typed term substitutions.
    simpleTyped : SimpleTyped simple typedSub
    simpleTyped = record
      { extensionTyped  = extensionTyped
      ; var             = var
      ; id-vanishes     = L.id-vanishes
      ; /-wk            = λ {_ a} → L./-wk {t = a}
      ; wk-sub-vanishes = L.wk-sub-vanishes
      ; wf-wf           = wf-wf
      }

    -- Liftings from terms to terms.
    liftTyped : LiftTyped termLift typedSub _⊢_∈_
    liftTyped = record
      { simpleTyped  = simpleTyped
      ; lift         = Function.id
      }

    open LiftTyped liftTyped public
      hiding (var; weaken; extensionTyped; simpleTyped; wt-wf; wf-wf)

    typedSubstApp : TypedSubstApp termLift liftTyped
    typedSubstApp = record { /-sub-↑ = λ a _ _ → L.sub-commutes a }

    -- Substitutions preserve well-typedness.
    _/_ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a b σ} →
          Γ ⊢ a ∈ b → Γ ⇒ Δ ⊢ σ → Δ ⊢ a U./ σ ∈ b U./ σ
    _/_ = TypedSubstApp._/_ typedSubstApp

    infix 10 _[_]

    -- Single-variable substitutions preserve well-typedness.
    _[_] : ∀ {n} {Γ : Ctx n} {t a u b} →
           b ∷ Γ ⊢ t ∈ a → Γ ⊢ u ∈ b → Γ ⊢ t U.[ u ] ∈ a U.[ u ]
    t∈a [ u∈b ] = t∈a / sub u∈b

    -- Conversion of the first type in a context preserves
    -- well-typedness.
    conv-⊢ : ∀ {n} {Γ : Ctx n} {a₁ a₂ t b s} →
             a₁ ∷ Γ ⊢ t ∈ b → Γ ⊢ a₂ ∈ sort s → a₁ ≡β a₂ → a₂ ∷ Γ ⊢ t ∈ b
    conv-⊢ t∈b a₂∈s a₁≡a₂ =
      subst₂ (_⊢_∈_ _) (L.id-vanishes _) (L.id-vanishes _) (t∈b / csub)
      where
        open PropEq using (subst₂)
        open BetaSubstitution using (weaken-≡β)
        open Setoid ≡β-setoid using (sym)

        a₁∷Γ-wf = wt-wf t∈b
        a₁∈s′   = proj₂ (wf-∷₁ a₁∷Γ-wf)
        a₂∷Γ-wf = (_ , a₂∈s) ∷ (wf-∷₂ a₁∷Γ-wf)

        csub = tsub (conv (var zero a₂∷Γ-wf) (weaken a₁∈s′ a₂∈s)
                          (weaken-≡β (sym a₁≡a₂)))

  open TypedSubstitution

  -- Operations on well-formed contexts that require weakening of
  -- well-formedness judgments.
  module WfCtxOps where
    private module E = ExtensionTyped extensionTyped

    wfWeakenOps : WfWeakenOps weakenOps
    wfWeakenOps = record
      { weaken = λ { a-wk (_ , b∈s) → (_ , E.weaken a-wk b∈s) }
      }

    open WfWeakenOps wfWeakenOps public

  ----------------------------------------------------------------------
  -- Preservation of types under reduction (aka subject reduction)

  open Sβ
  open PropEq using (_≡_)

  -- Every well-typed term is either a type or an element.
  tp-or-el : ∀ {n} {Γ : Ctx n} {a b} → Γ ⊢ a ∈ b →
             ∃ λ s → b ≡ sort s ⊎ Γ ⊢ b ∈ sort s
  tp-or-el (var x Γ-wf)    = _ , inj₂ (proj₂ (WfCtxOps.lookup x Γ-wf))
  tp-or-el (axiom a Γ-wf)  = _ , inj₁ PropEq.refl
  tp-or-el (Π r a∈s₁ b∈s₂) = _ , inj₁ PropEq.refl
  tp-or-el (ƛ t∈b Πab∈s)   = _ , inj₂ Πab∈s
  tp-or-el (f∈Πab · t∈a)   with tp-or-el f∈Πab
  tp-or-el (f∈Πab · t∈a)   | _ , inj₁ ()
  tp-or-el (f∈Πab · t∈a)   | _ , inj₂ Πab∈s =
    let _ , s , _ , _ , _ , b∈s , _ = Π-gen Πab∈s
    in s , inj₂ (b∈s [ t∈a ])
  tp-or-el (conv t∈a b∈s a≡b) = _ , inj₂ b∈s

  -- An inversion lemma for product typings.
  Π-inv : ∀ {n} {Γ : Ctx n} {f a b} → Γ ⊢ f ∈ Π a b →
           ∃ λ s₁ → ∃ λ s₂ → Γ ⊢ a ∈ sort s₁ × a ∷ Γ ⊢ b ∈ sort s₂
  Π-inv f∈Πab with tp-or-el f∈Πab
  Π-inv f∈Πab | _ , inj₁ ()
  Π-inv f∈Πab | _ , inj₂ Πab∈s =
    let s₁ , s₂ , _ , _ , a∈s₁ , b∈s₂ , _ = Π-gen Πab∈s
    in s₁ , s₂ , a∈s₁ , b∈s₂

  -- An inversion lemma for abstractions.
  ƛ-inv : ∀ {n} {Γ : Ctx n} {a t b c} → Γ ⊢ ƛ a t ∈ Π b c →
           ∃ λ s → Γ ⊢ a ∈ sort s × b ≡β a × a ∷ Γ ⊢ t ∈ c
  ƛ-inv λat∈Πbc =
    let _ , _ , Πad∈s , t∈d , Πbc≡Πad = ƛ-gen λat∈Πbc
        s₁ , _ , _ , _ , a∈s₁ , _     = Π-gen Πad∈s
        _ , _ , _ , c∈s₂              = Π-inv λat∈Πbc
        b≡a , c≡d                     = Π-inj Πbc≡Πad
    in s₁ , a∈s₁ , b≡a , conv t∈d (conv-⊢ c∈s₂ a∈s₁ b≡a) (sym c≡d)

  -- Preservation of types under one-step reduction.
  pres : ∀ {n} {Γ : Ctx n} {a a′ b} → Γ ⊢ a ∈ b → a →β a′ → Γ ⊢ a′ ∈ b
  pres (var _ _)   ()
  pres (axiom _ _) ()
  pres (Π r a∈s₁ b∈s₂) (Π₁ a→a′ b) =
    Π r a′∈s₂ (conv-⊢ b∈s₂ a′∈s₂ (→β⇒≡β a→a′))
    where a′∈s₂ = pres a∈s₁ a→a′
  pres (Π r a∈s₁ b∈s₂) (Π₂ a b→b′) = Π r a∈s₁ (pres b∈s₂ b→b′)
  pres (ƛ t∈b Πab∈s) (ƛ₁ a→a′ t)   =
    let _ , _ , _ , _ , a′∈s , _ = Π-gen (pres Πab∈s (Π₁ a→a′ _))
        Πab→Πa′b                 = Π₁ a→a′ _
    in conv (ƛ (conv-⊢ t∈b a′∈s (→β⇒≡β a→a′)) (pres Πab∈s Πab→Πa′b))
            Πab∈s (sym (→β⇒≡β Πab→Πa′b))
  pres (ƛ t∈b Πab∈s) (ƛ₂ a t→t′)    = ƛ (pres t∈b t→t′) Πab∈s
  pres (λat∈Πbc · u∈b) (cont a t u) =
    let _ , a∈s , b≡a , t∈c = ƛ-inv λat∈Πbc
    in t∈c [ conv u∈b a∈s b≡a ]
  pres (f∈Πab · t∈a) (f→f′ ·₁ t) = pres f∈Πab f→f′ · t∈a
  pres (_·_ {b = b} f∈Πab t∈a) (f ·₂ t→t′) =
    let _ , _ , _ , b∈s = Π-inv f∈Πab
    in conv (f∈Πab · pres t∈a t→t′) (b∈s [ t∈a ])
            (sym (→β*⇒≡β (b [→β t→t′ ])))
  pres (conv a∈b₁ b₂∈s b₁≡b₂) a→a′ = conv (pres a∈b₁ a→a′) b₂∈s b₁≡b₂

  -- Preservation of types under reduction (aka subject reduction).
  pres* : ∀ {n} {Γ : Ctx n} {a a′ b} → Γ ⊢ a ∈ b → a →β* a′ → Γ ⊢ a′ ∈ b
  pres* a∈b  ε                = a∈b
  pres* a₁∈b (a₁→a₂ ◅ a₂→*a₃) = pres* (pres a₁∈b a₁→a₂) a₂→*a₃

max_stars_repo_name: asr/pts-agda

max_issues_repo_name: asr/pts-agda

max_forks_repo_name: asr/pts-agda


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

open import Categories.Category

module Categories.Category.Complete.Finitely {o ℓ e} (C : Category o ℓ e) where

open import Level

open import Categories.Category.Cartesian C
open import Categories.Diagram.Equalizer C
open import Categories.Diagram.Pullback C

open Category C

record FinitelyComplete : Set (levelOfTerm C) where
  field
    cartesian : Cartesian
    equalizer : ∀ {A B} (f g : A ⇒ B) → Equalizer f g

  module cartesian = Cartesian cartesian
  module equalizer {A B} (f g : A ⇒ B) = Equalizer (equalizer f g)
  open cartesian public

  pullback : ∀ {X Y Z} (f : X ⇒ Z) (g : Y ⇒ Z) → Pullback f g
  pullback f g = Product×Equalizer⇒Pullback product (equalizer _ _)

  module pullback {X Y Z} (f : X ⇒ Z) (g : Y ⇒ Z) = Pullback (pullback f g)

ext: agda

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Functor where

open import Level
open import Data.Product using (_×_; Σ)
open import Function.Surjection using (Surjective)
open import Function.Equality using (_⟶_)
open import Relation.Nullary

open import Categories.Category
open import Categories.Functor.Core public
import Categories.Morphism as Morphism

private
  variable
    o ℓ e o′ ℓ′ e′ : Level
    C D : Category o ℓ e

Contravariant : ∀ (C : Category o ℓ e) (D : Category o′ ℓ′ e′) → Set _
Contravariant C D = Functor (Category.op C) D

Faithful : Functor C D → Set _
Faithful {C = C} {D = D} F = ∀ {X Y} → (f g : C [ X , Y ]) → D [ F₁ f ≈ F₁ g ] → C [ f ≈ g ]
  where open Functor F

Full : Functor C D → Set _
Full {C = C} {D = D} F = ∀ {X Y} → Surjective {To = D.hom-setoid {F₀ X} {F₀ Y}} G
  where
    module C = Category C
    module D = Category D
    open Functor F
    G : ∀ {X Y} → (C.hom-setoid {X} {Y}) ⟶ D.hom-setoid {F₀ X} {F₀ Y}
    G = record { _⟨$⟩_ = F₁ ; cong = F-resp-≈ }

FullyFaithful : Functor C D → Set _
FullyFaithful F = Full F × Faithful F

-- Note that this is a constructive version of Essentially Surjective, which is
-- quite a strong assumption.
EssentiallySurjective : Functor C D → Set _
EssentiallySurjective {C = C} {D = D} F = (d : Obj) → Σ C.Obj (λ c → Functor.F₀ F c ≅ d)
  where
  open Morphism D
  open Category D
  module C = Category C

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


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

open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong)
open import Relation.Nullary using (Dec; yes; no)

import Data.Product as Product
import Data.Sum as Sum
import Data.Nat as ℕ
import Data.Nat.Properties as ℕₚ

open Product using (∃-syntax; _,_)
open Sum using (inj₁)
open ℕ using (ℕ; _+_; zero; suc)

open import PiCalculus.LinearTypeSystem.Algebras
module PiCalculus.LinearTypeSystem.Algebras.Graded where

_≔_∙_ : ℕ → ℕ → ℕ → Set
x ≔ y ∙ z = x ≡ (y + z)

computeʳ : (x y : ℕ) → Dec (∃[ z ] (x ≔ y ∙ z))
computeʳ x y with y ℕₚ.≤″? x
computeʳ x y | yes (ℕ.less-than-or-equal proof) = yes (_ , (sym proof))
computeʳ x y | no ¬p = no λ where
  (_ , p) → ¬p (ℕ.less-than-or-equal (sym p))

Graded : Algebra ℕ
Algebra.0∙ Graded = 0
Algebra.1∙ Graded = 1
Algebra._≔_∙_ Graded = _≔_∙_
Algebra.∙-computeʳ Graded = computeʳ
Algebra.∙-unique Graded refl refl = refl
Algebra.∙-uniqueˡ Graded refl = ℕₚ.+-cancelʳ-≡ _ _
Algebra.0∙-minˡ Graded {zero} {zero} refl = refl
Algebra.∙-idˡ Graded = refl
Algebra.∙-comm Graded {y = y} refl = ℕₚ.+-comm y _
Algebra.∙-assoc Graded {z = z} {v = v} refl refl = v + z , (ℕₚ.+-assoc _ v z , refl)

max_stars_repo_name: guilhermehas/typing-linear-pi

max_issues_repo_name: guilhermehas/typing-linear-pi

max_forks_repo_name: guilhermehas/typing-linear-pi


text:
{-

          Types Summer School 2007

                 Bertinoro
             Aug 19 - 31, 2007

                   Agda

                Ulf Norell

-}

module Parity where

open import Nat

-- Parity n tells us whether n is even or odd.

data Parity : Nat -> Set where
  even : (k : Nat) -> Parity (2 * k)
  odd  : (k : Nat) -> Parity (2 * k + 1)

-- Every number is either even or odd.

parity : (n : Nat) -> Parity n
parity  zero = even zero
parity (suc n)         with parity n
parity (suc .(2 * k))     | even k = {! !}
parity (suc .(2 * k + 1)) | odd  k = {! !}

half : Nat -> Nat
half n         with parity n
half .(2 * k)     | even k = k
half .(2 * k + 1) | odd  k = k

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --without-K #-}
module Util.HoTT.HLevel where

open import Util.HoTT.HLevel.Core public

open import Util.HoTT.Equiv
open import Util.HoTT.FunctionalExtensionality
open import Util.HoTT.Homotopy
open import Util.HoTT.Univalence.Axiom
open import Util.Prelude
open import Util.Relation.Binary.PropositionalEquality using
  ( Σ-≡⁺ ; Σ-≡⁻ ; Σ-≡⁺∘Σ-≡⁻ )
open import Util.Relation.Binary.LogicalEquivalence

private
  variable
    α β γ : Level
    A B C : Set α

infixr 0 _→-HProp_

-- Note that A and B must be at the same level. A more direct proof could
-- probably avoid this.
≃-pres-IsOfHLevel : ∀ {A B : Set α} n → A ≃ B → IsOfHLevel n A → IsOfHLevel n B
≃-pres-IsOfHLevel n A≃B = subst (IsOfHLevel n) (≃→≡ A≃B)

≅-pres-IsOfHLevel : ∀ {A B : Set α} n → A ≅ B → IsOfHLevel n A → IsOfHLevel n B
≅-pres-IsOfHLevel n A≅B = ≃-pres-IsOfHLevel n (≅→≃ A≅B)

∀-IsProp : {B : A → Set β} → (∀ a → IsProp (B a)) → IsProp (∀ a → B a)
∀-IsProp B-prop f g = funext λ a → B-prop _ _ _

∀∙-IsProp : {B : A → Set β} → (∀ a → IsProp (B a)) → IsProp (∀ {a} → B a)
∀∙-IsProp B-prop f g = funext∙ (B-prop _ _ _)

→-IsProp : IsProp B → IsProp (A → B)
→-IsProp B-prop = ∀-IsProp λ _ → B-prop

∀-HProp : (A : Set α) → ((a : A) → HProp β) → HProp (α ⊔ℓ β)
∀-HProp A B = HLevel⁺ (∀ a → B a .type) (∀-IsProp (λ a → B a .level))

∀∙-HProp : {A : Set α} → ((a : A) → HProp β) → HProp (α ⊔ℓ β)
∀∙-HProp B = HLevel⁺ (∀ {a} → B a .type) (∀∙-IsProp (λ a → B a .level))

_→-HProp_ : Set α → HProp β → HProp (α ⊔ℓ β)
A →-HProp B = HLevel⁺ (A → B .type) (→-IsProp (B .level))

_→-HProp′_ : HProp α → HProp β → HProp (α ⊔ℓ β)
A →-HProp′ B = A .type →-HProp B

IsContr-IsProp : IsProp (IsContr A)
IsContr-IsProp (x , x-unique) (y , y-unique)
  = Σ-≡⁺ (x-unique y , eq-prop _ _)
  where
  eq-prop : IsProp (∀ y′ → y ≡ y′)
  eq-prop = ∀-IsProp λ γ′ → IsOfHLevel-suc 1 (IsOfHLevel-suc 0 (x , x-unique))

IsProp-IsProp : IsProp (IsProp A)
IsProp-IsProp A-prop A-prop′
  = ∀-IsProp (λ x → ∀-IsProp λ y → IsOfHLevel-suc 1 A-prop) A-prop A-prop′

IsOfHLevel-IsProp : ∀ n → IsProp (IsOfHLevel n A)
IsOfHLevel-IsProp {A = A} zero = IsContr-IsProp
IsOfHLevel-IsProp (suc zero) = IsProp-IsProp
IsOfHLevel-IsProp (suc (suc n))
  = ∀∙-IsProp λ x → ∀∙-IsProp λ y → IsOfHLevel-IsProp (suc n)

IsSet-IsProp : IsProp (IsSet A)
IsSet-IsProp = IsOfHLevel-IsProp 2

∀-IsSet : {A : Set α} {B : A → Set β}
  → (∀ a → IsSet (B a))
  → IsSet (∀ a → B a)
∀-IsSet B-set {f} {g} p q = let open ≡-Reasoning in
  begin
    p
  ≡˘⟨ funext∘≡→~ p ⟩
    funext (≡→~ p)
  ≡⟨ cong funext (funext λ a → B-set a (≡→~ p a) (≡→~ q a)) ⟩
    funext (≡→~ q)
  ≡⟨ funext∘≡→~ q ⟩
    q
  ∎

∀∙-IsSet : {A : Set α} {B : A → Set β}
  → (∀ a → IsSet (B a))
  → IsSet (∀ {a} → B a)
∀∙-IsSet {A = A} {B = B} B-set = ≅-pres-IsOfHLevel 2 iso (∀-IsSet B-set)
  where
    iso : (∀ a → B a) ≅ (∀ {a} → B a)
    iso = record
      { forth = λ f {a} → f a
      ; isIso = record
        { back = λ f a → f {a}
        ; back∘forth = λ _ → refl
        ; forth∘back = λ _ → refl
        }
      }

→-IsSet : IsSet B → IsSet (A → B)
→-IsSet B-set = ∀-IsSet (λ _ → B-set)

∀-HSet : (A : Set α) → (A → HSet β) → HSet (α ⊔ℓ β)
∀-HSet A B = HLevel⁺ (∀ a → B a .type) (∀-IsSet (λ a → B a .level))

∀∙-HSet : {A : Set α} → (A → HSet β) → HSet (α ⊔ℓ β)
∀∙-HSet B = HLevel⁺ (∀ {a} → B a .type) (∀∙-IsSet (λ a → B a .level))

HLevel-≡⁺ : ∀ {n} (A B : HLevel α n)
  → A .type ≡ B .type
  → A ≡ B
HLevel-≡⁺ (HLevel⁺ A A-level) (HLevel⁺ B B-level) refl
  = cong (HLevel⁺ A) (IsOfHLevel-IsProp _ _ _)

IsContr-≅⁺ : IsContr A → IsContr B → A ≅ B
IsContr-≅⁺ (a , a-uniq) (b , b-uniq) = record
  { forth = λ _ → b
  ; isIso = record
    { back = λ _ → a
    ; back∘forth = λ _ → a-uniq _
    ; forth∘back = λ _ → b-uniq _
    }
  }

HContr-≡⁺ : (A B : HContr α) → A ≡ B
HContr-≡⁺ A B = HLevel-≡⁺ A B (≅→≡ (IsContr-≅⁺ (A .level) (B .level)))

IsProp-≅⁺ : IsProp A → IsProp B → A ↔ B → A ≅ B
IsProp-≅⁺ A-prop B-prop A↔B = record
  { forth = A↔B .forth
  ; isIso = record
    { back = A↔B .back
    ; back∘forth = λ _ → A-prop _ _
    ; forth∘back = λ _ → B-prop _ _
    }
  }

HProp-≡⁺ : (A B : HProp α) → A .type ↔ B .type → A ≡ B
HProp-≡⁺ A B A↔B = HLevel-≡⁺ A B (≅→≡ (IsProp-≅⁺ (A .level) (B .level) A↔B))

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


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

module Experiment.FingerTree where
open import Level renaming (zero to lzero ; suc to lsuc)
open import Algebra

open import Experiment.FingerTree.Common

data Digit {a} (A : Set a) : Set a where
  one   : (a       : A) → Digit A
  two   : (a b     : A) → Digit A
  three : (a b c   : A) → Digit A
  four  : (a b c d : A) → Digit A

data Node {v a} (V : Set v) (A : Set a) : Set (a ⊔ v) where
  :node2 : (v : V) → (a b   : A) → Node V A
  :node3 : (v : V) → (a b c : A) → Node V A

nodeToDigit : ∀ {v a} {V : Set v} {A : Set a} → Node V A → Digit A
nodeToDigit (:node2 v a b  ) = two a b
nodeToDigit (:node3 v a b c) = three a b c

data FingerTree {v a} (V : Set v) (A : Set a) : Set (a ⊔ v) where
  :empty  : FingerTree V A
  :single : A → FingerTree V A
  :deep   : V → Digit A → FingerTree V (Node V A) → Digit A → FingerTree V A

Digit-foldr : ∀ {a b} {A : Set a} {B : Set b} → (A → B → B) → B → Digit A → B
Digit-foldr _<>_ e (one   a)       = a <> e
Digit-foldr _<>_ e (two   a b)     = a <> (b <> e)
Digit-foldr _<>_ e (three a b c)   = a <> (b <> (c <> e))
Digit-foldr _<>_ e (four  a b c d) = a <> (b <> (c <> (d <> e)))

Node-foldr : ∀ {v a b} {V : Set v} {A : Set a} {B : Set b} →
  (A → B → B) → B → Node V A → B
Node-foldr _<>_ e (:node2 v a b  ) = a <> (b <> e)
Node-foldr _<>_ e (:node3 v a b c) = a <> (b <> (c <> e))

Node-measure : ∀ {v a} {V : Set v} {A : Set a} → Node V A → V
Node-measure (:node2 v a b  ) = v
Node-measure (:node3 v a b c) = v

record IsMeasured {c e a} (M : Monoid c e) (A : Set a) : Set (a ⊔ c ⊔ e) where
  open Monoid M
  field
    measure : A → Carrier

module Constructor {c e a} {A : Set a} {M : Monoid c e} (MS : IsMeasured M A) where
  open Monoid M renaming (Carrier to V)
  open IsMeasured MS

  empty : FingerTree V A
  empty = :empty

  single : A → FingerTree V A
  single = :single

  deep : Digit A → FingerTree V (Node V A) → Digit A → FingerTree V A
  deep pr m sf = :deep {! (Node-measure pr ∙ measure m) ∙ Node-measure sf  !} pr m sf


text:
module string where

open import bool
open import eq
open import char
open import list
open import nat
open import unit

----------------------------------------------------------------------
-- datatypes
----------------------------------------------------------------------

postulate
  string : Set

{-# BUILTIN STRING string #-}

private
 primitive
  primStringToList   : string → 𝕃 char
  primStringAppend   : string → string → string
  primStringFromList : 𝕃 char → string
  primStringEquality : string → string → 𝔹

-- see string-thms.agda for some axioms about the above primitive functions

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

infixr 6 _^_
infix 8 _=string_

----------------------------------------------------------------------
-- operations
----------------------------------------------------------------------

_^_ : string → string → string
_^_ = primStringAppend

string-to-𝕃char : string → 𝕃 char
string-to-𝕃char = primStringToList

𝕃char-to-string : 𝕃 char → string
𝕃char-to-string = primStringFromList

_=string_ : string → string → 𝔹
_=string_ = primStringEquality

char-to-string : char → string
char-to-string c = 𝕃char-to-string [ c ]

string-append-t : ℕ → Set
string-append-t 0 = string → string
string-append-t (suc n) = string → (string-append-t n)

string-append-h : (n : ℕ) → string → string-append-t n
string-append-h 0 ret = λ x → ret ^ x
string-append-h (suc n) ret = λ x → (string-append-h n (ret ^ x))

string-append : (n : ℕ) → string-append-t n
string-append n = string-append-h n ""

string-concat : 𝕃 string → string
string-concat [] = ""
string-concat (s :: ss) = s ^ (string-concat ss)

string-concat-sep : (separator : string) → 𝕃 string → string
string-concat-sep sep [] = ""
string-concat-sep sep (s1 :: ss) with ss
... | [] = s1
... | s2 :: ss' = s1 ^ sep ^ (string-concat-sep sep ss)

string-concat-sep-map : ∀{A : Set} → (separator : string) → (A → string) → 𝕃 A → string
string-concat-sep-map sep f l = string-concat-sep sep (map f l)

escape-string-h : 𝕃 char → 𝕃 char
escape-string-h ('\n' :: cs) = '\\' :: 'n' :: (escape-string-h cs)
escape-string-h ('"' :: cs) = '\\' :: '"' :: (escape-string-h cs)
escape-string-h (c :: cs) = c :: escape-string-h cs
escape-string-h [] = []

escape-string : string → string
escape-string s = 𝕃char-to-string( escape-string-h( string-to-𝕃char s ) )

string-length : string → ℕ
string-length s = length (string-to-𝕃char s)

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
-- Andreas, 2019-02-23, issue #3586, reported by mcoblenz shrunk by G. Allais
-- WAS: Internal error in ConcreteToAbstract.

-- {-# OPTIONS -v scope.pat:60 #-}

infixl 5 ^_

data D : Set where
  ^_ : D → D

postulate
  _^_ : D → D → D

foo : D → Set
foo x@(y ^ z) = D

-- The term "y ^ z" is parsed as operator pattern (_^_ y z)
-- with _^_ being a variable name.
-- That is nonsense the scope checker did not expect and crashed.
-- Now, we report instead:
--
--   y ^ z is not a valid pattern

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------------
-- Lists
------------------------------------------------------------------------------

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

module FOTC.Data.List where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.List.Type public

infixr 5 _++_

------------------------------------------------------------------------------
-- Basic functions

postulate
  length    : D → D
  length-[] : length []                ≡ zero
  length-∷  : ∀ x xs → length (x ∷ xs) ≡ succ₁ (length xs)
{-# ATP axioms length-[] length-∷ #-}

postulate
  _++_  : D → D → D
  ++-[] : ∀ ys → [] ++ ys            ≡ ys
  ++-∷  : ∀ x xs ys → (x ∷ xs) ++ ys ≡ x ∷ (xs ++ ys)
{-# ATP axioms ++-[] ++-∷ #-}

-- List transformations

postulate
  map    : D → D → D
  map-[] : ∀ f → map f []            ≡ []
  map-∷  : ∀ f x xs → map f (x ∷ xs) ≡ f · x ∷ map f xs
{-# ATP axioms map-[] map-∷ #-}

postulate
  rev    : D → D → D
  rev-[] : ∀ ys → rev [] ys            ≡ ys
  rev-∷  : ∀ x xs ys → rev (x ∷ xs) ys ≡ rev xs (x ∷ ys)
{-# ATP axioms rev-[] rev-∷ #-}

reverse : D → D
reverse xs = rev xs []
{-# ATP definition reverse #-}

postulate
  reverse'    : D → D
  reverse'-[] : reverse' []                ≡ []
  reverse'-∷  : ∀ x xs → reverse' (x ∷ xs) ≡ reverse' xs ++ (x ∷ [])

postulate
  replicate   : D → D → D
  replicate-0 : ∀ x → replicate zero x        ≡ []
  replicate-S : ∀ n x → replicate (succ₁ n) x ≡ x ∷ replicate n x
{-# ATP axioms replicate-0 replicate-S #-}

-- Reducing lists

postulate
  foldr    : D → D → D → D
  foldr-[] : ∀ f n → foldr f n []            ≡ n
  foldr-∷  : ∀ f n x xs → foldr f n (x ∷ xs) ≡ f · x · (foldr f n xs)
{-# ATP axioms foldr-[] foldr-∷ #-}

-- Building lists

postulate
  iterate    : D → D → D
  iterate-eq : ∀ f x → iterate f x ≡ x ∷ iterate f (f · x)
{-# ATP axiom iterate-eq #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Andrea(s), 2018-11-23, issue #3378
--
-- WAS: internal error in coverage checker and clause compiler
-- for missing hcomp clauses triggered by non-exact splitting.

{-# OPTIONS --cubical #-}

-- {-# OPTIONS -v tc.cover:10 #-}

open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.Unit

data Interval : Set where
  pos : Interval
  neg : Interval
  zeroes-identified : pos ≡ neg

test : Interval → Interval → ⊤
test pos pos = tt
test neg pos = tt
test (zeroes-identified i) pos = tt
test x neg = tt
test x (zeroes-identified j) = tt

-- Should pass (with non-exact splitting).


text:
{-# OPTIONS --show-implicit #-}

data Bool : Set where
  true : Bool
  false : Bool

data D : Set where
  d : D

data E : Set where
  e : E

HSet : Set₁
HSet = {b : Bool} → Set

-- Here HA is HSet
-- The output of this function is the set E, for input HSet G.
⊨_ : HSet → Set
⊨_ HA = HA {true}

G : HSet
G {true} = E
G {false} = D

noo : ⊨ G {false}
noo = {!!}

boo : ⊨ λ {b} → G {b}
boo = {!!}


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

module Perm where

-- Definitions for permutations in the Cauchy representation

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

open import Relation.Unary using (Pred)
  renaming (Decidable to UnaryDecidable)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; subst; subst₂; cong; cong₂; setoid;
        proof-irrelevance; module ≡-Reasoning)
open import Relation.Binary.PropositionalEquality.TrustMe
  using (trustMe)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Data.Nat.Properties
  using (cancel-+-left; n∸n≡0; +-∸-assoc; m+n∸n≡m; 1+n≰n; m≤m+n;
         n≤m+n; n≤1+n; cancel-*-right-≤; ≰⇒>; ¬i+1+j≤i)
open import Data.Nat.Properties.Simple
  using (+-right-identity; +-suc; +-assoc; +-comm;
        *-assoc; *-comm; *-right-zero; distribʳ-*-+; +-*-suc)
open import Data.Nat.DivMod using (DivMod; result; _divMod_; _div_; _mod_)
open import Relation.Binary using (Rel; Decidable; Setoid)
open import Relation.Binary.Core using (REL; Transitive; _⇒_)

open import Data.String using (String)
  renaming (_++_ to _++S_)
open import Data.Nat.Show using (show)
open import Data.Bool using (Bool; false; true)
open import Data.Nat using (ℕ; suc; _+_; _∸_; _*_; _<_; _≮_; _≤_; _≰_;
  _≥_; z≤n; s≤s; _≟_; _≤?_; ≤-pred; module ≤-Reasoning)
open import Data.Fin
  using (Fin; zero; suc; toℕ; fromℕ; fromℕ≤; _ℕ-_; _≺_; reduce≥;
         raise; inject+; inject₁; inject≤; _≻toℕ_)
  renaming (_+_ to _F+_)
open import Data.Fin.Properties
  using (bounded; to-from; inject+-lemma; inject≤-lemma; toℕ-injective;
         toℕ-raise; toℕ-fromℕ≤)
open import Data.Vec.Properties
  using (lookup∘tabulate; tabulate∘lookup; lookup-allFin; tabulate-∘;
         tabulate-allFin; allFin-map; lookup-++-inject+; lookup-++-≥;
         lookup-++-<)
open import Data.Product using (Σ; swap)

open import Data.List
  using (List; []; _∷_; _∷ʳ_; foldl; replicate; reverse; downFrom;
         concatMap; gfilter; initLast; InitLast; _∷ʳ'_)
  renaming (_++_ to _++L_; map to mapL; concat to concatL; zip to zipL)
open import Data.List.NonEmpty
  using (List⁺; [_]; _∷⁺_; head; last; _⁺++_)
  renaming (toList to nonEmptyListtoList; _∷ʳ_ to _n∷ʳ_; tail to ntail)
open import Data.List.Any using (Any; here; there; any; module Membership)
open import Data.Maybe using (Maybe; nothing; just; maybe′)
open import Data.Vec
  using (Vec; tabulate; []; _∷_; tail; lookup; zip; zipWith; splitAt;
         _[_]≔_; allFin; toList)
  renaming (_++_ to _++V_; map to mapV; concat to concatV)
open import Function using (id; _∘_; _$_; flip)
open import Data.Maybe using (Maybe; just; nothing)

open import Data.Empty   using (⊥; ⊥-elim)
open import Data.Unit    using (⊤; tt)
open import Data.Sum     using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; _,_; proj₁; proj₂)

open import Proofs
open import Cauchy

------------------------------------------------------------------------------
-- What JC thinks will actually work
-- we need injectivity.  surjectivity ought to be provable.

Permutation : ℕ → Set
Permutation n = Σ (Cauchy n) (λ v → ∀ {i j} → lookup i v ≡ lookup j v → i ≡ j)

------------------------------------------------------------------------------
-- Iso between Fin (m * n) and Fin m × Fin n

absurd-quotient : (m n q : ℕ) (r : Fin (suc n)) (k : Fin (suc (n + m * suc n)))
         (k≡r+q*sn : toℕ k ≡ toℕ r + q * suc n) (p : suc m ≤ q) → ⊥
absurd-quotient m n q r k k≡r+q*sn p = ¬i+1+j≤i (toℕ k) {toℕ r} k≥k+sr
  where k≥k+sr : toℕ k ≥ toℕ k + suc (toℕ r)
        k≥k+sr = begin (toℕ k + suc (toℕ r)
                   ≡⟨ +-suc (toℕ k) (toℕ r) ⟩
                 suc (toℕ k) + toℕ r
                   ≤⟨ cong+r≤ (bounded k) (toℕ r) ⟩
                 (suc n + m * suc n) + toℕ r
                   ≡⟨ +-comm (suc n + m * suc n) (toℕ r) ⟩
                 toℕ r + (suc n + m * suc n)
                   ≡⟨ refl ⟩
                 toℕ r + suc m * suc n
                   ≤⟨ cong+l≤ (cong*r≤ p (suc n)) (toℕ r) ⟩
                 toℕ r + q * suc n
                   ≡⟨ sym k≡r+q*sn ⟩
                 toℕ k ∎)
                  where open ≤-Reasoning

Fin0-⊥ : Fin 0 → ⊥
Fin0-⊥ ()

fin-project : (m n : ℕ) → Fin (m * n) → Fin m × Fin n
fin-project 0 n ()
fin-project (suc m) 0 k =  ⊥-elim (Fin0-⊥ (subst Fin (*-right-zero (suc m)) k))
fin-project (suc m) (suc n) k with (toℕ k) divMod (suc n)
... | result q r k≡r+q*sn = (fromℕ≤ {q} {suc m} (s≤s q≤m) , r)
  where q≤m : q ≤ m
        q≤m with suc m ≤? q
        ... | yes p = ⊥-elim (absurd-quotient m n q r k k≡r+q*sn p)
        ... | no ¬p = ≤-pred (≰⇒> ¬p)

fin-proj-lem : (m n : ℕ) (k : Fin (m * n)) →
  k ≡ let (b , d) = fin-project m n k in
      inject≤ (fromℕ (toℕ b * n + toℕ d)) (i*n+k≤m*n b d)
fin-proj-lem 0 n ()
fin-proj-lem (suc m) 0 k = ⊥-elim (Fin0-⊥ (subst Fin (*-right-zero (suc m)) k))
fin-proj-lem (suc m) (suc n) k with _divMod_ (toℕ k) (suc n) {_}
... | result q r k≡r+q*sn with suc m ≤? q
... | yes p = ⊥-elim (absurd-quotient m n q r k k≡r+q*sn p)
... | no ¬p = toℕ-injective toℕk≡
  where q≡ : (m : ℕ) (q : ℕ) (¬p : ¬ suc m ≤ q) →
             q ≡ toℕ (fromℕ≤ (s≤s (≤-pred (≰⇒> ¬p))))
        q≡ m q ¬p = sym (toℕ-fromℕ≤ (s≤s (≤-pred (≰⇒> ¬p))))
        toℕk≡ = begin (toℕ k
                  ≡⟨ k≡r+q*sn ⟩
                       toℕ r + q * suc n
                  ≡⟨ +-comm (toℕ r) (q * suc n) ⟩
                       q * suc n + toℕ r
                  ≡⟨ cong
                        (λ x → x * suc n + toℕ r)
                        (q≡ m q ¬p) ⟩
                       toℕ (fromℕ≤ (s≤s (≤-pred (≰⇒> ¬p)))) * suc n + toℕ r
                  ≡⟨ sym (to-from
                           (toℕ (fromℕ≤ (s≤s (≤-pred (≰⇒> ¬p)))) * suc n + toℕ r)) ⟩
                       toℕ (fromℕ
                             (toℕ (fromℕ≤ (s≤s (≤-pred (≰⇒> ¬p)))) * suc n + toℕ r))
                  ≡⟨ sym
                       (inject≤-lemma
                         (fromℕ
                           (toℕ (fromℕ≤ (s≤s (≤-pred (≰⇒> ¬p)))) * suc n + toℕ r))
                         (i*n+k≤m*n (fromℕ≤ (s≤s (≤-pred (≰⇒> ¬p)))) r)) ⟩
                       toℕ
                         (inject≤
                           (fromℕ
                             (toℕ (fromℕ≤ (s≤s (≤-pred (≰⇒> ¬p)))) * suc n + toℕ r))
                           (i*n+k≤m*n
                             (fromℕ≤ {q} {suc m} (s≤s (≤-pred (≰⇒> ¬p)))) r)) ∎)
                where open ≡-Reasoning

fin-proj-lem2 : (m n : ℕ) (b : Fin m) (d : Fin n) →
  (b , d) ≡ fin-project m n
              (inject≤ (fromℕ (toℕ b * n + toℕ d)) (i*n+k≤m*n b d))
fin-proj-lem2 m 0 b ()
fin-proj-lem2 0 (suc n) () d
fin-proj-lem2 (suc m) (suc n) b d with
 (toℕ (inject≤ (fromℕ (toℕ b * suc n + toℕ d)) (i*n+k≤m*n b d))) divMod (suc n)
... | result q r eq =
  begin ((b , d)
        ≡⟨ cong₂ _,_
            (toℕ-injective
              (sym
                (trans
                  (toℕ-fromℕ≤ (s≤s (trans≤ (refl′ (proj₁ eq')) (bounded' m b))))
                  (proj₁ eq'))) )
            (sym (proj₂ eq')) ⟩
        (fromℕ≤ (s≤s (trans≤ (refl′ (proj₁ eq')) (bounded' m b))) , r)
        ≡⟨ cong₂ _,_ (cong fromℕ≤ (≤-proof-irrelevance _ _)) refl ⟩
        (fromℕ≤ _ , r) ∎)
  where open ≡-Reasoning
        eq' : q ≡ toℕ b × r ≡ d
        eq' = swap
                (addMul-lemma′ q (toℕ b) n r d
                  (trans
                    (trans (+-comm (q * suc n) (toℕ r)) (sym eq))
                    (trans (inject≤-lemma _ _) (to-from _))))

-- The actual isomorphism

record Fin-Product-Iso (m n : ℕ) : Set where
  constructor iso
  field
    split   : Fin (m * n) → Fin m × Fin n
    combine : Fin m × Fin n → Fin (m * n)
    inv     : (i : Fin (m * n)) → combine (split i) ≡ i
    inv'    : (bd : Fin m × Fin n) → split (combine bd) ≡ bd

fin-product-iso : (m n : ℕ) → Fin-Product-Iso m n
fin-product-iso m n =
  iso
    (fin-project m n)
    (λ {(b , d) → inject≤ (fromℕ (toℕ b * n + toℕ d)) (i*n+k≤m*n b d)})
    (λ k → sym (fin-proj-lem m n k))
    ((λ {(b , d) → sym (fin-proj-lem2 m n b d)}))

record Fin-DivMod (m n : ℕ) (i : Fin (m * n)) : Set where
  constructor fin-result
  field
    b    : Fin m
    d    : Fin n
    dec  : toℕ i ≡ toℕ d + toℕ b * n
    dec' : i ≡ inject≤ (fromℕ (toℕ b * n + toℕ d)) (i*n+k≤m*n b d)

fin-divMod : (m n : ℕ) (i : Fin (m * n)) → Fin-DivMod m n i
fin-divMod m n i = fin-result b d dec dec'
  where
    bd = Fin-Product-Iso.split (fin-product-iso m n) i
    b = proj₁ bd
    d = proj₂ bd
    dec' = sym (Fin-Product-Iso.inv (fin-product-iso m n) i)
    dec = begin (toℕ i
                ≡⟨ cong toℕ (sym (inv (fin-product-iso m n) i)) ⟩
                toℕ (inject≤ (fromℕ (toℕ b * n + toℕ d)) (i*n+k≤m*n b d))
                ≡⟨ inject≤-lemma (fromℕ (toℕ b * n + toℕ d)) (i*n+k≤m*n b d) ⟩
                toℕ (fromℕ (toℕ b * n + toℕ d))
                ≡⟨ to-from (toℕ b * n + toℕ d) ⟩
                toℕ b * n + toℕ d
                ≡⟨ +-comm (toℕ b * n) (toℕ d) ⟩
                toℕ d + toℕ b * n ∎)
          where open ≡-Reasoning
                open Fin-Product-Iso

fin-addMul-lemma : (m n : ℕ) (b b' : Fin m) (d d' : Fin n) →
  toℕ b * n + toℕ d ≡ toℕ b' * n + toℕ d' → b ≡ b' × d ≡ d'
fin-addMul-lemma m 0 _ _ ()
fin-addMul-lemma m (suc n) b b' d d' p =
  let (d≡ , b≡) = addMul-lemma′ (toℕ b) (toℕ b') n d d' p
  in (toℕ-injective b≡ , d≡)

------------------------------------------------------------------------------
-- Vec lemmas

fi≡fj : {m : ℕ} → (i j : Fin m) (f : Fin m → Fin m) →
        (p : lookup i (tabulate f) ≡ lookup j (tabulate f)) → (f i ≡ f j)
fi≡fj i j f p = trans
                  (sym (lookup∘tabulate f i))
                  (trans p (lookup∘tabulate f j))

lookup-bounded : (m n : ℕ) (i : Fin n) (v : Vec (Fin m) n) → toℕ (lookup i v) < m
lookup-bounded m 0 () v
lookup-bounded m (suc n) zero (x ∷ v) = bounded x
lookup-bounded m (suc n) (suc i) (x ∷ v) = lookup-bounded m n i v

lookup-concat-left : ∀ {ℓ} {A : Set ℓ} {m n : ℕ} →
  (d : Fin n) (leq : suc (toℕ d) ≤ n + m) (vs : Vec A n) (ws : Vec A m) →
  lookup (inject≤ (fromℕ (toℕ d)) leq) (vs ++V ws) ≡ lookup d vs
lookup-concat-left zero (s≤s z≤n) (x ∷ vs) ws = refl
lookup-concat-left (suc d) (s≤s leq) (x ∷ vs) ws = lookup-concat-left d leq vs ws

lookup-concat-right : ∀ {ℓ} {A : Set ℓ} {m n : ℕ} →
  (j : ℕ) (leq : suc (n + j) ≤ n + m) (leq' : suc j ≤ m)
  (vs : Vec A n) (ws : Vec A m) →
  lookup (inject≤ (fromℕ (n + j)) leq) (vs ++V ws) ≡
  lookup (inject≤ (fromℕ j) leq') ws
lookup-concat-right {n = 0} j leq leq' [] ws =
  cong
    (λ x → lookup (inject≤ (fromℕ j) x) ws)
    (≤-proof-irrelevance leq leq')
lookup-concat-right {n = suc n} j (s≤s leq) leq' (v ∷ vs) ws =
  lookup-concat-right j leq leq' vs ws

lookup-concat-right' : ∀ {ℓ} {A : Set ℓ} {m n : ℕ} →
  (j k : ℕ) (leq : suc ((n + j) + k) ≤ n + m) (leq' : suc (j + k) ≤ m)
  (vs : Vec A n) (ws : Vec A m) →
  lookup (inject≤ (fromℕ ((n + j) + k)) leq) (vs ++V ws) ≡
  lookup (inject≤ (fromℕ (j + k)) leq') ws
lookup-concat-right' {n = 0} j k leq leq' [] ws =
  cong
    (λ x → lookup (inject≤ (fromℕ (j + k)) x) ws)
    (≤-proof-irrelevance leq leq')
lookup-concat-right' {n = suc n} j k (s≤s leq) leq' (v ∷ vs) ws =
  lookup-concat-right' j k leq leq' vs ws

helper-leq : (m n : ℕ) → (b : Fin m) →
  suc (n + toℕ b * suc n) ≤ n + m * suc n
helper-leq m n b =
  begin (suc (n + toℕ b * suc n)
       ≡⟨ cong suc (+-comm n (toℕ b * suc n)) ⟩
         suc (toℕ b * suc n + n)
       ≡⟨ cong (λ x → suc (toℕ b * suc n + x)) (sym (to-from n)) ⟩
         suc (toℕ b * suc n + toℕ (fromℕ n))
       ≤⟨ i*n+k≤m*n b (fromℕ n) ⟩
         m * suc n
       ≤⟨ n≤m+n n (m * suc n) ⟩
         n + m * suc n ∎)
  where open ≤-Reasoning

helper-leq' : (m n : ℕ) → (b : Fin m) →
  suc (toℕ b * suc n) ≤ m * suc n
helper-leq' 0 n ()
helper-leq' (suc m) n zero = s≤s z≤n
helper-leq' (suc m) n (suc b) = s≤s (helper-leq m n b)

lookup-concat-inner : {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃} →
  (m n : ℕ) (b : Fin m) (j : B)
  (leq : suc (toℕ b * suc n) ≤ m * suc n)
  (f : A × B → C) (pm : Vec A m) (pn : Vec B n) →
  lookup
     (inject≤ (fromℕ (toℕ b * suc n)) leq)
     (concatV (mapV (λ b → mapV (λ d → f (b , d)) (j ∷ pn)) pm))
   ≡ f (lookup b pm , j)
lookup-concat-inner 0 n () j leq f pm pn
lookup-concat-inner (suc m) n zero j (s≤s z≤n) f (i ∷ pm) pn = refl
lookup-concat-inner (suc m) n (suc b) j (s≤s leq) f (i ∷ pm) pn =
  begin (lookup
           (inject≤ (fromℕ (n + toℕ b * suc n)) leq)
           (mapV (λ d → f (i , d)) pn ++V
            concatV (mapV (λ b → mapV (λ d → f (b , d)) (j ∷ pn)) pm))
       ≡⟨ lookup-concat-right (toℕ b * suc n) leq (helper-leq' m n b)
           (mapV (λ d → f (i , d)) pn)
           (concatV (mapV (λ b → mapV (λ d → f (b , d)) (j ∷ pn)) pm)) ⟩
         lookup
           (inject≤ (fromℕ (toℕ b * suc n)) (helper-leq' m n b))
           (concatV (mapV (λ b → mapV (λ d → f (b , d)) (j ∷ pn)) pm))
       ≡⟨ lookup-concat-inner m n b j (helper-leq' m n b) f pm pn ⟩
         f (lookup b pm , j) ∎)
  where open ≡-Reasoning

lookup-concat' : ∀ {ℓ₁ ℓ₂ ℓ₃} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃} →
  (m n : ℕ) (b : Fin m) (d : Fin n) →
  (leq : suc (toℕ b * n + toℕ d) ≤ m * n) →
  (f : A × B → C) (pm : Vec A m) (pn : Vec B n) →
  lookup
    (inject≤ (fromℕ (toℕ b * n + toℕ d)) leq)
    (concatV (mapV (λ b → mapV (λ d → f (b , d)) pn) pm)) ≡
  f (lookup b pm , lookup d pn)
lookup-concat' 0 n () d leq f pm pn
lookup-concat' (suc m) n zero d leq f (i ∷ pm) pn =
  begin (lookup
           (inject≤ (fromℕ (toℕ d)) leq)
           (concatV (mapV (λ b → mapV (λ d → f (b , d)) pn) (i ∷ pm)))
       ≡⟨ refl ⟩
         lookup
           (inject≤ (fromℕ (toℕ d)) leq)
           (concatV (mapV (λ d → f (i , d)) pn ∷
                     mapV (λ b → mapV (λ d → f (b , d)) pn) pm))
       ≡⟨ refl ⟩
         lookup
           (inject≤ (fromℕ (toℕ d)) leq)
           (mapV (λ d → f (i , d)) pn ++V
            concatV (mapV (λ b → mapV (λ d → f (b , d)) pn) pm))
       ≡⟨ lookup-concat-left d leq
            (mapV (λ d → f (i , d)) pn)
            (concatV (mapV (λ b → mapV (λ d → f (b , d)) pn) pm)) ⟩
         lookup d (mapV (λ d → f (i , d)) pn)
       ≡⟨ lookup-map d (λ d → f (i , d)) pn ⟩
         f (i , lookup d pn) ∎)
  where open ≡-Reasoning
lookup-concat' (suc m) 0 (suc b) () leq f (i ∷ pm) pn
lookup-concat' (suc m) (suc n) (suc b) zero (s≤s leq) f (i ∷ pm) (j ∷ pn) =
  begin (lookup
           (inject≤ (fromℕ ((n + toℕ b * suc n) + 0)) leq)
           (mapV (λ d → f (i , d)) pn ++V
            concatV (mapV (λ b → mapV (λ d → f (b , d)) (j ∷ pn)) pm))
       ≡⟨ cong₂D!
            (λ x y →
              lookup
                (inject≤ (fromℕ x) y)
                (mapV (λ d → f (i , d)) pn ++V
                 concatV (mapV (λ b → mapV (λ d → f (b , d)) (j ∷ pn)) pm)))
            (sym (+-right-identity (n + toℕ b * suc n)))
            (≤-proof-irrelevance
              (subst
                 (λ z → suc z ≤ n + m * suc n)
                 (sym (+-right-identity (n + toℕ b * suc n)))
                 (helper-leq m n b))
              leq) ⟩
         lookup
           (inject≤
             (fromℕ (n + toℕ b * suc n))
             (helper-leq m n b))
           (mapV (λ d → f (i , d)) pn ++V
            concatV (mapV (λ b → mapV (λ d → f (b , d)) (j ∷ pn)) pm))
       ≡⟨ lookup-concat-right
             (toℕ b * suc n)
             (helper-leq m n b)
             (helper-leq' m n b)
             (mapV (λ d → f (i , d)) pn)
             (concatV (mapV (λ b → mapV (λ d → f (b , d)) (j ∷ pn)) pm)) ⟩
         lookup
           (inject≤ (fromℕ (toℕ b * suc n)) (helper-leq' m n b))
           (concatV (mapV (λ b → mapV (λ d → f (b , d)) (j ∷ pn)) pm))
       ≡⟨ lookup-concat-inner m n b j (helper-leq' m n b) f pm pn ⟩
         f (lookup b pm , j) ∎)
  where open ≡-Reasoning
lookup-concat' (suc m) (suc n) (suc b) (suc d) (s≤s leq) f (i ∷ pm) (j ∷ pn) =
  begin (lookup
           (inject≤ (fromℕ ((n + toℕ b * suc n) + toℕ (suc d))) leq)
           (mapV (λ d → f (i , d)) pn ++V
            concatV (mapV (λ b → mapV (λ d → f (b , d)) (j ∷ pn)) pm))
       ≡⟨ lookup-concat-right' (toℕ b * suc n) (toℕ (suc d)) leq (i*n+k≤m*n b (suc d))
            (mapV (λ d → f (i , d)) pn)
            (concatV (mapV (λ b → mapV (λ d → f (b , d)) (j ∷ pn)) pm)) ⟩
         lookup
           (inject≤ (fromℕ (toℕ b * suc n + toℕ (suc d))) (i*n+k≤m*n b (suc d)))
           (concatV (mapV (λ b → mapV (λ d → f (b , d)) (j ∷ pn)) pm))
       ≡⟨ lookup-concat' m (suc n) b (suc d) (i*n+k≤m*n b (suc d)) f pm (j ∷ pn) ⟩
         f (lookup b pm , lookup d pn) ∎)
  where open ≡-Reasoning

lookup-2d : (m n : ℕ) (i : Fin (m * n)) (α : Cauchy m) (β : Cauchy n) →
  (h : (Fin m × Fin n) → Fin (m * n)) →
  lookup i (concatV (mapV (λ b → mapV (λ d → h (b , d)) β) α)) ≡
  let fin-result b d _ _ = fin-divMod m n i in h (lookup b α , lookup d β)
lookup-2d m n i α β h =
  let fin-result b d dec dec' = fin-divMod m n i in
  begin (lookup i (concatV (mapV (λ b → mapV (λ d → h (b , d)) β) α))
         ≡⟨ cong
              (λ x → lookup x (concatV (mapV (λ b → mapV (λ d → h (b , d)) β) α)))
              dec' ⟩
         lookup
           (inject≤ (fromℕ (toℕ b * n + toℕ d)) (i*n+k≤m*n b d))
           (concatV (mapV (λ b → mapV (λ d → h (b , d)) β) α))
         ≡⟨ lookup-concat' m n b d (i*n+k≤m*n b d) h α β ⟩
         h (lookup b α , lookup d β) ∎)
  where open ≡-Reasoning

------------------------------------------------------------------------------
-- Elementary permutations in the Cauchy representation

emptyperm : Permutation 0
emptyperm = (emptycauchy , f)
  where f : {i j : Fin 0} → (lookup i emptycauchy ≡ lookup j emptycauchy) → (i ≡ j)
        f {()}

idperm : (n : ℕ) → Permutation n
idperm n = (idcauchy n , λ {i} {j} p → fi≡fj i j id p)

-- Sequential composition

scompperm : ∀ {n} → Permutation n → Permutation n → Permutation n
scompperm {n} (α , f) (β , g) =
  (scompcauchy α β ,
   λ {i} {j} p → f (g (fi≡fj i j (λ i → lookup (lookup i α) β) p)))

-- swap the first m elements with the last n elements
-- [ v₀ , v₁   , v₂   , ... , vm-1 ,     vm , vm₊₁ , ... , vm+n-1 ]
-- ==>
-- [ vm , vm₊₁ , ... , vm+n-1 ,     v₀ , v₁   , v₂   , ... , vm-1 ]

swap+cauchy< : (m n : ℕ) (i : Fin (m + n)) (i< : toℕ i < m) →
  lookup i (swap+cauchy m n) ≡ id+ {m} (raise n (fromℕ≤ i<))
swap+cauchy< m n i i< =
  let j = fromℕ≤ i< in
  let eq = inj₁-≡ i i< in
  begin
    (lookup i (splitVOp+ {m} {n} {f = id+ {m}})
         ≡⟨ cong (flip lookup (splitVOp+ {m} {n} {f = id+ {m}})) eq ⟩
    lookup (inject+ n j)  (splitVOp+ {m} {n} {f = id+ {m}})
         ≡⟨ lookup-++-inject+  (tabulate (id+ {m} ∘ raise n)) (tabulate (id+ {m} ∘ inject+ m)) j ⟩
     lookup j (tabulate {m} (id+ {m} ∘ raise n))
          ≡⟨ lookup∘tabulate (id+ {m} ∘ raise n) j ⟩
     id+ {m} (raise n j) ∎)
  where open ≡-Reasoning

swap+cauchy≥ : (m n : ℕ) (i : Fin (m + n)) (i≥ : m ≤ toℕ i) →
  lookup i (swap+cauchy m n) ≡ subst Fin (+-comm n m) (inject+ m (reduce≥ i i≥))
swap+cauchy≥ m n i i≥ =
  let j = reduce≥ i i≥ in
  let eq = inj₂-≡ i i≥ in
  let v = splitVOp+ {m} {f = id+ {m}} in
  begin (
    lookup i v
        ≡⟨ cong (flip lookup v) eq ⟩
    lookup (raise m j) v
        ≡⟨ lookup-++-raise (tabulate (id+ {m} ∘ raise n)) (tabulate (id+ {m} ∘ inject+ m)) j ⟩
    lookup j (tabulate (id+ {m} ∘ inject+ m))
        ≡⟨ lookup∘tabulate (id+ {m} ∘ inject+ m) j ⟩
    id+ {m} (inject+ m j) ∎)
  where open ≡-Reasoning

swap+perm' : (m n : ℕ) (i j : Fin (m + n))
  (p : lookup i (swap+cauchy m n) ≡ lookup j (swap+cauchy m n)) → (i ≡ j)
swap+perm' m n i j p with toℕ i <? m | toℕ j <? m
... | yes i< | yes j< = toℕ-injective (cancel-+-left n {toℕ i} {toℕ j} ni≡nj)
  where ni≡nj = begin (n + toℕ i
                     ≡⟨ sym (raise< m n i i<)  ⟩
                       toℕ (subst Fin (+-comm n m) (raise n (fromℕ≤ i<)))
                     ≡⟨ cong toℕ (sym (swap+cauchy< m n i i<)) ⟩
                       toℕ (lookup i (swap+cauchy m n))
                     ≡⟨ cong toℕ p ⟩
                       toℕ (lookup j (swap+cauchy m n))
                     ≡⟨ cong toℕ (swap+cauchy< m n j j<) ⟩
                       toℕ (subst Fin (+-comm n m) (raise n (fromℕ≤ j<)))
                     ≡⟨ raise< m n j j< ⟩
                       n + toℕ j ∎)
               where open ≡-Reasoning
... | yes i< | no j≥ = ⊥-elim (1+n≰n contra')
  where contra : n + toℕ i ≡ toℕ j ∸ m
        contra = begin (n + toℕ i
                       ≡⟨ sym (raise< m n i i<) ⟩
                       toℕ (subst Fin (+-comm n m) (raise n (fromℕ≤ i<)))
                       ≡⟨ cong toℕ (sym (swap+cauchy< m n i i<)) ⟩
                       toℕ (lookup i (swap+cauchy m n))
                       ≡⟨ cong toℕ p ⟩
                       toℕ (lookup j (swap+cauchy m n))
                       ≡⟨ cong toℕ (swap+cauchy≥ m n j (≤-pred (≰⇒> j≥))) ⟩
                       toℕ (subst Fin (+-comm n m)
                             (inject+ m (reduce≥ j (≤-pred (≰⇒> j≥)))))
                       ≡⟨ inject≥ m n j (≤-pred (≰⇒> j≥)) ⟩
                       toℕ j ∸ m ∎)
                 where open ≡-Reasoning
        contra' : suc (m + n) ≤ m + n
        contra' = begin (suc (m + n)
                        ≤⟨ m≤m+n (suc (m + n)) (toℕ i) ⟩
                        suc (m + n) + toℕ i
                        ≡⟨ +-assoc (suc m) n (toℕ i) ⟩
                        suc (m + (n + toℕ i))
                        ≡⟨ cong (λ x → suc m + x) contra ⟩
                        suc (m + (toℕ j ∸ m))
                        ≡⟨ cong suc (sym (+-∸-assoc m (≤-pred (≰⇒> j≥))))  ⟩
                        suc ((m + toℕ j) ∸ m)
                        ≡⟨ cong (λ x → suc (x ∸ m)) (+-comm m (toℕ j)) ⟩
                        suc ((toℕ j + m) ∸ m)
                        ≡⟨ cong suc (m+n∸n≡m (toℕ j) m) ⟩
                        suc (toℕ j)
                        ≤⟨ bounded j ⟩
                        m + n ∎)
                  where open ≤-Reasoning
... | no i≥ | yes j< = ⊥-elim (1+n≰n contra')
  where contra : n + toℕ j ≡ toℕ i ∸ m
        contra = begin (n + toℕ j
                       ≡⟨ sym (raise< m n j j<) ⟩
                       toℕ (subst Fin (+-comm n m) (raise n (fromℕ≤ j<)))
                       ≡⟨ cong toℕ (sym (swap+cauchy< m n j j<)) ⟩
                       toℕ (lookup j (swap+cauchy m n))
                       ≡⟨ cong toℕ (sym p) ⟩
                       toℕ (lookup i (swap+cauchy m n))
                       ≡⟨ cong toℕ (swap+cauchy≥ m n i (≤-pred (≰⇒> i≥))) ⟩
                       toℕ (subst Fin (+-comm n m)
                             (inject+ m (reduce≥ i (≤-pred (≰⇒> i≥)))))
                       ≡⟨ inject≥ m n i (≤-pred (≰⇒> i≥)) ⟩
                       toℕ i ∸ m ∎)
                 where open ≡-Reasoning
        contra' : suc (m + n) ≤ m + n
        contra' = begin (suc (m + n)
                        ≤⟨ m≤m+n (suc (m + n)) (toℕ j) ⟩
                        suc (m + n) + toℕ j
                        ≡⟨ +-assoc (suc m) n (toℕ j) ⟩
                        suc (m + (n + toℕ j))
                        ≡⟨ cong (λ x → suc m + x) contra ⟩
                        suc (m + (toℕ i ∸ m))
                        ≡⟨ cong suc (sym (+-∸-assoc m (≤-pred (≰⇒> i≥))))  ⟩
                        suc ((m + toℕ i) ∸ m)
                        ≡⟨ cong (λ x → suc (x ∸ m)) (+-comm m (toℕ i)) ⟩
                        suc ((toℕ i + m) ∸ m)
                        ≡⟨ cong suc (m+n∸n≡m (toℕ i) m) ⟩
                        suc (toℕ i)
                        ≤⟨ bounded i ⟩
                        m + n ∎)
                  where open ≤-Reasoning
... | no i≥ | no j≥ = ∸≡ m n i j (≤-pred (≰⇒> i≥)) (≤-pred (≰⇒> j≥)) ri≡rj
  where ri≡rj = begin (toℕ i ∸ m
                       ≡⟨ sym (inject≥ m n i (≤-pred (≰⇒> i≥))) ⟩
                       toℕ (subst Fin (+-comm n m)
                             (inject+ m (reduce≥ i (≤-pred (≰⇒> i≥)))))
                       ≡⟨ cong toℕ (sym (swap+cauchy≥ m n i (≤-pred (≰⇒> i≥)))) ⟩
                       toℕ (lookup i (swap+cauchy m n))
                       ≡⟨ cong toℕ p ⟩
                       toℕ (lookup j (swap+cauchy m n))
                       ≡⟨ cong toℕ (swap+cauchy≥ m n j (≤-pred (≰⇒> j≥)))  ⟩
                       toℕ (subst Fin (+-comm n m)
                             (inject+ m (reduce≥ j (≤-pred (≰⇒> j≥)))))
                       ≡⟨ inject≥ m n j (≤-pred (≰⇒> j≥)) ⟩
                       toℕ j ∸ m ∎)
                where open ≡-Reasoning

swap+perm : (m n : ℕ) → Permutation (m + n)
swap+perm m n = (swap+cauchy m n , λ {i} {j} p → swap+perm' m n i j p)

-- Parallel additive composition
-- append both permutations but adjust the indices in the second
-- permutation by the size of the first type so that it acts on the
-- second part of the vector

pcompperm' : (m n : ℕ) (i j : Fin (m + n))
  (α : Cauchy m) (β : Cauchy n)
  (p : lookup i (pcompcauchy α β) ≡ lookup j (pcompcauchy α β))
  (f : {i j : Fin m} → lookup i α ≡ lookup j α → i ≡ j)
  (g : {i j : Fin n} → lookup i β ≡ lookup j β → i ≡ j) → i ≡ j
pcompperm' m n i j α β p f g with toℕ i <? m | toℕ j <? m
... | yes i< | yes j< = fromℕ≤-inj m (m + n) i j i< j< (f (toℕ-injective li≡lj))
  where li≡lj = begin (toℕ (lookup (fromℕ≤ i<) α)
                       ≡⟨ inject+-lemma n (lookup (fromℕ≤ i<) α) ⟩
                       toℕ (inject+ n (lookup (fromℕ≤ i<) α))
                       ≡⟨ cong toℕ (sym (lookup-map (fromℕ≤ i<) (inject+ n) α)) ⟩
                       toℕ (lookup (fromℕ≤ i<) (mapV (inject+ n) α))
                       ≡⟨ cong toℕ (sym (lookup-++-<
                                      (mapV (inject+ n) α)
                                      (mapV (raise m) β)
                                      i i<)) ⟩
                       toℕ (lookup i (mapV (inject+ n) α ++V mapV (raise m) β))
                       ≡⟨ cong toℕ p ⟩
                       toℕ (lookup j (mapV (inject+ n) α ++V mapV (raise m) β))
                       ≡⟨ cong toℕ (lookup-++-<
                                     (mapV (inject+ n) α)
                                     (mapV (raise m) β)
                                     j j<) ⟩
                       toℕ (lookup (fromℕ≤ j<) (mapV (inject+ n) α))
                       ≡⟨ cong toℕ (lookup-map (fromℕ≤ j<) (inject+ n) α) ⟩
                       toℕ (inject+ n (lookup (fromℕ≤ j<) α))
                       ≡⟨ sym (inject+-lemma n (lookup (fromℕ≤ j<) α)) ⟩
                       toℕ (lookup (fromℕ≤ j<) α) ∎)
                where open ≡-Reasoning
... | yes i< | no j≥ = ⊥-elim (1+n≰n contra')
  where contra = begin (toℕ (lookup (fromℕ≤ i<) α)
                       ≡⟨ inject+-lemma n (lookup (fromℕ≤ i<) α) ⟩
                       toℕ (inject+ n (lookup (fromℕ≤ i<) α))
                       ≡⟨ cong toℕ (sym (lookup-map (fromℕ≤ i<) (inject+ n) α)) ⟩
                       toℕ (lookup (fromℕ≤ i<) (mapV (inject+ n) α))
                       ≡⟨ cong toℕ (sym (lookup-++-<
                                      (mapV (inject+ n) α)
                                      (mapV (raise m) β)
                                      i i<)) ⟩
                       toℕ (lookup i (mapV (inject+ n) α ++V mapV (raise m) β))
                       ≡⟨ cong toℕ p ⟩
                       toℕ (lookup j (mapV (inject+ n) α ++V mapV (raise m) β))
                       ≡⟨ cong toℕ (lookup-++-≥
                                     (mapV (inject+ n) α)
                                     (mapV (raise m) β)
                                     j (≤-pred (≰⇒> j≥))) ⟩
                       toℕ (lookup (reduce≥ j (≤-pred (≰⇒> j≥))) (mapV (raise m) β))
                       ≡⟨ cong toℕ
                           (lookup-map (reduce≥ j (≤-pred (≰⇒> j≥))) (raise m) β) ⟩
                       toℕ (raise m (lookup (reduce≥ j (≤-pred (≰⇒> j≥))) β))
                       ≡⟨ toℕ-raise m (lookup (reduce≥ j (≤-pred (≰⇒> j≥))) β) ⟩
                       m + toℕ (lookup (reduce≥ j (≤-pred (≰⇒> j≥))) β) ∎)
                 where open ≡-Reasoning
        contra' = begin (suc (toℕ (lookup (fromℕ≤ i<) α))
                        ≤⟨ lookup-bounded m m (fromℕ≤ i<) α ⟩
                        m
                        ≤⟨ m≤m+n m (toℕ (lookup (reduce≥ j (≤-pred (≰⇒> j≥))) β)) ⟩
                        m + toℕ (lookup (reduce≥ j (≤-pred (≰⇒> j≥))) β)
                        ≡⟨ sym contra ⟩
                        toℕ (lookup (fromℕ≤ i<) α) ∎)
                  where open ≤-Reasoning
... | no i≥ | yes j< = ⊥-elim (1+n≰n contra')
  where contra = begin (m + toℕ (lookup (reduce≥ i (≤-pred (≰⇒> i≥))) β)
                       ≡⟨ sym (toℕ-raise m (lookup (reduce≥ i (≤-pred (≰⇒> i≥))) β)) ⟩
                       toℕ (raise m (lookup (reduce≥ i (≤-pred (≰⇒> i≥))) β))
                       ≡⟨ cong toℕ
                           (sym (lookup-map (reduce≥ i (≤-pred (≰⇒> i≥))) (raise m) β)) ⟩
                       toℕ (lookup (reduce≥ i (≤-pred (≰⇒> i≥))) (mapV (raise m) β))
                       ≡⟨ cong toℕ (sym (lookup-++-≥
                                      (mapV (inject+ n) α)
                                      (mapV (raise m) β)
                                      i (≤-pred (≰⇒> i≥)))) ⟩
                       toℕ (lookup i (mapV (inject+ n) α ++V mapV (raise m) β))
                       ≡⟨ cong toℕ p ⟩
                       toℕ (lookup j (mapV (inject+ n) α ++V mapV (raise m) β))
                       ≡⟨ cong toℕ (lookup-++-<
                                     (mapV (inject+ n) α)
                                     (mapV (raise m) β)
                                     j j<) ⟩
                       toℕ (lookup (fromℕ≤ j<) (mapV (inject+ n) α))
                       ≡⟨ cong toℕ (lookup-map (fromℕ≤ j<) (inject+ n) α) ⟩
                       toℕ (inject+ n (lookup (fromℕ≤ j<) α))
                       ≡⟨ sym (inject+-lemma n (lookup (fromℕ≤ j<) α)) ⟩
                        toℕ (lookup (fromℕ≤ j<) α) ∎)
                 where open ≡-Reasoning
        contra' = begin (suc (toℕ (lookup (fromℕ≤ j<) α))
                        ≤⟨ lookup-bounded m m (fromℕ≤ j<) α ⟩
                        m
                        ≤⟨ m≤m+n m (toℕ (lookup (reduce≥ i (≤-pred (≰⇒> i≥))) β)) ⟩
                        m + toℕ (lookup (reduce≥ i (≤-pred (≰⇒> i≥))) β)
                        ≡⟨ contra ⟩
                        toℕ (lookup (fromℕ≤ j<) α) ∎)
                  where open ≤-Reasoning
... | no i≥ | no j≥ =
  reduce≥-inj m n i j (≤-pred (≰⇒> i≥)) (≤-pred (≰⇒> j≥))
    (g (toℕ-injective (cancel-+-left m li≡lj)))
  where li≡lj = begin (m + toℕ (lookup (reduce≥ i (≤-pred (≰⇒> i≥))) β)
                       ≡⟨ sym (toℕ-raise m (lookup (reduce≥ i (≤-pred (≰⇒> i≥))) β)) ⟩
                       toℕ (raise m (lookup (reduce≥ i (≤-pred (≰⇒> i≥))) β))
                       ≡⟨ cong toℕ
                           (sym (lookup-map (reduce≥ i (≤-pred (≰⇒> i≥))) (raise m) β)) ⟩
                       toℕ (lookup (reduce≥ i (≤-pred (≰⇒> i≥))) (mapV (raise m) β))
                       ≡⟨ cong toℕ (sym (lookup-++-≥
                                      (mapV (inject+ n) α)
                                      (mapV (raise m) β)
                                      i (≤-pred (≰⇒> i≥)))) ⟩
                       toℕ (lookup i (mapV (inject+ n) α ++V mapV (raise m) β))
                       ≡⟨ cong toℕ p ⟩
                       toℕ (lookup j (mapV (inject+ n) α ++V mapV (raise m) β))
                       ≡⟨ cong toℕ (lookup-++-≥
                                     (mapV (inject+ n) α)
                                     (mapV (raise m) β)
                                     j (≤-pred (≰⇒> j≥))) ⟩
                       toℕ (lookup (reduce≥ j (≤-pred (≰⇒> j≥))) (mapV (raise m) β))
                       ≡⟨ cong toℕ
                           (lookup-map (reduce≥ j (≤-pred (≰⇒> j≥))) (raise m) β) ⟩
                       toℕ (raise m (lookup (reduce≥ j (≤-pred (≰⇒> j≥))) β))
                       ≡⟨ toℕ-raise m (lookup (reduce≥ j (≤-pred (≰⇒> j≥))) β) ⟩
                       m + toℕ (lookup (reduce≥ j (≤-pred (≰⇒> j≥))) β) ∎)
                where open ≡-Reasoning

pcompperm : ∀ {m n} → Permutation m → Permutation n → Permutation (m + n)
pcompperm {m} {n} (α , f) (β , g) =
  (pcompcauchy α β , λ {i} {j} p → pcompperm' m n i j α β p f g)

-- Tensor multiplicative composition
-- Transpositions in α correspond to swapping entire rows
-- Transpositions in β correspond to swapping entire columns

tcompperm' : (m n : ℕ) (i j : Fin (m * n)) (α : Cauchy m) (β : Cauchy n)
  (f : {i j : Fin m} → lookup i α ≡ lookup j α → i ≡ j)
  (g : {i j : Fin n} → lookup i β ≡ lookup j β → i ≡ j)
  (p : lookup i (tcompcauchy α β) ≡ lookup j (tcompcauchy α β)) → (i ≡ j)
tcompperm' m n i j α β f g p =
  let fin-result bi di deci deci' = fin-divMod m n i
      fin-result bj dj decj decj' = fin-divMod m n j
      (lookb≡ , lookd≡) = fin-addMul-lemma
                            m n (lookup bi α) (lookup bj α)
                            (lookup di β) (lookup dj β) sp
      (b≡ , d≡) = (f {bi} {bj} lookb≡ , g {di} {dj} lookd≡)
      bn+d≡ = cong₂ (λ b d → toℕ d + toℕ b * n) b≡ d≡
  in toℕ-injective (trans deci (trans bn+d≡ (sym decj)))
  where sp = let fin-result bi di deci deci' = fin-divMod m n i
                 fin-result bj dj decj decj' = fin-divMod m n j in
             begin (let b' = lookup bi α
                        d' = lookup di β
                     in toℕ b' * n + toℕ d'
                   ≡⟨ sym (to-from _) ⟩
                   toℕ
                     (let b' = lookup bi α
                          d' = lookup di β
                      in fromℕ (toℕ b' * n + toℕ d'))
                   ≡⟨ sym (inject≤-lemma _ _) ⟩
                   toℕ
                     (let b' = lookup bi α
                          d' = lookup di β
                      in inject≤
                           (fromℕ (toℕ b' * n + toℕ d'))
                           (i*n+k≤m*n b' d'))
                   ≡⟨ cong toℕ
                        (sym (lookup-2d m n i α β
                             (λ {(b , d) → inject≤
                                             (fromℕ (toℕ b * n + toℕ d))
                                             (i*n+k≤m*n b d)}))) ⟩
                   toℕ (lookup i (tcompcauchy α β))
                   ≡⟨ cong toℕ p ⟩
                   toℕ (lookup j (tcompcauchy α β))
                   ≡⟨ cong toℕ
                        (lookup-2d m n j α β
                          (λ {(b , d) → inject≤
                                          (fromℕ (toℕ b * n + toℕ d))
                                          (i*n+k≤m*n b d)})) ⟩
                   toℕ
                     (let b' = lookup bj α
                          d' = lookup dj β
                      in inject≤
                           (fromℕ (toℕ b' * n + toℕ d'))
                           (i*n+k≤m*n b' d'))
                   ≡⟨ inject≤-lemma _ _ ⟩
                   toℕ
                     (let b' = lookup bj α
                          d' = lookup dj β
                      in fromℕ (toℕ b' * n + toℕ d'))
                   ≡⟨ to-from _ ⟩
                   let b' = lookup bj α
                       d' = lookup dj β
                   in toℕ b' * n + toℕ d' ∎)
             where open ≡-Reasoning

tcompperm : ∀ {m n} → Permutation m → Permutation n → Permutation (m * n)
tcompperm {m} {n} (α , f) (β , g) =
  (tcompcauchy α β , λ {i} {j} p → tcompperm' m n i j α β f g p)

-- swap⋆
--
-- This is essentially the classical problem of in-place matrix transpose:
-- "http://en.wikipedia.org/wiki/In-place_matrix_transposition"
-- Given m and n, the desired permutation in Cauchy representation is:
-- P(i) = m*n-1 if i=m*n-1
--      = m*i mod m*n-1 otherwise

transpose≡ : (m n : ℕ) (i j : Fin (m * n)) (bi bj : Fin m) (di dj : Fin n)
             (deci : toℕ i ≡ toℕ di + toℕ bi * n)
             (decj : toℕ j ≡ toℕ dj + toℕ bj * n)
             (tpr : transposeIndex m n bi di ≡ transposeIndex m n bj dj) → (i ≡ j)
transpose≡ m n i j bi bj di dj deci decj tpr =
  let (d≡ , b≡) = fin-addMul-lemma n m di dj bi bj stpr
      d+bn≡ = cong₂ (λ x y → toℕ x + toℕ y * n) d≡ b≡
  in toℕ-injective (trans deci (trans d+bn≡ (sym decj)))
  where stpr = begin (toℕ di * m + toℕ bi
                      ≡⟨ sym (to-from _) ⟩
                      toℕ (fromℕ (toℕ di * m + toℕ bi))
                      ≡⟨ sym (inject≤-lemma _ _) ⟩
                      toℕ (inject≤
                        (fromℕ (toℕ di * m + toℕ bi))
                        (trans≤
                          (i*n+k≤m*n di bi)
                          (refl′ (*-comm n m))))
                      ≡⟨ cong toℕ tpr ⟩
                      toℕ (inject≤
                        (fromℕ (toℕ dj * m + toℕ bj))
                        (trans≤
                          (i*n+k≤m*n dj bj)
                          (refl′ (*-comm n m))))
                      ≡⟨ inject≤-lemma _ _ ⟩
                      toℕ (fromℕ (toℕ dj * m + toℕ bj))
                      ≡⟨ to-from _ ⟩
                      toℕ dj * m + toℕ bj ∎)
               where open ≡-Reasoning

swap⋆perm' : (m n : ℕ) (i j : Fin (m * n))
             (p : lookup i (swap⋆cauchy m n) ≡ lookup j (swap⋆cauchy m n)) → (i ≡ j)
swap⋆perm' m n i j p =
  let fin-result bi di deci _ = fin-divMod m n i
      fin-result bj dj decj _ = fin-divMod m n j
  in transpose≡ m n i j bi bj di dj deci decj pr
  where pr = let fin-result bi di _ _ = fin-divMod m n i
                 fin-result bj dj _ _ = fin-divMod m n j in
             begin (transposeIndex m n bi di
                    ≡⟨ cong₂ (transposeIndex m n)
                         (sym (lookup-allFin bi)) (sym (lookup-allFin di)) ⟩
                    transposeIndex m n (lookup bi (allFin m)) (lookup di (allFin n))
                    ≡⟨ sym (lookup-2d m n i (allFin m) (allFin n)
                             (λ {(b , d) → transposeIndex m n b d})) ⟩
                    lookup i
                      (concatV (mapV
                        (λ b → mapV (λ d → transposeIndex m n b d) (allFin n))
                        (allFin m)))
                    ≡⟨ p ⟩
                    lookup j
                      (concatV (mapV
                        (λ b → mapV (λ d → transposeIndex m n b d) (allFin n))
                        (allFin m)))
                    ≡⟨ lookup-2d m n j (allFin m) (allFin n)
                         (λ {(b , d) → transposeIndex m n b d}) ⟩
                    transposeIndex m n (lookup bj (allFin m)) (lookup dj (allFin n))
                    ≡⟨ cong₂ (transposeIndex m n)
                         (lookup-allFin bj) (lookup-allFin dj) ⟩
                    transposeIndex m n bj dj ∎)
             where open ≡-Reasoning

swap⋆perm : (m n : ℕ) → Permutation (m * n)
swap⋆perm m n = (swap⋆cauchy m n , λ {i} {j} p → swap⋆perm' m n i j p)

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Pointwise lifting of relations to lists
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Pointwise where

open import Function.Base
open import Function.Inverse using (Inverse)
open import Data.Bool.Base using (true; false)
open import Data.Product hiding (map)
open import Data.List.Base as List hiding (map; head; tail; uncons)
open import Data.List.Properties using (≡-dec; length-++)
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_)
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.Fin.Base using (Fin) renaming (zero to fzero; suc to fsuc)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Nat.Properties
open import Level
open import Relation.Nullary hiding (Irrelevant)
open import Relation.Nullary.Negation using (contradiction)
import Relation.Nullary.Decidable as Dec using (map′)
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Unary as U using (Pred)
open import Relation.Binary renaming (Rel to Rel₂)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

private
  variable
    a b c d p q r ℓ ℓ₁ ℓ₂ ℓ₃ : Level
    A : Set a
    B : Set b
    C : Set c
    D : Set d

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

infixr 5 _∷_

data Pointwise {A : Set a} {B : Set b} (_∼_ : REL A B ℓ)
               : List A → List B → Set (a ⊔ b ⊔ ℓ) where
  []  : Pointwise _∼_ [] []
  _∷_ : ∀ {x xs y ys} (x∼y : x ∼ y) (xs∼ys : Pointwise _∼_ xs ys) →
        Pointwise _∼_ (x ∷ xs) (y ∷ ys)

------------------------------------------------------------------------
-- Operations

module _ {_∼_ : REL A B ℓ} where

  head : ∀ {x y xs ys} → Pointwise _∼_ (x ∷ xs) (y ∷ ys) → x ∼ y
  head (x∼y ∷ xs∼ys) = x∼y

  tail : ∀ {x y xs ys} → Pointwise _∼_ (x ∷ xs) (y ∷ ys) →
         Pointwise _∼_ xs ys
  tail (x∼y ∷ xs∼ys) = xs∼ys

  uncons : ∀ {x y xs ys} → Pointwise _∼_ (x ∷ xs) (y ∷ ys) →
           x ∼ y × Pointwise _∼_ xs ys
  uncons = < head , tail >

  rec : ∀ (P : ∀ {xs ys} → Pointwise _∼_ xs ys → Set c) →
        (∀ {x y xs ys} {xs∼ys : Pointwise _∼_ xs ys} →
          (x∼y : x ∼ y) → P xs∼ys → P (x∼y ∷ xs∼ys)) →
        P [] →
        ∀ {xs ys} (xs∼ys : Pointwise _∼_ xs ys) → P xs∼ys
  rec P c n []            = n
  rec P c n (x∼y ∷ xs∼ys) = c x∼y (rec P c n xs∼ys)

  map : ∀ {_≈_ : REL A B ℓ₂} → _≈_ ⇒ _∼_ → Pointwise _≈_ ⇒ Pointwise _∼_
  map ≈⇒∼ []            = []
  map ≈⇒∼ (x≈y ∷ xs≈ys) = ≈⇒∼ x≈y ∷ map ≈⇒∼ xs≈ys

------------------------------------------------------------------------
-- Relational properties

reflexive : ∀ {_≈_ : REL A B ℓ₁} {_∼_ : REL A B ℓ₂} →
            _≈_ ⇒ _∼_ → Pointwise _≈_ ⇒ Pointwise _∼_
reflexive ≈⇒∼ []            = []
reflexive ≈⇒∼ (x≈y ∷ xs≈ys) = ≈⇒∼ x≈y ∷ reflexive ≈⇒∼ xs≈ys

refl : ∀ {_∼_ : Rel₂ A ℓ} → Reflexive _∼_ → Reflexive (Pointwise _∼_)
refl rfl {[]}     = []
refl rfl {x ∷ xs} = rfl ∷ refl rfl

symmetric : ∀ {_≈_ : REL A B ℓ₁} {_∼_ : REL B A ℓ₂} →
            Sym _≈_ _∼_ → Sym (Pointwise _≈_) (Pointwise _∼_)
symmetric sym []            = []
symmetric sym (x∼y ∷ xs∼ys) = sym x∼y ∷ symmetric sym xs∼ys

transitive : ∀ {_≋_ : REL A B ℓ₁} {_≈_ : REL B C ℓ₂} {_∼_ : REL A C ℓ₃} →
             Trans _≋_ _≈_ _∼_ →
             Trans (Pointwise _≋_) (Pointwise _≈_) (Pointwise _∼_)
transitive trans []            []            = []
transitive trans (x∼y ∷ xs∼ys) (y∼z ∷ ys∼zs) =
  trans x∼y y∼z ∷ transitive trans xs∼ys ys∼zs

antisymmetric : ∀ {_≤_ : REL A B ℓ₁} {_≤′_ : REL B A ℓ₂} {_≈_ : REL A B ℓ₃} →
                Antisym _≤_ _≤′_ _≈_ →
                Antisym (Pointwise _≤_) (Pointwise _≤′_) (Pointwise _≈_)
antisymmetric antisym []            []            = []
antisymmetric antisym (x∼y ∷ xs∼ys) (y∼x ∷ ys∼xs) =
  antisym x∼y y∼x ∷ antisymmetric antisym xs∼ys ys∼xs

respects₂ : ∀ {_≈_ : Rel₂ A ℓ₁} {_∼_ : Rel₂ A ℓ₂} →
            _∼_ Respects₂ _≈_ → (Pointwise _∼_) Respects₂ (Pointwise _≈_)
respects₂ {_≈_ = _≈_} {_∼_} resp = respʳ , respˡ
  where
  respʳ : (Pointwise _∼_) Respectsʳ (Pointwise _≈_)
  respʳ []            []            = []
  respʳ (x≈y ∷ xs≈ys) (z∼x ∷ zs∼xs) =
    proj₁ resp x≈y z∼x ∷ respʳ xs≈ys zs∼xs

  respˡ : (Pointwise _∼_) Respectsˡ (Pointwise _≈_)
  respˡ []            []            = []
  respˡ (x≈y ∷ xs≈ys) (x∼z ∷ xs∼zs) =
    proj₂ resp x≈y x∼z ∷ respˡ xs≈ys xs∼zs

module _ {_∼_ : REL A B ℓ} (dec : Decidable _∼_) where

  decidable : Decidable (Pointwise _∼_)
  decidable []       []       = yes []
  decidable []       (y ∷ ys) = no (λ ())
  decidable (x ∷ xs) []       = no (λ ())
  decidable (x ∷ xs) (y ∷ ys) =
    Dec.map′ (uncurry _∷_) uncons (dec x y ×-dec decidable xs ys)

module _ {_≈_ : Rel₂ A ℓ} where

  isEquivalence : IsEquivalence _≈_ → IsEquivalence (Pointwise _≈_)
  isEquivalence eq = record
    { refl  = refl       Eq.refl
    ; sym   = symmetric  Eq.sym
    ; trans = transitive Eq.trans
    } where module Eq = IsEquivalence eq

  isDecEquivalence : IsDecEquivalence _≈_ → IsDecEquivalence (Pointwise _≈_)
  isDecEquivalence eq = record
    { isEquivalence = isEquivalence DE.isEquivalence
    ; _≟_           = decidable     DE._≟_
    } where module DE = IsDecEquivalence eq

module _ {_≈_ : Rel₂ A ℓ₁} {_∼_ : Rel₂ A ℓ₂} where

  isPreorder : IsPreorder _≈_ _∼_ → IsPreorder (Pointwise _≈_) (Pointwise _∼_)
  isPreorder pre = record
    { isEquivalence = isEquivalence Pre.isEquivalence
    ; reflexive     = reflexive     Pre.reflexive
    ; trans         = transitive    Pre.trans
    } where module Pre = IsPreorder pre

  isPartialOrder : IsPartialOrder _≈_ _∼_ →
                   IsPartialOrder (Pointwise _≈_) (Pointwise _∼_)
  isPartialOrder po = record
    { isPreorder = isPreorder    PO.isPreorder
    ; antisym    = antisymmetric PO.antisym
    } where module PO = IsPartialOrder po

setoid : Setoid a ℓ → Setoid a (a ⊔ ℓ)
setoid s = record
  { isEquivalence = isEquivalence (Setoid.isEquivalence s)
  }

decSetoid : DecSetoid a ℓ → DecSetoid a (a ⊔ ℓ)
decSetoid d = record
  { isDecEquivalence = isDecEquivalence (DecSetoid.isDecEquivalence d)
  }

preorder : Preorder a ℓ₁ ℓ₂ → Preorder _ _ _
preorder p = record
  { isPreorder = isPreorder (Preorder.isPreorder p)
  }

poset : Poset a ℓ₁ ℓ₂ → Poset _ _ _
poset p = record
  { isPartialOrder = isPartialOrder (Poset.isPartialOrder p)
  }

------------------------------------------------------------------------
-- Relationships to other predicates

module _ {_∼_ : Rel₂ A ℓ} {P : Pred A p} where

  All-resp-Pointwise : P Respects _∼_ → (All P) Respects (Pointwise _∼_)
  All-resp-Pointwise resp []         []         = []
  All-resp-Pointwise resp (x∼y ∷ xs) (px ∷ pxs) =
    resp x∼y px ∷ All-resp-Pointwise resp xs pxs

  Any-resp-Pointwise : P Respects _∼_ → (Any P) Respects (Pointwise _∼_)
  Any-resp-Pointwise resp (x∼y ∷ xs) (here px)   = here (resp x∼y px)
  Any-resp-Pointwise resp (x∼y ∷ xs) (there pxs) = there (Any-resp-Pointwise resp xs pxs)

module _ {_∼_ : Rel₂ A ℓ} {R : Rel₂ A r} where

  AllPairs-resp-Pointwise : R Respects₂ _∼_ → (AllPairs R) Respects (Pointwise _∼_)
  AllPairs-resp-Pointwise _                    []         []         = []
  AllPairs-resp-Pointwise resp@(respₗ , respᵣ) (x∼y ∷ xs) (px ∷ pxs) =
    All-resp-Pointwise respₗ xs (All.map (respᵣ x∼y) px) ∷ (AllPairs-resp-Pointwise resp xs pxs)

------------------------------------------------------------------------
-- length

module _ {_∼_ : REL A B ℓ} where

  Pointwise-length : ∀ {xs ys} → Pointwise _∼_ xs ys →
                     length xs ≡ length ys
  Pointwise-length []            = P.refl
  Pointwise-length (x∼y ∷ xs∼ys) = P.cong ℕ.suc (Pointwise-length xs∼ys)

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

module _ {_∼_ : REL A B ℓ} where

  tabulate⁺ : ∀ {n} {f : Fin n → A} {g : Fin n → B} →
              (∀ i → f i ∼ g i) → Pointwise _∼_ (tabulate f) (tabulate g)
  tabulate⁺ {zero}  f∼g = []
  tabulate⁺ {suc n} f∼g = f∼g fzero ∷ tabulate⁺ (f∼g ∘ fsuc)

  tabulate⁻ : ∀ {n} {f : Fin n → A} {g : Fin n → B} →
              Pointwise _∼_ (tabulate f) (tabulate g) → (∀ i → f i ∼ g i)
  tabulate⁻ {suc n} (x∼y ∷ xs∼ys) fzero    = x∼y
  tabulate⁻ {suc n} (x∼y ∷ xs∼ys) (fsuc i) = tabulate⁻ xs∼ys i

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

module _ {_∼_ : REL A B ℓ} where

  ++⁺ : ∀ {ws xs ys zs} → Pointwise _∼_ ws xs → Pointwise _∼_ ys zs →
        Pointwise _∼_ (ws ++ ys) (xs ++ zs)
  ++⁺ []            ys∼zs = ys∼zs
  ++⁺ (w∼x ∷ ws∼xs) ys∼zs = w∼x ∷ ++⁺ ws∼xs ys∼zs

module _ {_∼_ : Rel₂ A ℓ} where

  ++-cancelˡ : ∀ xs {ys zs : List A} → Pointwise _∼_ (xs ++ ys) (xs ++ zs) → Pointwise _∼_ ys zs
  ++-cancelˡ []       ys∼zs               = ys∼zs
  ++-cancelˡ (x ∷ xs) (_ ∷ xs++ys∼xs++zs) = ++-cancelˡ xs xs++ys∼xs++zs

  ++-cancelʳ : ∀ {xs : List A} ys zs → Pointwise _∼_ (ys ++ xs) (zs ++ xs) → Pointwise _∼_ ys zs
  ++-cancelʳ []       []       _             = []
  ++-cancelʳ (y ∷ ys) (z ∷ zs) (y∼z ∷ ys∼zs) = y∼z ∷ (++-cancelʳ ys zs ys∼zs)
  -- Impossible cases
  ++-cancelʳ {xs}     []       (z ∷ zs) eq   =
    contradiction (P.trans (Pointwise-length eq) (length-++ (z ∷ zs))) (m≢1+n+m (length xs))
  ++-cancelʳ {xs}     (y ∷ ys) []       eq   =
    contradiction (P.trans (P.sym (length-++ (y ∷ ys))) (Pointwise-length eq)) (m≢1+n+m (length xs) ∘ P.sym)

------------------------------------------------------------------------
-- concat

module _ {_∼_ : REL A B ℓ} where

  concat⁺ : ∀ {xss yss} → Pointwise (Pointwise _∼_) xss yss →
            Pointwise _∼_ (concat xss) (concat yss)
  concat⁺ []                = []
  concat⁺ (xs∼ys ∷ xss∼yss) = ++⁺ xs∼ys (concat⁺ xss∼yss)

------------------------------------------------------------------------
-- reverse

module _ {R : REL A B ℓ} where

  reverseAcc⁺ : ∀ {as bs as′ bs′} → Pointwise R as′ bs′ → Pointwise R as bs →
                Pointwise R (reverseAcc as′ as) (reverseAcc bs′ bs)
  reverseAcc⁺ rs′ []       = rs′
  reverseAcc⁺ rs′ (r ∷ rs) = reverseAcc⁺ (r ∷ rs′) rs

  ʳ++⁺ : ∀ {as bs as′ bs′} →
           Pointwise R as bs →
           Pointwise R as′ bs′ →
           Pointwise R (as ʳ++ as′) (bs ʳ++ bs′)
  ʳ++⁺ rs rs′ = reverseAcc⁺ rs′ rs

  reverse⁺ : ∀ {as bs} → Pointwise R as bs → Pointwise R (reverse as) (reverse bs)
  reverse⁺ = reverseAcc⁺ []

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

module _ {R : REL C D ℓ} where

  map⁺ : ∀ {as bs} (f : A → C) (g : B → D) →
         Pointwise (λ a b → R (f a) (g b)) as bs →
         Pointwise R (List.map f as) (List.map g bs)
  map⁺ f g []       = []
  map⁺ f g (r ∷ rs) = r ∷ map⁺ f g rs

  map⁻ : ∀ {as bs} (f : A → C) (g : B → D) →
         Pointwise R (List.map f as) (List.map g bs) →
         Pointwise (λ a b → R (f a) (g b)) as bs
  map⁻ {as = []}     {[]}     f g [] = []
  map⁻ {as = []}     {b ∷ bs} f g rs = contradiction (Pointwise-length rs) λ()
  map⁻ {as = a ∷ as} {[]}     f g rs = contradiction (Pointwise-length rs) λ()
  map⁻ {as = a ∷ as} {b ∷ bs} f g (r ∷ rs) = r ∷ map⁻ f g rs

------------------------------------------------------------------------
-- filter

module _ {R : REL A B ℓ} {P : Pred A p} {Q : Pred B q}
         (P? : U.Decidable P) (Q? : U.Decidable Q)
         (P⇒Q : ∀ {a b} → R a b → P a → Q b)
         (Q⇒P : ∀ {a b} → R a b → Q b → P a)
         where

  filter⁺ : ∀ {as bs} → Pointwise R as bs → Pointwise R (filter P? as) (filter Q? bs)
  filter⁺ []       = []
  filter⁺ {a ∷ _} {b ∷ _} (r ∷ rs) with P? a | Q? b
  ... | true  because _ | true  because _ = r ∷ filter⁺ rs
  ... | false because _ | false because _ = filter⁺ rs
  ... | yes p | no ¬q = contradiction (P⇒Q r p) ¬q
  ... | no ¬p | yes q = contradiction (Q⇒P r q) ¬p

------------------------------------------------------------------------
-- replicate

module _ {R : REL A B ℓ} where

  replicate⁺ : ∀ {a b} → R a b → ∀ n → Pointwise R (replicate n a) (replicate n b)
  replicate⁺ r 0       = []
  replicate⁺ r (suc n) = r ∷ replicate⁺ r n

------------------------------------------------------------------------
-- Irrelevance

module _ {R : REL A B ℓ} where

  irrelevant : Irrelevant R → Irrelevant (Pointwise R)
  irrelevant R-irr [] [] = P.refl
  irrelevant R-irr (r ∷ rs) (r₁ ∷ rs₁) =
    P.cong₂ _∷_ (R-irr r r₁) (irrelevant R-irr rs rs₁)

------------------------------------------------------------------------
-- Properties of propositional pointwise

Pointwise-≡⇒≡ : Pointwise {A = A} _≡_ ⇒ _≡_
Pointwise-≡⇒≡ []               = P.refl
Pointwise-≡⇒≡ (P.refl ∷ xs∼ys) with Pointwise-≡⇒≡ xs∼ys
... | P.refl = P.refl

≡⇒Pointwise-≡ :  _≡_ ⇒ Pointwise {A = A} _≡_
≡⇒Pointwise-≡ P.refl = refl P.refl

Pointwise-≡↔≡ : Inverse (setoid (P.setoid A)) (P.setoid (List A))
Pointwise-≡↔≡ = record
  { to         = record { _⟨$⟩_ = id; cong = Pointwise-≡⇒≡ }
  ; from       = record { _⟨$⟩_ = id; cong = ≡⇒Pointwise-≡ }
  ; inverse-of = record
    { left-inverse-of  = λ _ → refl P.refl
    ; right-inverse-of = λ _ → P.refl
    }
  }

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.15

Rel    = Pointwise
{-# WARNING_ON_USAGE Rel
"Warning: Rel was deprecated in v0.15.
Please use Pointwise instead."
#-}
Rel≡⇒≡ = Pointwise-≡⇒≡
{-# WARNING_ON_USAGE Rel≡⇒≡
"Warning: Rel≡⇒≡ was deprecated in v0.15.
Please use Pointwise-≡⇒≡ instead."
#-}
≡⇒Rel≡ = ≡⇒Pointwise-≡
{-# WARNING_ON_USAGE ≡⇒Rel≡
"Warning: ≡⇒Rel≡ was deprecated in v0.15.
Please use ≡⇒Pointwise-≡ instead."
#-}
Rel↔≡  = Pointwise-≡↔≡
{-# WARNING_ON_USAGE Rel↔≡
"Warning: Rel↔≡ was deprecated in v0.15.
Please use Pointwise-≡↔≡ instead."
#-}

-- Version 1.0

decidable-≡ = ≡-dec
{-# WARNING_ON_USAGE decidable-≡
"Warning: decidable-≡ was deprecated in v1.0.
Please use ≡-dec from `Data.List.Properties` instead."
#-}


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

open import Functions.Definition
open import Orders.WellFounded.Definition

module Orders.WellFounded.Induction {a b : _} {A : Set a} {_<_ : Rel {a} {b} A} (wf : WellFounded _<_) where

private
  foldAcc :
    {c : _}
    (P : A → Set c) →
    (∀ x → (∀ y → y < x → P y) → P x) →
    ∀ z → Accessible _<_ z →
    P z
  foldAcc P inductionProof = go
    where
      go : (z : A) → (Accessible _<_ z) → P z
      go z (access prf) = inductionProof z (λ y yLessZ → go y (prf y yLessZ))

rec :
  {c : _}
  (P : A → Set c) →
  (∀ x → (∀ y → y < x → P y) → P x) → (∀ z → P z)
rec P inductionProof z = foldAcc P inductionProof _ (wf z)


text:
module DecidableMembership where

open import OscarPrelude
open import Membership
open import Successor

record DecidableMembership {ℓ} (m : Set ℓ) (M : Set ℓ) ⦃ _ : Membership m M ⦄ : Set (⊹ ℓ)
 where
  field _∈?_ : (x : m) → (X : M) → Dec $ x ∈ X
  field _∉?_ : (x : m) → (X : M) → Dec $ x ∉ X

open DecidableMembership ⦃ … ⦄ public

instance DecidableMembershipList : ∀ {ℓ} {A : Set ℓ} ⦃ _ : Eq A ⦄ → DecidableMembership A $ List A
DecidableMembership._∈?_ (DecidableMembershipList {ℓ} {A}) = _∈List?_
 where
  _∈List?_ : (a : A) → (xs : List A) → Dec (a ∈ xs)
  a ∈List? [] = no λ ()
  a ∈List? (x ∷ xs) with a ≟ x
  … | yes a≡x rewrite a≡x = yes zero
  … | no a≢x with a ∈List? xs
  … | yes a∈xs = yes (⊹ a∈xs)
  … | no a∉xs = no (λ {zero → a≢x refl ; (suc a∈xs) → a∉xs a∈xs})
DecidableMembership._∉?_ (DecidableMembershipList {ℓ} {A}) x X with x ∈? X
DecidableMembership._∉?_ (DecidableMembershipList {ℓ} {A}) x X | yes x∈X = no (λ x∉X → x∉X x∈X)
DecidableMembership._∉?_ (DecidableMembershipList {ℓ} {A}) x X | no x∉X = yes x∉X


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The Delay type and some operations
------------------------------------------------------------------------

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

module Codata.Delay where

open import Size
open import Codata.Thunk using (Thunk; force)
open import Codata.Conat using (Conat; zero; suc; Finite)

open import Data.Empty
open import Relation.Nullary
open import Data.Nat.Base
open import Data.Maybe.Base hiding (map ; fromMaybe ; zipWith ; alignWith ; zip ; align)
open import Data.Product as P hiding (map ; zip)
open import Data.Sum as S hiding (map)
open import Data.These as T using (These; this; that; these)
open import Function

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

data Delay {ℓ} (A : Set ℓ) (i : Size) : Set ℓ where
  now   : A → Delay A i
  later : Thunk (Delay A) i → Delay A i

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

 length : ∀ {i} → Delay A i → Conat i
 length (now _)   = zero
 length (later d) = suc λ where .force → length (d .force)

 never : ∀ {i} → Delay A i
 never = later λ where .force → never

 fromMaybe : Maybe A → Delay A ∞
 fromMaybe = maybe now never

 runFor : ℕ → Delay A ∞ → Maybe A
 runFor zero    d         = nothing
 runFor (suc n) (now a)   = just a
 runFor (suc n) (later d) = runFor n (d .force)

module _ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′} where

 map : (A → B) → ∀ {i} → Delay A i → Delay B i
 map f (now a)   = now (f a)
 map f (later d) = later λ where .force → map f (d .force)

 bind : ∀ {i} → Delay A i → (A → Delay B i) → Delay B i
 bind (now a)   f = f a
 bind (later d) f = later λ where .force → bind (d .force) f

 unfold : (A → A ⊎ B) → A → ∀ {i} → Delay B i
 unfold next seed with next seed
 ... | inj₁ seed′ = later λ where .force → unfold next seed′
 ... | inj₂ b     = now b

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

 zipWith : (A → B → C) → ∀ {i} → Delay A i → Delay B i → Delay C i
 zipWith f (now a)   d         = map (f a) d
 zipWith f d         (now b)   = map (λ a → f a b) d
 zipWith f (later a) (later b) = later λ where .force → zipWith f (a .force) (b .force)

 alignWith : (These A B → C) → ∀ {i} → Delay A i → Delay B i → Delay C i
 alignWith f (now a)   (now b)   = now (f (these a b))
 alignWith f (now a)   (later _) = now (f (this a))
 alignWith f (later _) (now b)   = now (f (that b))
 alignWith f (later a) (later b) = later λ where
   .force → alignWith f (a .force) (b .force)

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

  zip : ∀ {i} → Delay A i → Delay B i → Delay (A × B) i
  zip   = zipWith _,_

  align : ∀ {i} → Delay A i → Delay B i → Delay (These A B) i
  align = alignWith id

------------------------------------------------------------------------
-- Finite Delays

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

 infix 3 _⇓
 data _⇓ : Delay A ∞ → Set ℓ where
   now   : ∀ a → now a ⇓
   later : ∀ {d} → d .force ⇓ → later d ⇓

 extract : ∀ {d} → d ⇓ → A
 extract (now a)   = a
 extract (later d) = extract d

 ¬never⇓ : ¬ (never ⇓)
 ¬never⇓ (later p) = ¬never⇓ p

 length-⇓ : ∀ {d} → d ⇓ → Finite (length d)
 length-⇓ (now a)    = zero
 length-⇓ (later d⇓) = suc (length-⇓ d⇓)

module _ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′} where

 map-⇓ : ∀ (f : A → B) {d} → d ⇓ → map f d ⇓
 map-⇓ f (now a)   = now (f a)
 map-⇓ f (later d) = later (map-⇓ f d)

 bind-⇓ : ∀ {m} (m⇓ : m ⇓) {f : A → Delay B ∞} → f (extract m⇓) ⇓ → bind m f ⇓
 bind-⇓ (now a)   fa⇓ = fa⇓
 bind-⇓ (later p) fa⇓ = later (bind-⇓ p fa⇓)


text:
-- Andreas, 2017-04-28, issue #2558 reported by Youyou Cong
-- Size solver assumed invariants that do not hold.

open import Common.Size

data Con (i : Size) : Set where
  c : {j : Size< i} → Con i  -- needed

postulate
  Tms : {i j : Size} → Con i → Con j → Set
  Ty  : (i : Size) {j : Size< i} → Con j → Set

  sub : ∀{i}{j k : Size< i} {l : Size< j} {Γ : Con k} {Δ : Con l} →
          Tms Γ Δ → Ty j Δ → Ty i Γ

  P   : ∀{A : Set} (a : A) → Set

  [][]T : {i : Size} {j : Size< i} {k : Size< ↑ i} {l : Size< ↑ (↑ i)}
          {Γ : Con l} {Δ : Con k} {Σ : Con j} {A : Ty i Σ} →
          (δ : Tms Δ Σ) →
          (σ : Tms Γ Δ) →  -- Γ needed
          P (sub σ (sub δ A))  -- sub σ needed

-- Should pass