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

module ConcretePermutation where

import Level using (zero)
open import Data.Nat using (ℕ; _+_; _*_)
open import Data.Fin using (Fin; zero; suc; inject+; raise)
open import Data.Sum
  using (_⊎_; inj₁; inj₂; [_,_]′)
  renaming (map to map⊎)
open import Data.Product using (_×_; proj₁; proj₂; _,′_)
open import Data.Vec
  using (Vec; _∷_; []; tabulate; _>>=_; allFin)
  renaming (_++_ to _++V_; map to mapV; concat to concatV)
open import Data.Vec.Properties
  using (lookup-allFin; tabulate∘lookup; lookup∘tabulate; lookup-++-inject+;
         tabulate-∘)
open import Function using (_∘_; id)
open import Algebra using (CommutativeSemiring)
open import Algebra.Structures using
  (IsSemigroup; IsCommutativeMonoid; IsCommutativeSemiring)
open import Relation.Binary using (IsEquivalence)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans;
         cong; cong₂; module ≡-Reasoning; proof-irrelevance)

open import Proofs using (
  -- FiniteFunctions
     finext;
  -- VectorLemmas
     lookup-++-raise; lookupassoc; tabulate-split; _!!_; unSplit;
     concat-map; map-map-map; lookup-map; map-∘;
     left!!; right!!
     )

open import FinVec -- using ()
open import FinVecProperties -- using ()

------------------------------------------------------------------------------
-- a concrete permutation has 4 components:
-- - the permutation
-- - its inverse
-- - and 2 proofs that it is indeed inverse

record CPerm (values : ℕ) (size : ℕ) : Set where
  constructor cp
  field
    π : FinVec values size
    πᵒ : FinVec size values
    αp : π ∘̂ πᵒ ≡ 1C
    βp : πᵒ ∘̂ π ≡ 1C

πᵒ≡ : ∀ {m n} → (π₁ π₂ : CPerm m n) → (CPerm.π π₁ ≡ CPerm.π π₂) →
  (CPerm.πᵒ π₁ ≡ CPerm.πᵒ π₂)
πᵒ≡ {n} (cp π πᵒ αp βp) (cp .π πᵒ₁ αp₁ βp₁) refl =
  begin (
    πᵒ                  ≡⟨ sym (∘̂-rid πᵒ) ⟩
    πᵒ ∘̂ 1C          ≡⟨  cong (_∘̂_ πᵒ) (sym αp₁)  ⟩
    πᵒ ∘̂ (π ∘̂ πᵒ₁)      ≡⟨ ∘̂-assoc πᵒ π πᵒ₁ ⟩
    (πᵒ ∘̂ π) ∘̂ πᵒ₁      ≡⟨ cong (λ x → x ∘̂ πᵒ₁) βp ⟩
    1C ∘̂ πᵒ₁            ≡⟨ ∘̂-lid πᵒ₁ ⟩
    πᵒ₁ ∎)
  where open ≡-Reasoning

p≡ : ∀ {m n} → {π₁ π₂ : CPerm m n} → (CPerm.π π₁ ≡ CPerm.π π₂) → π₁ ≡ π₂
p≡ {m} {n} {cp π πᵒ αp βp} {cp .π πᵒ₁ αp₁ βp₁} refl with
  πᵒ≡ (cp π πᵒ αp βp) (cp π πᵒ₁ αp₁ βp₁) refl
p≡ {m} {n} {cp π πᵒ αp βp} {cp .π .πᵒ αp₁ βp₁} refl | refl
  with proof-irrelevance αp αp₁ | proof-irrelevance βp βp₁
p≡ {m} {n} {cp π πᵒ αp βp} {cp .π .πᵒ .αp .βp} refl | refl | refl | refl = refl

idp : ∀ {n} → CPerm n n
idp {n} = cp 1C 1C (∘̂-rid _) (∘̂-lid _)

symp : ∀ {m n} → CPerm m n → CPerm n m
symp (cp p₁ p₂ α β) = cp p₂ p₁ β α

transp : ∀ {m₁ m₂ m₃} → CPerm m₂ m₁ → CPerm m₃ m₂ → CPerm m₃ m₁
transp {n} (cp π πᵒ αp βp) (cp π₁ πᵒ₁ αp₁ βp₁) = cp (π ∘̂ π₁) (πᵒ₁ ∘̂ πᵒ) pf₁ pf₂
  where
    open ≡-Reasoning
    pf₁ : (π ∘̂ π₁) ∘̂ (πᵒ₁ ∘̂ πᵒ) ≡ 1C
    pf₁ =
      begin (
        (π ∘̂ π₁) ∘̂ (πᵒ₁ ∘̂ πᵒ)      ≡⟨ ∘̂-assoc _ _ _ ⟩
        ((π ∘̂ π₁) ∘̂ πᵒ₁) ∘̂ πᵒ      ≡⟨ cong (λ x → x ∘̂ πᵒ) (sym (∘̂-assoc _ _ _)) ⟩
        (π ∘̂ (π₁ ∘̂ πᵒ₁)) ∘̂ πᵒ      ≡⟨ cong (λ x → (π ∘̂ x) ∘̂ πᵒ) (αp₁) ⟩
        (π ∘̂ 1C) ∘̂ πᵒ       ≡⟨ cong (λ x → x ∘̂ πᵒ) (∘̂-rid _) ⟩
        π ∘̂ πᵒ                     ≡⟨ αp ⟩
        1C ∎)
    pf₂ : (πᵒ₁ ∘̂ πᵒ) ∘̂ (π ∘̂ π₁) ≡ 1C
    pf₂ =
      begin (
        (πᵒ₁ ∘̂ πᵒ) ∘̂ (π ∘̂ π₁)     ≡⟨ ∘̂-assoc _ _ _ ⟩
        ((πᵒ₁ ∘̂ πᵒ) ∘̂ π) ∘̂ π₁     ≡⟨ cong (λ x → x ∘̂ π₁) (sym (∘̂-assoc _ _ _)) ⟩
        (πᵒ₁ ∘̂ (πᵒ ∘̂ π)) ∘̂ π₁     ≡⟨ cong (λ x → (πᵒ₁ ∘̂ x) ∘̂ π₁) βp ⟩
        (πᵒ₁ ∘̂ 1C) ∘̂ π₁     ≡⟨ cong (λ x → x ∘̂ π₁) (∘̂-rid _) ⟩
         πᵒ₁ ∘̂ π₁                 ≡⟨ βp₁ ⟩
        1C ∎)

-- zero permutation

0p : CPerm 0 0
0p = idp {0}

_⊎p_ : ∀ {m₁ m₂ n₁ n₂} → CPerm m₁ m₂ → CPerm n₁ n₂ → CPerm (m₁ + n₁) (m₂ + n₂)
_⊎p_ {m₁} {m₂} {n₁} {n₂} π₀ π₁ =
  cp ((π π₀) ⊎c (π π₁)) ((πᵒ π₀) ⊎c (πᵒ π₁)) pf₁ pf₂
  where
    open CPerm
    open ≡-Reasoning
    pf₁ : (π π₀ ⊎c π π₁) ∘̂ (πᵒ π₀ ⊎c πᵒ π₁) ≡ 1C
    pf₁ =
      begin (
        (π π₀ ⊎c π π₁) ∘̂ (πᵒ π₀ ⊎c πᵒ π₁)
          ≡⟨ ⊎c-distrib {p₁ = π π₀} ⟩
       (π π₀ ∘̂ πᵒ π₀) ⊎c (π π₁ ∘̂ πᵒ π₁)
          ≡⟨ cong₂ _⊎c_ (αp π₀) (αp π₁) ⟩
        1C {m₂} ⊎c 1C {n₂}
          ≡⟨ 1C⊎1C≡1C {m₂} ⟩
        1C ∎)
    pf₂ : (πᵒ π₀ ⊎c πᵒ π₁) ∘̂ (π π₀ ⊎c π π₁) ≡ 1C
    pf₂ =
      begin (
        (πᵒ π₀ ⊎c πᵒ π₁) ∘̂ (π π₀ ⊎c π π₁)
          ≡⟨ ⊎c-distrib {p₁ = πᵒ π₀} ⟩
        (πᵒ π₀ ∘̂ π π₀) ⊎c (πᵒ π₁ ∘̂ π π₁)
          ≡⟨ cong₂ _⊎c_ (βp π₀) (βp π₁) ⟩
        1C {m₁} ⊎c 1C {n₁}
          ≡⟨ 1C⊎1C≡1C {m₁} ⟩
        1C ∎ )

-- For the rest of the permutations, it is convenient to lift things from
-- FinVec in one go; but don't use it yet, it makes other things fall apart
{--
mkPerm : {m n : ℕ} (eq : Fin m ≃ Fin n) → CPerm m n
mkPerm {m} {n} eq = cp p q p∘̂q≡1 q∘̂p≡1
  where
    f = proj₁ eq
    g = proj₁ (sym≃ eq)
    p = tabulate g -- note the flip!
    q = tabulate f
    q∘̂p≡1 = ~⇒≡ {f = g} {g = f} (p∘!p≡id {p = eq})
    p∘̂q≡1 = ~⇒≡ {f = f} {g = g} (p∘!p≡id {p = sym≃ eq})
--}

unite+p : {m : ℕ} → CPerm m (0 + m)
unite+p {m} =
  cp (unite+ {m}) (uniti+ {m}) (unite+∘̂uniti+~id {m}) (uniti+∘̂unite+~id {m})

uniti+p : {m : ℕ} → CPerm (0 + m) m
uniti+p {m} = symp (unite+p {m})

unite+rp : {m : ℕ} → CPerm m (m + 0)
unite+rp {m} =
  cp (unite+r {m}) (uniti+r) (unite+r∘̂uniti+r~id) (uniti+r∘̂unite+r~id)

uniti+rp : {m : ℕ} → CPerm (m + 0) m
uniti+rp {m} = symp (unite+rp {m})

assocl+p : {m n o : ℕ} → CPerm ((m + n) + o) (m + (n + o))
assocl+p {m} =
  cp
    (assocl+ {m}) (assocr+ {m})
    (assocl+∘̂assocr+~id {m}) (assocr+∘̂assocl+~id {m})

assocr+p : {m n o : ℕ} → CPerm (m + (n + o)) ((m + n) + o)
assocr+p {m} = symp (assocl+p {m})

swap+p : {m n : ℕ} → CPerm (n + m) (m + n)
swap+p {m} {n} =
  cp (swap+cauchy m n) (swap+cauchy n m) (swap+-inv {m}) (swap+-inv {n})

unite*p : {m : ℕ} → CPerm m (1 * m)
unite*p {m} =
  cp (unite* {m}) (uniti* {m}) (unite*∘̂uniti*~id {m}) (uniti*∘̂unite*~id {m})

uniti*p : {m : ℕ} → CPerm (1 * m) m
uniti*p {m} = symp (unite*p {m})

unite*rp : {m : ℕ} → CPerm m (m * 1)
unite*rp {m} =
  cp
    (unite*r {m}) (uniti*r {m})
    (unite*r∘̂uniti*r~id {m}) (uniti*r∘̂unite*r~id {m})

uniti*rp : {m : ℕ} → CPerm (m * 1) m
uniti*rp {m} = symp (unite*rp {m})

swap*p : {m n : ℕ} → CPerm (n * m) (m * n)
swap*p {m} {n} =
  cp (swap⋆cauchy m n) (swap⋆cauchy n m) (swap*-inv {m}) (swap*-inv {n})

assocl*p : {m n o : ℕ} → CPerm ((m * n) * o) (m * (n * o))
assocl*p {m} =
  cp
    (assocl* {m}) (assocr* {m})
    (assocl*∘̂assocr*~id {m}) (assocr*∘̂assocl*~id {m})

assocr*p : {m n o : ℕ} → CPerm (m * (n * o)) ((m * n) * o)
assocr*p {m} = symp (assocl*p {m})

_×p_ : ∀ {m₁ m₂ n₁ n₂} → CPerm m₁ m₂ → CPerm n₁ n₂ → CPerm (m₁ * n₁) (m₂ * n₂)
_×p_ {m₁} {m₂} {n₁} {n₂} π₀ π₁ =
  cp ((π π₀) ×c (π π₁)) ((πᵒ π₀) ×c (πᵒ π₁)) pf₁ pf₂
  where
    open CPerm
    open ≡-Reasoning
    pf₁ : (π π₀ ×c π π₁) ∘̂ (πᵒ π₀ ×c πᵒ π₁) ≡ 1C
    pf₁ =
      begin (
        (π π₀ ×c π π₁) ∘̂ (πᵒ π₀ ×c πᵒ π₁) ≡⟨ ×c-distrib {p₁ = π π₀} ⟩
        (π π₀ ∘̂ πᵒ π₀) ×c (π π₁ ∘̂ πᵒ π₁)  ≡⟨ cong₂ _×c_ (αp π₀) (αp π₁) ⟩
        1C ×c 1C                          ≡⟨ 1C×1C≡1C ⟩
        1C ∎)
    pf₂ : (πᵒ π₀ ×c πᵒ π₁) ∘̂ (π π₀ ×c π π₁) ≡ 1C
    pf₂ =
      begin (
        (πᵒ π₀ ×c πᵒ π₁) ∘̂ (π π₀ ×c π π₁) ≡⟨ ×c-distrib {p₁ = πᵒ π₀} ⟩
        (πᵒ π₀ ∘̂ π π₀) ×c (πᵒ π₁ ∘̂ π π₁) ≡⟨ cong₂ _×c_ (βp π₀) (βp π₁) ⟩
        1C ×c 1C                          ≡⟨ 1C×1C≡1C ⟩
        1C ∎)

distp : {m n o : ℕ} → CPerm (m * o + n * o) ((m + n) * o)
distp {m} {n} {o} =
  cp
    (dist*+ {m}) (factor*+ {m})
    (dist*+∘̂factor*+~id {m}) (factor*+∘̂dist*+~id {m})

factorp : {m n o : ℕ} → CPerm ((m + n) * o) (m * o + n * o)
factorp {m} = symp (distp {m})

distlp : {m n o : ℕ} → CPerm (m * n + m * o) (m * (n + o))
distlp {m} {n} {o} =
  cp
    (distl*+ {m}) (factorl*+ {m})
    (distl*+∘̂factorl*+~id {m}) (factorl*+∘̂distl*+~id {m})

factorlp : {m n o : ℕ} → CPerm (m * (n + o)) (m * n + m * o)
factorlp {m} = symp (distlp {m})

-- right-zero absorbing permutation

0pr : ∀ {n} → CPerm 0 (n * 0)
0pr {n} =
  cp
    (right-zero*l {n}) (right-zero*r {n})
    (right-zero*l∘̂right-zero*r~id {n}) (right-zero*r∘̂right-zero*l~id {n})

-- and its symmetric version

0pl : ∀ {n} → CPerm (n * 0) 0
0pl {n} = symp (0pr {n})

--

ridp : ∀ {m₁ m₂} {p : CPerm m₂ m₁} → transp p idp ≡ p
ridp {p = p} = p≡ (∘̂-rid (CPerm.π p))

lidp : ∀ {m₁ m₂} {p : CPerm m₂ m₁} → transp idp p ≡ p
lidp {p = p} = p≡ (∘̂-lid (CPerm.π p))

assocp : ∀ {m₁ m₂ m₃ n₁} → {p₁ : CPerm m₁ n₁} → {p₂ : CPerm m₂ m₁} →
  {p₃ : CPerm m₃ m₂} →
  transp p₁ (transp p₂ p₃) ≡ transp (transp p₁ p₂) p₃
assocp {p₁ = p₁} {p₂} {p₃} =
  p≡ (∘̂-assoc (CPerm.π p₁) (CPerm.π p₂) (CPerm.π p₃))

linv : ∀ {m₁ m₂} (p : CPerm m₂ m₁) → transp p (symp p) ≡ idp
linv p = p≡ (CPerm.αp p)

rinv : ∀ {m₁ m₂} (p : CPerm m₂ m₁) → transp (symp p) p ≡ idp
rinv p = p≡ (CPerm.βp p)

transp-resp-≡ : ∀ {m₁ m₂ m₃} {f h : CPerm m₂ m₃} {g i : CPerm m₁ m₂} →
  f ≡ h → g ≡ i → transp f g ≡ transp h i
transp-resp-≡ refl refl = refl

1p⊎1p≡1p : ∀ {m n} → idp {m} ⊎p idp {n} ≡ idp
1p⊎1p≡1p {m} = p≡ (1C⊎1C≡1C {m})

1p×1p≡1p : ∀ {m n} → idp {m} ×p idp {n} ≡ idp
1p×1p≡1p {m} = p≡ (1C×1C≡1C {m})

⊎p-distrib :  ∀ {m₁ m₂ m₃ m₄ n₁ n₂} → {p₁ : CPerm m₁ n₁} → {p₂ : CPerm m₂ n₂}
    → {p₃ : CPerm m₃ m₁} → {p₄ : CPerm m₄ m₂} →
      transp (p₁ ⊎p p₂) (p₃ ⊎p p₄) ≡ (transp p₁ p₃) ⊎p (transp p₂ p₄)
⊎p-distrib {p₁ = p₁} = p≡ (⊎c-distrib {p₁ = CPerm.π p₁})

×p-distrib :  ∀ {m₁ m₂ m₃ m₄ n₁ n₂} → {p₁ : CPerm m₁ n₁} → {p₂ : CPerm m₂ n₂}
    → {p₃ : CPerm m₃ m₁} → {p₄ : CPerm m₄ m₂} →
      (transp p₁ p₃) ×p (transp p₂ p₄) ≡ transp (p₁ ×p p₂) (p₃ ×p p₄)
×p-distrib {p₁ = p₁} = p≡ (sym (×c-distrib {p₁ = CPerm.π p₁}))

0p⊎x≡x : ∀ {m n} {p : CPerm m n} → idp {0} ⊎p p ≡ p
0p⊎x≡x {p = p} = p≡ 1C₀⊎x≡x

-- this comes from looking at things categorically:

unite+p∘[0⊎x]≡x∘unite+p : ∀ {m n} (p : CPerm m n) →
  transp unite+p (0p ⊎p p) ≡ transp p unite+p
unite+p∘[0⊎x]≡x∘unite+p p = p≡ unite+∘[0⊎x]≡x∘unite+

uniti+p∘x≡[0⊎x]∘uniti+p : ∀ {m n} (p : CPerm m n) →
  transp uniti+p p ≡ transp (0p ⊎p p) uniti+p
uniti+p∘x≡[0⊎x]∘uniti+p p = p≡ (uniti+∘x≡[0⊎x]∘uniti+ {x = CPerm.π p})

-- and the right version
{-
unite+rp∘[x⊎0]≡x∘unite+rp : ∀ {m n} (p : CPerm m n) →
  transp unite+rp (p ⊎p 0p) ≡ transp p unite+rp
unite+rp∘[x⊎0]≡x∘unite+rp p = p≡ ?

uniti+rp∘[x⊎0]≡x∘uniti+rp : ∀ {m n} (p : CPerm m n) →
  transp uniti+rp (p ⊎p 0p) ≡ transp p uniti+rp
uniti+rp∘[x⊎0]≡x∘uniti+rp p = p≡ {!!}
-}

-- SCPerm : ℕ → ℕ → Setoid zero zero
-- SCPerm m n = setoid (CPerm m n)

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
{-

  Reflection-based tools for converting between iterated record types, particularly between
  record types and iterated Σ-types. Currently requires eta equality.

  See end of file for examples.

-}
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Reflection.RecordEquiv where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Data.List as List
open import Cubical.Data.Nat
open import Cubical.Data.Maybe
open import Cubical.Data.Sigma

import Agda.Builtin.Reflection as R
open import Cubical.Reflection.Base

Projections = List R.Name

-- Describes a correspondence between two iterated record types
Assoc = List (Projections × Projections)

-- Describes a correspondence between a record type and an iterated Σ-types;
-- more convenient than Assoc for this special case
data ΣFormat : Type where
  leaf : R.Name → ΣFormat
  _,_ : ΣFormat → ΣFormat → ΣFormat

infixr 4 _,_

module Internal where

  flipAssoc : Assoc → Assoc
  flipAssoc = List.map λ {p .fst → p .snd; p .snd → p .fst}

  list→ΣFormat : List R.Name → Maybe ΣFormat
  list→ΣFormat [] = nothing
  list→ΣFormat (x ∷ []) = just (leaf x)
  list→ΣFormat (x ∷ y ∷ xs) = map-Maybe (leaf x ,_) (list→ΣFormat (y ∷ xs))

  recordName→ΣFormat : R.Name → R.TC (Maybe ΣFormat)
  recordName→ΣFormat name = R.getDefinition name >>= go
    where
    go : R.Definition → R.TC (Maybe ΣFormat)
    go (R.record-type c fs) = R.returnTC (list→ΣFormat (List.map (λ {(R.arg _ n) → n}) fs))
    go _ = R.typeError (R.strErr "Not a record type name:" ∷ R.nameErr name ∷ [])

  ΣFormat→Assoc : ΣFormat → Assoc
  ΣFormat→Assoc = go []
    where
    go : List R.Name → ΣFormat → Assoc
    go prefix (leaf fieldName) = [ prefix , [ fieldName ] ]
    go prefix (sig₁ , sig₂) =
      go (quote fst ∷ prefix) sig₁ ++ go (quote snd ∷ prefix) sig₂

  MaybeΣFormat→Assoc : Maybe ΣFormat → Assoc
  MaybeΣFormat→Assoc nothing = [ [] , [] ]
  MaybeΣFormat→Assoc (just sig) = ΣFormat→Assoc sig

  convertTerm : Assoc → R.Term → R.Term
  convertTerm al term = R.pat-lam (List.map makeClause al) []
    where
    makeClause : Projections × Projections → R.Clause
    makeClause (projl , projr) =
      R.clause [] (goPat [] projr) (goTm projl)
      where
      goPat : List (R.Arg R.Pattern) → List R.Name → List (R.Arg R.Pattern)
      goPat acc [] = acc
      goPat acc (π ∷ projs) = goPat (varg (R.proj π) ∷ acc) projs

      goTm : List R.Name → R.Term
      goTm [] = term
      goTm (π ∷ projs) = R.def π [ varg (goTm projs) ]

  convertFun : Assoc → R.Term
  convertFun al = vlam "ρ" (convertTerm al (v 0))

  convertMacro : Assoc → R.Term → R.TC Unit
  convertMacro al hole = R.unify hole (convertFun al)

  equivMacro : Assoc → R.Term → R.TC Unit
  equivMacro al hole =
    newMeta R.unknown >>= λ hole₁ →
    newMeta R.unknown >>= λ hole₂ →
    let
      iso : R.Term
      iso =
        R.pat-lam
          ( R.clause [] [ varg (R.proj (quote Iso.fun)) ] hole₁
          ∷ R.clause [] [ varg (R.proj (quote Iso.inv)) ] hole₂
          ∷ R.clause [] [ varg (R.proj (quote Iso.rightInv)) ] (vlam "_" (R.def (quote refl) []))
          ∷ R.clause [] [ varg (R.proj (quote Iso.leftInv)) ] (vlam "_" (R.def (quote refl) []))
          ∷ []
          )
          []
    in
    R.unify hole (R.def (quote isoToEquiv) [ varg iso ]) >>
    convertMacro al hole₁ >>
    convertMacro (flipAssoc al) hole₂

open Internal

macro
  -- ΣFormat → <Σ-Type> ≃ <RecordType>
  Σ≃Record : ΣFormat → R.Term → R.TC Unit
  Σ≃Record sig = equivMacro (ΣFormat→Assoc sig)

  -- ΣFormat → <RecordType> ≃ <Σ-Type>
  Record≃Σ : ΣFormat → R.Term → R.TC Unit
  Record≃Σ sig = equivMacro (flipAssoc (ΣFormat→Assoc sig))

  -- <RecordTypeName> → <Σ-Type> ≃ <RecordType>
  FlatΣ≃Record : R.Name → R.Term → R.TC Unit
  FlatΣ≃Record name hole =
    recordName→ΣFormat name >>= λ sig →
    equivMacro (MaybeΣFormat→Assoc sig) hole

  -- <RecordTypeName> → <RecordType> ≃ <Σ-Type>
  Record≃FlatΣ : R.Name → R.Term → R.TC Unit
  Record≃FlatΣ name hole =
    recordName→ΣFormat name >>= λ sig →
    equivMacro (flipAssoc (MaybeΣFormat→Assoc sig)) hole

  -- ΣFormat → <RecordType₁> ≃ <RecordType₂>
  Record≃Record : Assoc → R.Term → R.TC Unit
  Record≃Record = equivMacro

module Example where

  private
    variable
      ℓ ℓ' : Level
      A : Type ℓ
      B : A → Type ℓ'

  record Example {A : Type ℓ} (B : A → Type ℓ') : Type (ℓ-max ℓ ℓ') where
    field
      cool : A
      fun : A
      wow : B cool

  open Example

  {-
    Example: Equivalence between a Σ-type and record type using FlatΣ≃Record
  -}

  Example0 : (Σ[ a ∈ A ] Σ[ a' ∈ A ] B a) ≃ Example B
  Example0 = FlatΣ≃Record Example

  Example0' : Example B ≃ (Σ[ a ∈ A ] Σ[ a' ∈ A ] B a)
  Example0' = Record≃FlatΣ Example

  Example0'' : Unit ≃ Unit -- any record with no fields is equivalent to unit
  Example0'' = FlatΣ≃Record Unit

  {-
    Example: Equivalence between an arbitrarily arrange Σ-type and record type using Σ≃Record
  -}

  Example1 : (Σ[ p ∈ A × A ] B (p .snd)) ≃ Example B
  Example1 =
    Σ≃Record ((leaf (quote fun) , leaf (quote cool)) , leaf (quote wow))

  {-
    Example: Equivalence between arbitrary iterated record types (less convenient) using
    Record≃Record
  -}

  record Inner {A : Type ℓ} (B : A → Type ℓ') (a : A) : Type (ℓ-max ℓ ℓ') where
    field
      fun' : A
      wow' : B a

  record Outer {A : Type ℓ} (B : A → Type ℓ') : Type (ℓ-max ℓ ℓ') where
    field
      cool' : A
      inner : B cool'

  open Inner
  open Outer

  Example2 : Example B ≃ Outer (Inner B)
  Example2 =
    Record≃Record
      ( ([ quote cool ] , [ quote cool' ])
      ∷ ([ quote fun ] , (quote fun' ∷ quote inner ∷ []))
      ∷ ([ quote wow ] , (quote wow' ∷ quote inner ∷ []))
      ∷ []
      )

ext: agda

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

open import Categories.Category

open import Function
open import Relation.Binary.PropositionalEquality as ≡

Discrete : ∀ {a} (A : Set a) → Category a a a
Discrete A = record
  { Obj       = A
  ; _⇒_       = _≡_
  ; _≈_       = _≡_
  ; id        = refl
  ; _∘_       = flip ≡.trans
  ; assoc     = λ {_ _ _ _ g} → sym (trans-assoc g)
  ; sym-assoc = λ {_ _ _ _ g} → trans-assoc g
  ; identityˡ = λ {_ _ f} → trans-reflʳ f
  ; identityʳ = refl
  ; identity² = refl
  ; equiv     = isEquivalence
  ; ∘-resp-≈  = λ where
    refl refl → refl
  }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.ImplShared.Base.Types

open import LibraBFT.Abstract.Types.EpochConfig UID NodeId
open        EpochConfig
open import LibraBFT.Concrete.System
open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Util.Crypto
open import Optics.All
open import Util.Hash
open import Util.KVMap
open import Util.PKCS
open import Util.Prelude
open import Yasm.Base

-- This module contains definitions and proofs used by both the VotesOnce and PreferredRoundRule
-- proofs.

module LibraBFT.Concrete.Properties.Common (iiah : SystemInitAndHandlers ℓ-RoundManager ConcSysParms) (𝓔 : EpochConfig) where
 open        SystemTypeParameters ConcSysParms
 open        SystemInitAndHandlers iiah
 open        ParamsWithInitAndHandlers iiah
 open import LibraBFT.ImplShared.Util.HashCollisions iiah
 open import Yasm.Yasm ℓ-RoundManager ℓ-VSFP ConcSysParms iiah PeerCanSignForPK PeerCanSignForPK-stable

 record VoteForRound∈ (pk : PK)(round : ℕ)(epoch : ℕ)(bId : HashValue)(pool : SentMessages) : Set where
   constructor mkVoteForRound∈
   field
     msgWhole  : NetworkMsg
     msgVote   : Vote
     msg⊆      : msgVote ⊂Msg msgWhole
     msgSender : ℕ
     msg∈pool  : (msgSender , msgWhole) ∈ pool
     msgSigned : WithVerSig pk msgVote
     msgEpoch≡ : msgVote ^∙ vEpoch ≡ epoch
     msgRound≡ : msgVote ^∙ vRound ≡ round
     msgBId≡   : msgVote ^∙ vProposedId ≡ bId
 open VoteForRound∈ public

 ImplObl-bootstrapVotesRound≡0 : Set
 ImplObl-bootstrapVotesRound≡0 = ∀ {pk v}
                         → (wvs : WithVerSig pk v)
                         → ∈BootstrapInfo bootstrapInfo (ver-signature wvs)
                         → v ^∙ vRound ≡ 0

 ImplObl-bootstrapVotesConsistent : Set
 ImplObl-bootstrapVotesConsistent = (v1 v2 : Vote)
                             → ∈BootstrapInfo bootstrapInfo (_vSignature v1) → ∈BootstrapInfo bootstrapInfo (_vSignature v2)
                             → v1 ^∙ vProposedId ≡ v2 ^∙ vProposedId

 ImplObl-NewVoteRound≢0 : Set (ℓ+1 ℓ-RoundManager)
 ImplObl-NewVoteRound≢0 =
   ∀{pid s' outs pk}{pre : SystemState}
   → ReachableSystemState pre
   -- For any honest call to /handle/ or /init/,
   → (sps : StepPeerState pid (msgPool pre) (initialised pre) (peerStates pre pid) (s' , outs))
   → ∀{v m} → Meta-Honest-PK pk
   -- For signed every vote v of every outputted message
   → v ⊂Msg m → send m ∈ outs
   → (wvs : WithVerSig pk v)
   → (¬ ∈BootstrapInfo bootstrapInfo (ver-signature wvs))
   → v ^∙ vRound ≢ 0

 IncreasingRoundObligation : Set (ℓ+1 ℓ-RoundManager)
 IncreasingRoundObligation =
   ∀{pid pid' s' outs pk}{pre : SystemState}
   → ReachableSystemState pre
   -- For any honest call to /handle/ or /init/,
   → (sps : StepPeerState pid (msgPool pre) (initialised pre) (peerStates pre pid) (s' , outs))
   → ∀{v m v' m'} → Meta-Honest-PK pk
   -- For signed every vote v of every outputted message
   → v  ⊂Msg m → send m ∈ outs
   → (sig : WithVerSig pk v) → ¬ (∈BootstrapInfo bootstrapInfo (ver-signature sig))
   → ¬ (MsgWithSig∈ pk (ver-signature sig) (msgPool pre))
   → PeerCanSignForPK (StepPeer-post {pre = pre} (step-honest sps)) v pid pk
   -- And if there exists another v' that has been sent before
   → v' ⊂Msg m' → (pid' , m') ∈ (msgPool pre)
   → (sig' : WithVerSig pk v') → ¬ (∈BootstrapInfo bootstrapInfo (ver-signature sig'))
   -- If v and v' share the same epoch
   → v ^∙ vEpoch ≡ v' ^∙ vEpoch
   → v' ^∙ vRound < v ^∙ vRound
     ⊎ VoteForRound∈ pk (v ^∙ vRound) (v ^∙ vEpoch) (v ^∙ vProposedId) (msgPool pre)

 module ConcreteCommonProperties
        (st         : SystemState)
        (r          : ReachableSystemState st)
        (sps-corr   : StepPeerState-AllValidParts)
        (Impl-bsvr  : ImplObl-bootstrapVotesRound≡0)
        (Impl-nvr≢0 : ImplObl-NewVoteRound≢0)
   where

   open Structural sps-corr
   open PerReachableState r

   msgSentB4⇒VoteRound∈ : ∀ {v pk pool}
                         → (vv : WithVerSig pk v)
                         → (m : MsgWithSig∈ pk (ver-signature vv) pool)
                         → Σ (VoteForRound∈ pk (v ^∙ vRound) (v ^∙ vEpoch) (v ^∙ vProposedId) pool)
                             (λ v4r → ver-signature (msgSigned v4r) ≡ ver-signature vv)
   msgSentB4⇒VoteRound∈ {v} vv m
       with sameSig⇒sameVoteDataNoCol (msgSigned m) vv (msgSameSig m)
   ...| refl = mkVoteForRound∈ (msgWhole m) (msgPart m) (msg⊆ m) (msgSender m)
                                (msg∈pool m) (msgSigned m) refl refl refl , msgSameSig m

   VoteRound∈⇒msgSent : ∀ {round eid bid pk pool}
                      → (v4r : VoteForRound∈ pk round eid bid pool)
                      → Σ (MsgWithSig∈ pk (ver-signature $ msgSigned v4r) pool)
                          (λ mws → ( ver-signature (msgSigned mws) ≡ ver-signature (msgSigned v4r)
                                   × (msgPart mws) ^∙ vRound ≡ round))
   VoteRound∈⇒msgSent (mkVoteForRound∈ msgWhole₁ msgVote₁ msg⊆₁ msgSender₁ msg∈pool₁ msgSigned₁ msgEpoch≡₁ msgRound≡₁ msgBId≡₁)
           = mkMsgWithSig∈ msgWhole₁ msgVote₁ msg⊆₁ msgSender₁ msg∈pool₁ msgSigned₁ refl , refl , msgRound≡₁

    -- If a Vote signed for an honest PK has been sent, and it is not in bootstrapInfo, then
    -- it is for a round > 0
   NewVoteRound≢0 : ∀ {pk round epoch bId} {st : SystemState}
                     → ReachableSystemState st
                     → Meta-Honest-PK pk
                     → (v : VoteForRound∈ pk round epoch bId (msgPool st))
                     → ¬ ∈BootstrapInfo bootstrapInfo (ver-signature (msgSigned v))
                     → round ≢ 0
   NewVoteRound≢0 (step-s r (step-peer (step-honest stP))) pkH v ¬bootstrap r≡0
     with msgRound≡ v
   ...| refl
     with newMsg⊎msgSentB4 r stP pkH (msgSigned v) ¬bootstrap (msg⊆ v) (msg∈pool v)
   ...| Left (m∈outs , _ , _) = ⊥-elim (Impl-nvr≢0 r stP pkH (msg⊆ v) m∈outs
                                                    (msgSigned v) ¬bootstrap r≡0)
   ...| Right m
      with msgSameSig m
   ...| refl
      with sameSig⇒sameVoteDataNoCol (msgSigned m) (msgSigned v) (msgSameSig m)
   ...| refl = let vsb4 = mkVoteForRound∈ (msgWhole m) (msgPart m) (msg⊆ m) (msgSender m)
                                          (msg∈pool m) (msgSigned m) refl refl refl
               in ⊥-elim (NewVoteRound≢0 r pkH vsb4 ¬bootstrap r≡0)
   NewVoteRound≢0 (step-s r (step-peer cheat@(step-cheat c))) pkH v ¬bootstrap r≡0
     with ¬cheatForgeNewSig r cheat unit pkH (msgSigned v) (msg⊆ v) (msg∈pool v) ¬bootstrap
   ...| m
     with msgSameSig m
   ...| refl
      with sameSig⇒sameVoteDataNoCol (msgSigned m) (msgSigned v) (msgSameSig m)
   ...| refl = let vsb4 = mkVoteForRound∈ (msgWhole m) (msgPart m) (msg⊆ m) (msgSender m)
                                       (msg∈pool m) (msgSigned m) refl refl refl
               in ⊥-elim (NewVoteRound≢0 r pkH vsb4 ¬bootstrap (trans (msgRound≡ v) r≡0))

   ¬Bootstrap∧Round≡⇒¬Bootstrap : ∀ {v pk round epoch bId} {st : SystemState}
                     → ReachableSystemState st
                     → Meta-Honest-PK pk
                     → (vfr : VoteForRound∈ pk round epoch bId (msgPool st))
                     → ¬ (∈BootstrapInfo bootstrapInfo (ver-signature (msgSigned vfr)))
                     → (sig : WithVerSig pk v)
                     → v ^∙ vRound ≡ round
                     → ¬ (∈BootstrapInfo bootstrapInfo (ver-signature sig))
   ¬Bootstrap∧Round≡⇒¬Bootstrap r pkH v₁ ¬bootstrapV₁ sigV₂ refl bootstrapV₂
     = let v₁r≢0 = NewVoteRound≢0 r pkH v₁ ¬bootstrapV₁
       in ⊥-elim (v₁r≢0 (Impl-bsvr sigV₂ bootstrapV₂))


text:
module Issue249 where

postulate
  A B : Set

module A where
  X = A
  Y = B

open A renaming (X to C; Y to C)

-- open A using (X) renaming (Y to X)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Relator.Equals where

open import Logic
import      Lvl
open import Type
open import Type.Cubical
open import Type.Cubical.Path
open import Type.Cubical.Path.Proofs

infix 15 _≡_

_≡_ = Path

-- _≢_ : ∀{ℓ}{T} → T → T → Stmt{ℓ}
-- _≢_ a b = ¬(a ≡ b)

{-# BUILTIN REWRITE  _≡_ #-}

data Id {ℓ}{T : Type{ℓ}} : T → T → Stmt{ℓ} where
  instance intro : ∀{x : T} → (Id x x)

{-# BUILTIN EQUALITY Id #-}

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 --type-in-type #-}
open import Data.Empty
open import Data.Unit
open import Data.Bool hiding ( T )
open import Data.Product hiding ( curry ; uncurry )
open import Data.Nat
open import Data.String
open import Relation.Binary.PropositionalEquality using ( refl ; _≢_ ; _≡_ )
open import Function
module ClosedTheory2 where

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

data Tel : Set₁ where
  Emp : Tel
  Ext : (A : Set) (B : A → Tel) → Tel

Scope : Tel → Set
Scope Emp = ⊤
Scope (Ext A B) = Σ A λ a → Scope (B a)

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

UncurriedScope : (T : Tel) (X : Scope T → Set) → Set
UncurriedScope T X = (xs : Scope T) → X xs

CurriedScope : (T : Tel) (X : Scope T → Set) → Set
CurriedScope Emp X = X tt
CurriedScope (Ext A B) X = (a : A) → CurriedScope (B a) (λ b → X (a , b))

curryScope : (T : Tel) (X : Scope T → Set) → UncurriedScope T X → CurriedScope T X
curryScope Emp X f = f tt
curryScope (Ext A B) X f a = curryScope (B a) (λ b → X (a , b)) (λ b → f (a , b))

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

data Desc (I : Set) : Set₁ where
  End : (i : I) → Desc I
  Rec : (i : I) (D : Desc I) → Desc I
  Arg : (A : Set) (B : A → Desc I) → Desc I

ISet : Set → Set₁
ISet I = I → Set

El : {I : Set} (D : Desc I) → ISet I → ISet I
El (End j) X i = j ≡ i
El (Rec j D) X i = X j × El D X i
El (Arg A B) X i = Σ A (λ a → El (B a) X i)

data μ {I : Set} (D : Desc I) (i : I) : Set where
  init : El D (μ D) i → μ D i

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

UncurriedEl : {I : Set} (D : Desc I) (X : ISet I) → Set
UncurriedEl D X = ∀{i} → El D X i → X i

CurriedEl : {I : Set} (D : Desc I) (X : ISet I) → Set
CurriedEl (End i) X = X i
CurriedEl (Rec i D) X = (x : X i) → CurriedEl D X
CurriedEl (Arg A B) X = (a : A) → CurriedEl (B a) X

curryEl : {I : Set} (D : Desc I) (X : ISet I)
  → UncurriedEl D X → CurriedEl D X
curryEl (End i) X cn = cn refl
curryEl (Rec i D) X cn = λ x → curryEl D X (λ xs → cn (x , xs))
curryEl (Arg A B) X cn = λ a → curryEl (B a) X (λ xs → cn (a , xs))

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

record Data : Set₁ where
  field
    E : Set
    P : Tel
    I : Scope P → Tel
    C : (p : Scope P) (t : E) → Desc (Scope (I p))

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

  UncurriedFormer : Set
  UncurriedFormer =
    UncurriedScope P λ p
    → UncurriedScope (I p) λ i
    → Set

  FormUncurried : UncurriedFormer
  FormUncurried p = μ (Arg E (C p))

  Former : Set
  Former = CurriedScope P λ p → CurriedScope (I p) λ i → Set

  Form : Former
  Form =
    curryScope P (λ p → CurriedScope (I p) λ i → Set) λ p →
    curryScope (I p) (λ i → Set) λ i →
    FormUncurried p i

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

  InjUncurried : E → Set
  InjUncurried t = UncurriedScope P λ p → CurriedEl (C p t ) (FormUncurried p)

  injUncurried : (t : E) → InjUncurried t
  injUncurried t p = curryEl (C p t)
    (FormUncurried p)
    (λ xs → init (t , xs))

  Inj : E → Set
  Inj t = CurriedScope P λ p → CurriedEl (C p t) (FormUncurried p)

  inj : (t : E) → Inj t
  inj t = curryScope P
    (λ p → CurriedEl (C p t) (FormUncurried p))
    (injUncurried t)

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

open Data using ( Former ; Form ; Inj ; inj )

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

data VecT : Set where
  nilT consT : VecT

VecR : Data
VecR = record {
    E = VecT
  ; P = Ext Set λ _ → Emp
  ; I = λ _ → Ext ℕ λ _ → Emp
  ; C = λ { (A , tt) → λ
    { nilT → End (zero , tt)
    ; consT → Arg ℕ λ n → Arg A λ _
            → Rec (n , tt)
            $ End (suc n , tt)
    } }
  }

Vec : (A : Set) → ℕ → Set
Vec = Form VecR

nil : (A : Set) → Vec A zero
nil = inj VecR nilT

cons : (A : Set) (n : ℕ) (x : A) (xs : Vec A n) → Vec A (suc n)
cons = inj VecR consT

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

data TreeT : Set where
  leaf₁T leaf₂T branchT : TreeT

TreeR : Data
TreeR = record {
    E = TreeT
  ; P = Ext Set λ _ → Ext Set λ _ → Emp
  ; I = λ _ → Ext ℕ λ _ → Ext ℕ λ _ → Emp
  ; C = λ { (A , B , tt) → λ
    { leaf₁T → Arg A λ _ → End (suc zero , zero , tt)
    ; leaf₂T → Arg B λ _ → End (zero , suc zero , tt)
    ; branchT
      → Arg ℕ λ m → Arg ℕ λ n
      → Arg ℕ λ x → Arg ℕ λ y
      → Rec (m , n , tt) $ Rec (x , y , tt)
      $ End (m + x , n + y , tt)
    } }
  }

Tree : (A B : Set) (m n : ℕ) → Set
Tree = Form TreeR

leaf₁ : (A B : Set) → A → Tree A B (suc zero) zero
leaf₁ = inj TreeR leaf₁T

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

max_stars_repo_name: larrytheliquid/generic-elim

max_issues_repo_name: larrytheliquid/generic-elim

max_forks_repo_name: larrytheliquid/generic-elim


text:
------------------------------------------------------------------------
-- A README directed towards readers of the paper
-- "Correct-by-Construction Pretty-Printing"
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

{-# OPTIONS --guardedness #-}

module README.Correct-by-Construction-Pretty-Printing where

------------------------------------------------------------------------
-- 2: Grammars

-- The basic grammar data type, including its semantics. Only a small
-- number of derived combinators is defined directly for this data
-- type. It is proved that an inductive version of this type would be
-- quite restrictive.

import Grammar.Infinite.Basic

-- The extended grammar data type mentioned in Section 4.3, along with
-- a semantics and lots of derived combinators. This type is proved to
-- be no more expressive than the previous one; but it is also proved
-- that every language that can be recursively enumerated can be
-- represented by a (unit-valued) grammar.

import Grammar.Infinite

------------------------------------------------------------------------
-- 3: Pretty-Printers

import Pretty

------------------------------------------------------------------------
-- 4: Examples

-- Reusable document combinators introduced in this section.

import Pretty

-- The symbol combinator and the heuristic procedure
-- trailing-whitespace.

import Grammar.Infinite

-- 4.1: Boolean literals.

import Examples.Bool

-- 4.2: Expressions, and 4.3: Expressions, Take Two.

import Examples.Expression

-- 4.4: Identifiers.

import Examples.Identifier

-- 4.5: Other Examples.

-- Some of these examples are not mentioned in the paper.

-- Another expression example based on one in Matsuda and Wang's
-- "FliPpr: A Prettier Invertible Printing System".

import Examples.Expression

-- An example based on one in Swierstra and Chitil's "Linear, bounded,
-- functional pretty-printing".

import Examples.Identifier-list

-- Two examples, both based on examples in Wadler's "A prettier
-- printer".

import Examples.Tree
import Examples.XML

-- The fill combinator.

import Pretty

-- A general grammar and pretty-printer for binary operators of
-- various (not necessarily linearly ordered) precedences.

import Examples.Precedence

------------------------------------------------------------------------
-- 5: Renderers

import Renderer

-- Unambiguous and Parser.

import Grammar.Infinite

max_stars_repo_name: nad/pretty

max_issues_repo_name: nad/pretty

max_forks_repo_name: nad/pretty


text:
module HC-Lec2 where

open import HC-Lec1

-- ==============================================================================
-- Lecture 4 : Sigma, Difference, Vector Take
-- https://www.youtube.com/watch?v=OZeDRtRmgkw

-- 43:14

data Vec (X : Set) : Nat -> Set where
  []   :                              Vec X  zero
  _::_ : {n : Nat} -> X -> Vec X n -> Vec X (suc n)
infixr 4 _::_

vTake : (m n : Nat) -> m >= n -> {X : Set} -> Vec X m -> Vec X n
vTake      m   zero   m>=n       xs  = []
vTake (suc m) (suc n) m>=n (x :: xs) = x :: vTake m n m>=n xs

vTake32 : Set
vTake32 = vTake 3 2 <> (1 :: 2 :: 3 :: []) == (1 :: 2 :: [])

-- 47:35 : taking ALL elements is an identity
vTakeIdFact : (n : Nat) {X : Set} (xs : Vec X n)
           -> vTake n n (refl->= n) xs == xs
vTakeIdFact .0             [] = refl []
vTakeIdFact (suc n) (x :: xs) rewrite vTakeIdFact n xs = refl (x :: xs)

-- 48:17 : taking p elements from Vm is same as taking n elements from Vm, forming Vn
--         then taking p elments from Vn
vTakeCpFact : (m n p : Nat) (m>=n : m >= n) (n>=p : n >= p) {X : Set} (xs : Vec X m)
           -> vTake m p (trans->= m n p m>=n n>=p)                 xs
           == vTake n p                      n>=p  (vTake m n m>=n xs)
vTakeCpFact      m       n   zero   m>=n n>=p _ = refl []
vTakeCpFact (suc m) (suc n) (suc p) m>=n n>=p (x :: xs)
  rewrite vTakeCpFact  m n p m>=n n>=p xs
  = refl (x :: (vTake n p n>=p (vTake m n m>=n xs)))

-- 48:54
-- vTakeIdFact : reflexivity  turns into identity
-- vTakeCpFact : transitivity turns into composition

-- ==============================================================================
-- Lecture 5 : How Rewrite Works
-- https://www.youtube.com/watch?v=b5salYMZoyM

-- 3:34
vTake53 : Vec Nat 3
vTake53 = vTake 5 3 <> (1 :: 2 :: 3 :: 4 :: 5 :: [])

-- 5:30
vTake' : ∀ {m : Nat} {X : Set}
      -> (n : Nat) -> m >= n -> Vec X m
      -> Vec X n
vTake'     {m}  zero   m>=n       xs  = []
vTake' {suc m} (suc n) m>=n (x :: xs) = x :: vTake' {m} n m>=n xs

{-
-- 7:45
rigid symbols : constructors (value and type)
- if you are trying to tell if two usages of constructors match each other,
  you can compare them component-wise
- no defined computational meaning - they are what they are
- e.g., Vec Nat 3
non-rigid
- e.g., >=
- can compute

-- 15:48
vTake : think of as turning a '>=' proof into a vector operation.
- In comes a proof on numbers, out comes an operation on vectors.
vTakeIdFact : identity proof on numbers turns into identity operation on vectors
vTakeCpFact : proof of transitivity on numbers turns into composition operation on vectors

-- 24:08 : best practice : use record (instead of data) when possible : agda is more aggressive

-- 24:28 : HOW REWRITE WORKS
Rewrite is shorthand for
- abstract the LHS   of the equation using 'with'
- abstract the proof of the equation using 'with'
- then pattern matching on the proof
-}

------------------------------------------------------------------------------
-- Splittings (which bear some relationship to <= from ex1)
-- 39:00

data _<[_]>_ : Nat -> Nat -> Nat -> Set where
  zzz : zero <[ zero ]> zero

  lll : {l m r : Nat} ->     l <[     m ]>     r
                      -> suc l <[ suc m ]>     r

  rrr : {l m r : Nat} ->     l <[     m ]>     r
                      ->     l <[ suc m ]> suc r

-- xzzz : Set
-- xzzz = zero <[ zero ]> zero

-- x1z1 : Set
-- x1z1 = 1 <[ zero ]> 1

-- x159 : Set
-- x159 = 1 <[ 5 ]> 9

-- x951 : Set
-- x951 = 9 <[ 5 ]> 1

-- 41:08
-- combine two vectors into one according to given instructions

-- this is kind of a "double-sided" '<='
{-        collection
              * <--- *
       * ---> *
       * ---> *
              * <--- *
       * ---> *
 3 from left     2 from right
-}
_>[_]<_ : {X : Set} {l m r : Nat}
       ->     Vec X l
       ->           l <[ m ]>       r -- instructions
             ->               Vec X r
       ->          Vec X m
-- why is rrr the first line?
-- 29:49 https://www.youtube.com/watch?v=RW4aC_6n0yQ
-- do NOT pattern match on vector first (LHS of first clause)
-- pattern match on instructions first
-- i.e., no pattern match on xl, so goes to try to match instruction : >[ rrr mmm ]<
xl        >[ rrr mmm ]< (x :: xr) = x :: (xl >[ mmm ]< xr)
(x :: xl) >[ lll mmm ]<       xr  = x :: (xl >[ mmm ]< xr)
[]        >[ zzz     ]<       []  = []

v6rl : Vec Nat 6
v6rl = (0 :: 2 :: 3 :: []) >[ rrr (rrr (rrr (lll (lll (lll zzz))))) ]< (7 :: 8 :: 9 :: [])

_ : v6rl == (7 :: 8 :: 9 :: 0 :: 2 :: 3 :: [])
_ = refl    (7 :: 8 :: 9 :: 0 :: 2 :: 3 :: [])

v6   : Vec Nat 6
v6   = (0 :: 2 :: 3 :: []) >[ lll (rrr (lll (rrr (lll (rrr zzz))))) ]< (7 :: 8 :: 9 :: [])

_ : v6 == (0 :: 7 :: 2 :: 8 :: 3 :: 9 :: [])
_ = refl  (0 :: 7 :: 2 :: 8 :: 3 :: 9 :: [])

-- 44:27

-- split a vector into two vectors according to given instructions
-- reverses '<[ m ]>' - instructions for taking things apart
data FindSplit {X : Set} {l m r : Nat}
     (nnn : l <[ m ]> r) : (xs : Vec X m) -> Set where
  splitBits : (xl : Vec X l) (xr : Vec X r) -> FindSplit nnn (xl >[ nnn ]< xr)

-- proves FindSplit
findSplit : {X : Set} {l m r : Nat} (nnn : l <[ m ]> r) (xs : Vec X m) -> FindSplit nnn xs

findSplit  zzz      [] = splitBits [] []

findSplit (lll nnn) (x :: xs) with findSplit nnn xs
                                           -- FindSplit (lll nnn) (x :: (xl >[ nnn ]< xr))
findSplit (lll nnn) (x :: .(xl >[ nnn ]< xr)) | splitBits xl xr = splitBits (x :: xl) xr

findSplit (rrr nnn) (x :: xs) with findSplit nnn xs
                                           -- FindSplit (rrr nnn) (x :: (xl >[ nnn ]< xr))
findSplit (rrr nnn) (x :: .(xl >[ nnn ]< xr)) | splitBits xl xr = splitBits xl (x :: xr)

-- ==============================================================================
-- https://www.youtube.com/watch?v=RW4aC_6n0yQ

-- 5:08
{-
The o' <= constructor : you can keep increasing the RHS

  oz -- stop
  os -- take this one and keep going
  o' -- skip this one and keep going

Tabulating the ways of choosing N things from M things
A path is a way to get a specific embedding.
The numbers in parenthesis shows the number of paths to a specific embedding (Pascal's triangle).

                                     oz
                                    0<=0
                                    (1)
                                   /    \
                                 /        \
                               /            \
                             o'              os
                          0<=1                1<=1
                          (1)                 (1)
                         /    \              /    \
                       /        \          /        \
                     /            \      /            \
                   o'              os   o'             os
                  0<=2              1<=2              2<=2
                  (1)               (2)               (2)
                 /    \            /    \            /    \
               /        \        /        \        /        \
             /            \     /           \    /            \
           o'              os  o'           os  o'             os
          0<=3              1<=3             2<=3             3<=3
          (1)               (3)              (3)              (1)

witnesses to M choose N
read a value in a set of this type as instructions for choosing
-}

-- 14:58
-- 'findSplit' (above)
-- 23:20
-- last clause of 'findSplit'
-- 29:49 : the same ERROR I had before changing order of clauses in _>[_]<_
-- 34:22 : rule of thumb
-- if there is one column of args, where on every line is a constructor then no change
-- otherwise, choose ordering carefully
-- 35:52 : final order of clauses of of  _>[_]<_ -- tidy to have nil case at top or bottom
-- 40:15 shows how agda/haskell does case splitting on _>[_]<_

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
module Generic.Main where

open import Generic.Core                public
open import Generic.Function.FoldMono   public
open import Generic.Property.Eq         public
open import Generic.Reflection.ReadData public
open import Generic.Reflection.DeriveEq public

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
{-# OPTIONS --universe-polymorphism #-}

module Issue441 where

open import Common.Level

postulate
  C : ∀ ℓ → Set ℓ → Set ℓ
  I : ∀ a b (A : Set a) (B : Set b) → (A → B) → B → Set (a ⊔ b)
  E : ∀ a b (A : Set a) → (A → Set b) → Set (a ⊔ b)
  c : ∀ a (A : Set a) → ((B : A → Set a) → E a a A B) → C a A

foo : (∀ a b (A : Set a) (B : A → Set b) → E a b A B) →
      ∀ a b (A : Set a) (B : Set b) (f : A → B) x →
      C (a ⊔ b) (I a b A B f x)
foo e a b A B f x = c _ _ (λ B′ → e _ _ _ _)

infix 4 _≡_

data _≡_ {a} {A : Set a} : A → A → Set a where
  refl : ∀ x → x ≡ x

elim : ∀ {a p} {A : Set a} (P : {x y : A} → x ≡ y → Set p) →
       (∀ x → P (refl x)) →
       ∀ {x y} (x≡y : x ≡ y) → P x≡y
elim P r (refl x) = r _

cong : ∀ {a b} {A : Set a} {B : Set b}
       (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
cong f (refl x) = refl (f x)

bar : ∀ {a} {A : Set a} {x y : A}
      (x≡y : x ≡ y) (f : x ≡ y → x ≡ y) →
      f x≡y ≡ f x≡y
bar = elim (λ {x} {y} x≡y → (f : x ≡ y → x ≡ y) → f x≡y ≡ f x≡y)
           (λ x f → cong {a = _} {b = _} f (refl (refl x)))

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module 00-preamble where

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

UU : (i : Level) → Set (lsuc i)
UU i = Set i

max_stars_repo_name: hemangandhi/HoTT-Intro

max_issues_repo_name: hemangandhi/HoTT-Intro

max_forks_repo_name: hemangandhi/HoTT-Intro


text:
module Everything where

open import Oscar.Prelude public

-- meta-class
open import Oscar.Class public

-- classes
open import Oscar.Class.Amgu                                        public
open import Oscar.Class.Apply                                       public
open import Oscar.Class.Bind                                        public
open import Oscar.Class.Category                                    public
open import Oscar.Class.Congruity                                   public
open import Oscar.Class.Fmap                                        public
open import Oscar.Class.Functor                                     public
open import Oscar.Class.HasEquivalence                              public
open import Oscar.Class.Hmap                                        public
open import Oscar.Class.Injectivity                                 public
open import Oscar.Class.IsCategory                                  public
open import Oscar.Class.IsDecidable                                 public
open import Oscar.Class.IsEquivalence                               public
open import Oscar.Class.IsFunctor                                   public
open import Oscar.Class.IsPrecategory                               public
open import Oscar.Class.IsPrefunctor                                public
open import Oscar.Class.Leftstar                                    public
open import Oscar.Class.Leftunit                                    public
open import Oscar.Class.Map                                         public
open import Oscar.Class.Precategory                                 public
open import Oscar.Class.Prefunctor                                  public
open import Oscar.Class.Properthing                                 public
open import Oscar.Class.Pure                                        public
open import Oscar.Class.Quadricity                                  public
open import Oscar.Class.Reflexivity                                 public
open import Oscar.Class.Setoid                                      public
open import Oscar.Class.Similarity                                  public
open import Oscar.Class.SimilarityM                                 public
open import Oscar.Class.SimilaritySingleton                         public
open import Oscar.Class.Smap                                        public
open import Oscar.Class.Smapoid                                     public
open import Oscar.Class.Successor₀                                  public
open import Oscar.Class.Successor₁                                  public
open import Oscar.Class.Surjection                                  public
open import Oscar.Class.Surjextensionality                          public
open import Oscar.Class.Surjidentity                                public
open import Oscar.Class.Surjtranscommutativity                      public
open import Oscar.Class.Symmetrical                                 public
open import Oscar.Class.Symmetry                                    public
open import Oscar.Class.Thickandthin                                public
open import Oscar.Class.Transassociativity                          public
open import Oscar.Class.Transextensionality                         public
open import Oscar.Class.Transitivity                                public
open import Oscar.Class.Transleftidentity                           public
open import Oscar.Class.Transrightidentity                          public
open import Oscar.Class.Unit                                        public
open import Oscar.Class.[ExtensibleType]                            public
open import Oscar.Class.[IsExtensionB]                              public

-- individual instances
open import Oscar.Class.Amgu.Term∃SubstitistMaybe                   public
open import Oscar.Class.Congruity.Proposequality                    public
open import Oscar.Class.Congruity.Proposextensequality              public
open import Oscar.Class.HasEquivalence.ExtensionṖroperty            public
open import Oscar.Class.HasEquivalence.Ṗroperty                     public
open import Oscar.Class.HasEquivalence.Substitunction               public
open import Oscar.Class.Hmap.Transleftidentity                      public
open import Oscar.Class.Injectivity.Vec                             public
open import Oscar.Class.IsDecidable.Fin                             public
open import Oscar.Class.IsDecidable.¶                               public
open import Oscar.Class.Properthing.ExtensionṖroperty               public
open import Oscar.Class.Properthing.Ṗroperty                        public
open import Oscar.Class.Reflexivity.Function                        public
open import Oscar.Class.Smap.ExtensionFinExtensionTerm              public
open import Oscar.Class.Smap.ExtensionṖroperty                      public
open import Oscar.Class.Smap.TransitiveExtensionLeftṖroperty        public
open import Oscar.Class.Surjection.⋆                                public
open import Oscar.Class.Symmetrical.ExtensionalUnifies              public
open import Oscar.Class.Symmetrical.Symmetry                        public
open import Oscar.Class.Symmetrical.Unifies                         public
open import Oscar.Class.Transextensionality.Proposequality          public
open import Oscar.Class.Transitivity.Function                       public
open import Oscar.Class.[ExtensibleType].Proposequality             public

-- instance bundles
open import Oscar.Property.Category.AListProposequality                                         public
open import Oscar.Property.Category.ExtensionProposextensequality                               public
open import Oscar.Property.Category.Function                                                    public
open import Oscar.Property.Functor.SubstitistProposequalitySubstitunctionProposextensequality   public
open import Oscar.Property.Functor.SubstitunctionExtensionTerm                                  public
open import Oscar.Property.Monad.Maybe                                                          public
open import Oscar.Property.Propergroup.Substitunction                                           public
open import Oscar.Property.Setoid.ProductIndexEquivalence                                       public
open import Oscar.Property.Setoid.Proposequality                                                public
open import Oscar.Property.Setoid.Proposextensequality                                          public
open import Oscar.Property.Setoid.ṖropertyEquivalence                                           public
open import Oscar.Property.Thickandthin.FinFinProposequalityMaybeProposequality                 public
open import Oscar.Property.Thickandthin.FinTermProposequalityMaybeProposequality                public

-- data
open import Oscar.Data.Constraint                        public
open import Oscar.Data.Decidable                         public
open import Oscar.Data.Descender                         public
open import Oscar.Data.ExtensionṖroperty                 public
open import Oscar.Data.Fin                               public
open import Oscar.Data.List                              public
open import Oscar.Data.Maybe                             public
open import Oscar.Data.ProductIndexEquivalence           public
open import Oscar.Data.ProperlyExtensionNothing          public
open import Oscar.Data.Proposequality                    public
open import Oscar.Data.ṖropertyEquivalence               public
open import Oscar.Data.Substitist                        public
open import Oscar.Data.Substitunction                    public
open import Oscar.Data.Surjcollation                     public
open import Oscar.Data.Surjextenscollation               public
open import Oscar.Data.Term                              public
open import Oscar.Data.Vec                               public
open import Oscar.Data.¶                                 public
open import Oscar.Data.𝟘                                 public
open import Oscar.Data.𝟙                                 public
open import Oscar.Data.𝟚                                 public

-- class derivations
open import Oscar.Class.Leftunit.ToUnit                  public
open import Oscar.Class.Symmetry.ToSym                   public
open import Oscar.Class.Transleftidentity.ToLeftunit     public


text:
open import Relation.Nullary.Decidable using (False; map)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym; cong; module ≡-Reasoning)
open ≡-Reasoning
open import Function.Equivalence as FE using ()

open import Data.Unit using (⊤; tt)
open import Agda.Builtin.FromNat using (Number)

module AKS.Modular.Quotient.Base where

open import AKS.Nat using (ℕ; zero; suc; _<_; _∸_) renaming (_+_ to _+ℕ_; _*_ to _*ℕ_; _≟_ to _≟ℕ_)
open import AKS.Nat using (≢⇒¬≟; ∸-mono-<ʳ; 0<1+n; <⇒≤; <-irrelevant; 0≢⇒0<)
open import AKS.Nat.Divisibility using (_%_; n%m<m; 0%m≡0; 1%m≡1; [m+kn]%n≡m%n; m%n%n≡m%n; %-distribˡ-+; %-distribˡ-*)
open import AKS.Nat.GCD using (+ʳ; +ˡ)
open import AKS.Primality using (IsPrime; Prime; prime≢0; bézout-prime)
open Prime

record ℤ/[_] (P : Prime) : Set where
  constructor ℤ✓
  field
    mod : ℕ
    mod<p : mod < prime P
open ℤ/[_] public

module Operations {P : Prime} where
  open Prime P using () renaming (prime to p; isPrime to p-isPrime)
  open IsPrime p-isPrime using (1<p)

  p≢0 : False (p ≟ℕ 0)
  p≢0 = ≢⇒¬≟ (prime≢0 p-isPrime)

  [_] : ℕ → ℤ/[ P ]
  [ n ] = ℤ✓ ((n % p) {p≢0}) (n%m<m n p)

  instance
    ℤ/[]-number : Number (ℤ/[ P ])
    ℤ/[]-number = record
      { Constraint = λ _ → ⊤
      ; fromNat = λ n → [ n ]
      }

  infixl 6 _+_
  _+_ : ℤ/[ P ] → ℤ/[ P ] → ℤ/[ P ]
  n + m = [ mod n +ℕ mod m ]

  infix 8 -_
  -_ : ℤ/[ P ] → ℤ/[ P ]
  - (ℤ✓ zero    0<p) = ℤ✓ zero  0<p
  - (ℤ✓ (suc n) 1+n<p) = ℤ✓ (p ∸ suc n) (∸-mono-<ʳ (<⇒≤ 1+n<p) 0<1+n)

  infixl 7 _*_
  _*_ : ℤ/[ P ] → ℤ/[ P ] → ℤ/[ P ]
  n * m = [ mod n *ℕ mod m ]

  ℤ/[]-irrelevance : ∀ {x y : ℤ/[ P ]} → mod x ≡ mod y → x ≡ y
  ℤ/[]-irrelevance {ℤ✓ mod[x] mod[x]<p} {ℤ✓ .mod[x] mod[y]<p} refl = cong (λ z<p → ℤ✓ mod[x] z<p) (<-irrelevant mod[x]<p mod[y]<p)

  n≢0⇒mod[n]≢0 : ∀ {n} → n ≢ 0 → mod n ≢ 0
  n≢0⇒mod[n]≢0 {ℤ✓ zero _} n≢0 = contradiction (ℤ/[]-irrelevance (sym (0%m≡0 p))) n≢0
  n≢0⇒mod[n]≢0 {ℤ✓ (suc n) _} n≢0 = λ ()

  bézout-x∤p : ∀ n x y → 1 +ℕ x *ℕ n ≡ y *ℕ p → 0 ≢ (x % p) {p≢0}
  bézout-x∤p n x y 1+x*n≡y*p 0≡x%p = contradiction 1≡0 (λ ())
    where
    1≡0 : 1 ≡ zero
    1≡0 = begin
      1 ≡⟨ sym (1%m≡1 1<p) ⟩
      (1 +ℕ 0 *ℕ n) % p ≡⟨ cong (λ t → ((1 +ℕ t *ℕ n) % p) {p≢0}) 0≡x%p ⟩
      (1 +ℕ (x % p) *ℕ n) % p ≡⟨ %-distribˡ-+ 1 ((x % p) *ℕ n) p ⟩
      (1 % p +ℕ ((x % p) *ℕ n) % p) % p ≡⟨ cong (λ t → ((1 % p +ℕ t) % p) {p≢0}) (%-distribˡ-* (x % p) n p) ⟩
      (1 % p +ℕ ((x % p % p) *ℕ (n % p)) % p) % p ≡⟨ cong (λ t → (1 % p +ℕ (t *ℕ (n % p)) % p) % p) (m%n%n≡m%n x p) ⟩
      (1 % p +ℕ ((x % p) *ℕ (n % p)) % p) % p ≡⟨ cong (λ t → (1 % p +ℕ t) % p) (sym (%-distribˡ-* x n p)) ⟩
      (1 % p +ℕ (x *ℕ n) % p) % p ≡⟨ sym (%-distribˡ-+ 1 (x *ℕ n) p) ⟩
      (1 +ℕ x *ℕ n) % p ≡⟨ cong (λ t → (t % p) {p≢0}) 1+x*n≡y*p ⟩
      (y *ℕ p) % p ≡⟨ [m+kn]%n≡m%n 0 y p {p≢0} ⟩
      0 % p ≡⟨ 0%m≡0 p ⟩
      0 ∎

  -- x⁻¹ * x - 1 ≡ z * p
  infix 8 _⁻¹
  _⁻¹ : ∀ (n : ℤ/[ P ]) {n≢0 : n ≢ 0} → ℤ/[ P ]
  (n ⁻¹) {n≢0} with bézout-prime (mod n) p (n≢0⇒mod[n]≢0 n≢0) (mod<p n) p-isPrime
  ... | +ʳ x y 1+x*n≡y*p = ℤ✓ (p ∸ (x % p) {p≢0}) (∸-mono-<ʳ (<⇒≤ (n%m<m x p)) (0≢⇒0< (bézout-x∤p (mod n) x y 1+x*n≡y*p)))
  ... | +ˡ x y 1+y*p≡x*n = [ x ]

  infixl 7 _/_
  _/_ : ∀ (n m : ℤ/[ P ]) {m≢0 : m ≢ 0} → ℤ/[ P ]
  (n / m) {m≢0} = n * (m ⁻¹) {m≢0}

  _≟_ : Decidable {A = ℤ/[ P ]} _≡_
  ℤ✓ x x<p ≟ ℤ✓ y y<p = map (FE.equivalence ℤ/[]-irrelevance (λ { refl → refl })) (x ≟ℕ y)

open Operations public

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
-- Jesper, 2016-11-04
-- Absurd patterns should *not* be counted as a UnusedArg.

open import Common.Equality

data ⊥ : Set where

data Bool : Set where
  true false : Bool

abort : (A : Set) → ⊥ → A
abort A ()

test : (x y : ⊥) → abort Bool x ≡ abort Bool y
test x y = refl


text:
postulate
  [_…_] : Set → Set → Set


text:
module Issue1494.Helper where

record Record : Set₁ where
  field _≡_ : {A : Set} → A → A → Set

module Module (r : Record) where

  open Record r public


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

module Categories.Category.Finite.Fin.Instance.Span where

open import Data.Nat using (ℕ)
open import Data.Fin
open import Data.Fin.Patterns
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)

open import Categories.Category.Finite.Fin
open import Categories.Category
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.NaturalTransformation using (ntHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_)
open import Categories.Adjoint.Equivalence using (_⊣⊢_; ⊣Equivalence; withZig)
import Categories.Morphism as Mor
import Categories.Category.Instance.Span as Sp

private
  variable
    a b c d : Fin 3

-- The diagram is the following:
--
-- 1 <------- 0 -------> 2
--
SpanShape : FinCatShape
SpanShape = record
  { size     = 3
  ; ∣_⇒_∣    = morph
  ; hasShape = record
    { id        = id
    ; _∘_       = _∘_
    ; assoc     = assoc
    ; identityˡ = identityˡ
    ; identityʳ = identityʳ
    }
  }
  where morph : Fin 3 → Fin 3 → ℕ
        morph 0F 0F = 1
        morph 0F 1F = 1
        morph 0F 2F = 1
        morph 1F 1F = 1
        morph 2F 2F = 1
        morph _ _   = 0

        id : Fin (morph a a)
        id {0F} = 0F
        id {1F} = 0F
        id {2F} = 0F

        _∘_ : ∀ {a b c} → Fin (morph b c) → Fin (morph a b) → Fin (morph a c)
        _∘_ {0F} {0F} {0F} 0F 0F = 0F
        _∘_ {0F} {0F} {1F} 0F 0F = 0F
        _∘_ {0F} {0F} {2F} 0F 0F = 0F
        _∘_ {0F} {1F} {1F} 0F 0F = 0F
        _∘_ {0F} {2F} {2F} 0F 0F = 0F
        _∘_ {1F} {1F} {1F} 0F 0F = 0F
        _∘_ {2F} {2F} {2F} 0F 0F = 0F

        assoc : ∀ {f : Fin (morph a b)} {g : Fin (morph b c)} {h : Fin (morph c d)} →
                  ((h ∘ g) ∘ f) ≡ (h ∘ (g ∘ f))
        assoc {0F} {0F} {0F} {0F} {0F} {0F} {0F} = refl
        assoc {0F} {0F} {0F} {1F} {0F} {0F} {0F} = refl
        assoc {0F} {0F} {0F} {2F} {0F} {0F} {0F} = refl
        assoc {0F} {0F} {1F} {1F} {0F} {0F} {0F} = refl
        assoc {0F} {0F} {2F} {2F} {0F} {0F} {0F} = refl
        assoc {0F} {1F} {1F} {1F} {0F} {0F} {0F} = refl
        assoc {0F} {2F} {2F} {2F} {0F} {0F} {0F} = refl
        assoc {1F} {1F} {1F} {1F} {0F} {0F} {0F} = refl
        assoc {2F} {2F} {2F} {2F} {0F} {0F} {0F} = refl

        identityˡ : ∀ {f : Fin (morph a b)} → (id ∘ f) ≡ f
        identityˡ {0F} {0F} {0F} = refl
        identityˡ {0F} {1F} {0F} = refl
        identityˡ {0F} {2F} {0F} = refl
        identityˡ {1F} {1F} {0F} = refl
        identityˡ {2F} {2F} {0F} = refl

        identityʳ : ∀ {f : Fin (morph a b)} → (f ∘ id) ≡ f
        identityʳ {0F} {0F} {0F} = refl
        identityʳ {0F} {1F} {0F} = refl
        identityʳ {0F} {2F} {0F} = refl
        identityʳ {1F} {1F} {0F} = refl
        identityʳ {2F} {2F} {0F} = refl

Span : Category _ _ _
Span = FinCategory SpanShape

module Span = Category Span

open FinCatShape SpanShape

SpanToF : Functor Span Sp.Span
SpanToF = record
  { F₀           = F₀
  ; F₁           = F₁
  ; identity     = identity
  ; homomorphism = homomorphism
  ; F-resp-≈     = F-resp-≈
  }
  where F₀ : Fin 3 → Sp.SpanObj
        F₀ 0F = Sp.center
        F₀ 1F = Sp.left
        F₀ 2F = Sp.right

        F₁ : Fin ∣ a ⇒ b ∣ → Sp.SpanArr (F₀ a) (F₀ b)
        F₁ {0F} {0F} 0F = Sp.span-id
        F₁ {0F} {1F} 0F = Sp.span-arrˡ
        F₁ {0F} {2F} 0F = Sp.span-arrʳ
        F₁ {1F} {1F} 0F = Sp.span-id
        F₁ {2F} {2F} 0F = Sp.span-id

        identity : F₁ (id {a}) ≡ Sp.span-id
        identity {0F} = refl
        identity {1F} = refl
        identity {2F} = refl

        homomorphism : ∀ {f : Fin ∣ a ⇒ b ∣} {g : Fin ∣ b ⇒ c ∣} →
                         F₁ (g ∘ f) ≡ Sp.span-compose (F₁ g) (F₁ f)
        homomorphism {0F} {0F} {0F} {0F} {0F} = refl
        homomorphism {0F} {0F} {1F} {0F} {0F} = refl
        homomorphism {0F} {0F} {2F} {0F} {0F} = refl
        homomorphism {0F} {1F} {1F} {0F} {0F} = refl
        homomorphism {0F} {2F} {2F} {0F} {0F} = refl
        homomorphism {1F} {1F} {1F} {0F} {0F} = refl
        homomorphism {2F} {2F} {2F} {0F} {0F} = refl

        F-resp-≈ : ∀ {f g : Fin ∣ a ⇒ b ∣} → f ≡ g → F₁ f ≡ F₁ g
        F-resp-≈ {0F} {0F} {0F} {0F} _ = refl
        F-resp-≈ {0F} {1F} {0F} {0F} _ = refl
        F-resp-≈ {0F} {2F} {0F} {0F} _ = refl
        F-resp-≈ {1F} {1F} {0F} {0F} _ = refl
        F-resp-≈ {2F} {2F} {0F} {0F} _ = refl

module SpanToF = Functor SpanToF

SpanFromF : Functor Sp.Span Span
SpanFromF = record
  { F₀           = F₀
  ; F₁           = F₁
  ; identity     = identity
  ; homomorphism = homomorphism
  ; F-resp-≈     = F-resp-≈
  }
  where F₀ : Sp.SpanObj → Fin 3
        F₀ Sp.center = 0F
        F₀ Sp.left   = 1F
        F₀ Sp.right  = 2F

        F₁ : ∀ {A B} → Sp.Span [ A , B ] → Span [ F₀ A , F₀ B ]
        F₁ {Sp.center} Sp.span-id = 0F
        F₁ {Sp.left} Sp.span-id   = 0F
        F₁ {Sp.right} Sp.span-id  = 0F
        F₁ Sp.span-arrˡ           = 0F
        F₁ Sp.span-arrʳ           = 0F

        identity : ∀ {A} → F₁ (Category.id Sp.Span {A}) ≡ id
        identity {Sp.center} = refl
        identity {Sp.left}   = refl
        identity {Sp.right}  = refl

        homomorphism : ∀ {X Y Z} {f : Sp.Span [ X , Y ]} {g : Sp.Span [ Y , Z ]} →
                       F₁ (Sp.Span [ g ∘ f ]) ≡ F₁ g ∘ F₁ f
        homomorphism {Sp.center} {_} {_} {Sp.span-id} {Sp.span-id} = refl
        homomorphism {Sp.left} {_} {_} {Sp.span-id} {Sp.span-id}   = refl
        homomorphism {Sp.right} {_} {_} {Sp.span-id} {Sp.span-id}  = refl
        homomorphism {_} {_} {_} {Sp.span-id} {Sp.span-arrˡ}       = refl
        homomorphism {_} {_} {_} {Sp.span-id} {Sp.span-arrʳ}       = refl
        homomorphism {_} {_} {_} {Sp.span-arrˡ} {Sp.span-id}       = refl
        homomorphism {_} {_} {_} {Sp.span-arrʳ} {Sp.span-id}       = refl

        F-resp-≈ : ∀ {A B} {f g : Sp.Span [ A , B ]} → f ≡ g → F₁ f ≡ F₁ g
        F-resp-≈ {Sp.center} {_} {Sp.span-id} {Sp.span-id} _              = refl
        F-resp-≈ {Sp.left} {_} {Sp.span-id} {Sp.span-id} _                = refl
        F-resp-≈ {Sp.right} {_} {Sp.span-id} {Sp.span-id} _               = refl
        F-resp-≈ {.Sp.center} {.Sp.left} {Sp.span-arrˡ} {Sp.span-arrˡ} _  = refl
        F-resp-≈ {.Sp.center} {.Sp.right} {Sp.span-arrʳ} {Sp.span-arrʳ} _ = refl

module SpanFromF = Functor SpanFromF

SpansEquivF : SpanToF ⊣⊢ SpanFromF
SpansEquivF = withZig record
  { unit   = unit
  ; counit = counit
  ; zig    = zig
  }
  where unit⇒η : ∀ a → Fin ∣ a ⇒ SpanFromF.₀ (SpanToF.₀ a) ∣
        unit⇒η 0F = 0F
        unit⇒η 1F = 0F
        unit⇒η 2F = 0F
        unit⇐η : ∀ a → Fin ∣ SpanFromF.₀ (SpanToF.₀ a) ⇒ a ∣
        unit⇐η 0F = 0F
        unit⇐η 1F = 0F
        unit⇐η 2F = 0F

        unit : idF ≃ SpanFromF ∘F SpanToF
        unit = record
          { F⇒G = ntHelper record
            { η       = unit⇒η
            ; commute = commute₁
            }
          ; F⇐G = ntHelper record
            { η       = unit⇐η
            ; commute = commute₂
            }
          ; iso = iso
          }
          where open Mor Span
                commute₁ : ∀ (f : Fin ∣ a ⇒ b ∣) → unit⇒η b ∘ f ≡ SpanFromF.₁ (SpanToF.₁ f) ∘ unit⇒η a
                commute₁ {0F} {0F} 0F = refl
                commute₁ {0F} {1F} 0F = refl
                commute₁ {0F} {2F} 0F = refl
                commute₁ {1F} {1F} 0F = refl
                commute₁ {2F} {2F} 0F = refl
                commute₂ : ∀ (f : Fin ∣ a ⇒ b ∣) → unit⇐η b ∘ SpanFromF.₁ (SpanToF.₁ f) ≡ f ∘ unit⇐η a
                commute₂ {0F} {0F} 0F = refl
                commute₂ {0F} {1F} 0F = refl
                commute₂ {0F} {2F} 0F = refl
                commute₂ {1F} {1F} 0F = refl
                commute₂ {2F} {2F} 0F = refl

                iso : ∀ a → Iso (unit⇒η a) (unit⇐η a)
                iso 0F = record
                  { isoˡ = refl
                  ; isoʳ = refl
                  }
                iso 1F = record
                  { isoˡ = refl
                  ; isoʳ = refl
                  }
                iso 2F = record
                  { isoˡ = refl
                  ; isoʳ = refl
                  }

        counit⇒η : ∀ X → Sp.Span [ Functor.F₀ (SpanToF ∘F SpanFromF) X , X ]
        counit⇒η Sp.center = Sp.span-id
        counit⇒η Sp.left   = Sp.span-id
        counit⇒η Sp.right  = Sp.span-id

        counit⇐η : ∀ X → Sp.Span [ X , Functor.F₀ (SpanToF ∘F SpanFromF) X ]
        counit⇐η Sp.center = Sp.span-id
        counit⇐η Sp.left   = Sp.span-id
        counit⇐η Sp.right  = Sp.span-id

        counit : SpanToF ∘F SpanFromF ≃ idF
        counit = record
          { F⇒G = ntHelper record
            { η       = counit⇒η
            ; commute = commute₁
            }
          ; F⇐G = ntHelper record
            { η       = counit⇐η
            ; commute = commute₂
            }
          ; iso = iso
          }
          where open Mor Sp.Span
                commute₁ : ∀ {X Y} (f : Sp.SpanArr X Y) →
                             Sp.span-compose (counit⇒η Y) (SpanToF.₁ (SpanFromF.₁ f)) ≡ Sp.span-compose f (counit⇒η X)
                commute₁ {Sp.center} {.Sp.center} Sp.span-id   = refl
                commute₁ {Sp.left} {.Sp.left} Sp.span-id       = refl
                commute₁ {Sp.right} {.Sp.right} Sp.span-id     = refl
                commute₁ {.Sp.center} {.Sp.left} Sp.span-arrˡ  = refl
                commute₁ {.Sp.center} {.Sp.right} Sp.span-arrʳ = refl

                commute₂ : ∀ {X Y} (f : Sp.SpanArr X Y) →
                             Sp.span-compose (counit⇐η Y) f ≡ Sp.span-compose (SpanToF.₁ (SpanFromF.₁ f)) (counit⇐η X)
                commute₂ {Sp.center} {.Sp.center} Sp.span-id   = refl
                commute₂ {Sp.left} {.Sp.left} Sp.span-id       = refl
                commute₂ {Sp.right} {.Sp.right} Sp.span-id     = refl
                commute₂ {.Sp.center} {.Sp.left} Sp.span-arrˡ  = refl
                commute₂ {.Sp.center} {.Sp.right} Sp.span-arrʳ = refl

                iso : ∀ X → Iso (counit⇒η X) (counit⇐η X)
                iso Sp.center = record
                  { isoˡ = refl
                  ; isoʳ = refl
                  }
                iso Sp.left   = record
                  { isoˡ = refl
                  ; isoʳ = refl
                  }
                iso Sp.right  = record
                  { isoˡ = refl
                  ; isoʳ = refl
                  }

        zig : ∀ {a} → Sp.span-compose (counit⇒η (SpanToF.₀ a)) (SpanToF.₁ (unit⇒η a)) ≡ Sp.span-id
        zig {0F} = refl
        zig {1F} = refl
        zig {2F} = refl

SpansEquiv : ⊣Equivalence Span Sp.Span
SpansEquiv = record { L⊣⊢R = SpansEquivF }

module SpansEquiv = ⊣Equivalence SpansEquiv


text:
-- Basic intuitionistic modal logic S4, without ∨, ⊥, or ◇.
-- Gentzen-style formalisation of syntax, after Bierman-de Paiva.
-- Simple terms.

module BasicIS4.Syntax.Gentzen where

open import BasicIS4.Syntax.Common public

-- Derivations.

mutual
  infix 3 _⊢_
  data _⊢_ (Γ : Cx Ty) : Ty → Set where
    var      : ∀ {A}   → A ∈ Γ → Γ ⊢ A
    lam      : ∀ {A B} → Γ , A ⊢ B → Γ ⊢ A ▻ B
    app      : ∀ {A B} → Γ ⊢ A ▻ B → Γ ⊢ A → Γ ⊢ B
    multibox : ∀ {A Δ} → Γ ⊢⋆ □⋆ Δ → □⋆ Δ ⊢ A → Γ ⊢ □ A
    down     : ∀ {A}   → Γ ⊢ □ A → Γ ⊢ A
    pair     : ∀ {A B} → Γ ⊢ A → Γ ⊢ B → Γ ⊢ A ∧ B
    fst      : ∀ {A B} → Γ ⊢ A ∧ B → Γ ⊢ A
    snd      : ∀ {A B} → Γ ⊢ A ∧ B → Γ ⊢ B
    unit     : Γ ⊢ ⊤

  infix 3 _⊢⋆_
  _⊢⋆_ : Cx Ty → Cx Ty → Set
  Γ ⊢⋆ ∅     = 𝟙
  Γ ⊢⋆ Ξ , A = Γ ⊢⋆ Ξ × Γ ⊢ A

-- Monotonicity with respect to context inclusion.

mutual
  mono⊢ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢ A → Γ′ ⊢ A
  mono⊢ η (var i)         = var (mono∈ η i)
  mono⊢ η (lam t)         = lam (mono⊢ (keep η) t)
  mono⊢ η (app t u)       = app (mono⊢ η t) (mono⊢ η u)
  mono⊢ η (multibox ts u) = multibox (mono⊢⋆ η ts) u
  mono⊢ η (down t)        = down (mono⊢ η t)
  mono⊢ η (pair t u)      = pair (mono⊢ η t) (mono⊢ η u)
  mono⊢ η (fst t)         = fst (mono⊢ η t)
  mono⊢ η (snd t)         = snd (mono⊢ η t)
  mono⊢ η unit            = unit

  mono⊢⋆ : ∀ {Ξ Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢⋆ Ξ → Γ′ ⊢⋆ Ξ
  mono⊢⋆ {∅}     η ∙        = ∙
  mono⊢⋆ {Ξ , A} η (ts , t) = mono⊢⋆ η ts , mono⊢ η t

-- Shorthand for variables.

v₀ : ∀ {A Γ} → Γ , A ⊢ A
v₀ = var i₀

v₁ : ∀ {A B Γ} → Γ , A , B ⊢ A
v₁ = var i₁

v₂ : ∀ {A B C Γ} → Γ , A , B , C ⊢ A
v₂ = var i₂

-- Reflexivity.

refl⊢⋆ : ∀ {Γ} → Γ ⊢⋆ Γ
refl⊢⋆ {∅}     = ∙
refl⊢⋆ {Γ , A} = mono⊢⋆ weak⊆ refl⊢⋆ , v₀

-- Deduction theorem is built-in.

lam⋆ : ∀ {Ξ Γ A} → Γ ⧺ Ξ ⊢ A → Γ ⊢ Ξ ▻⋯▻ A
lam⋆ {∅}     = I
lam⋆ {Ξ , B} = lam⋆ {Ξ} ∘ lam

lam⋆₀ : ∀ {Γ A} → Γ ⊢ A → ∅ ⊢ Γ ▻⋯▻ A
lam⋆₀ {∅}     = I
lam⋆₀ {Γ , B} = lam⋆₀ ∘ lam

-- Detachment theorem.

det : ∀ {A B Γ} → Γ ⊢ A ▻ B → Γ , A ⊢ B
det t = app (mono⊢ weak⊆ t) v₀

det⋆ : ∀ {Ξ Γ A} → Γ ⊢ Ξ ▻⋯▻ A → Γ ⧺ Ξ ⊢ A
det⋆ {∅}     = I
det⋆ {Ξ , B} = det ∘ det⋆ {Ξ}

det⋆₀ : ∀ {Γ A} → ∅ ⊢ Γ ▻⋯▻ A → Γ ⊢ A
det⋆₀ {∅}     = I
det⋆₀ {Γ , B} = det ∘ det⋆₀

-- Cut and multicut.

cut : ∀ {A B Γ} → Γ ⊢ A → Γ , A ⊢ B → Γ ⊢ B
cut t u = app (lam u) t

multicut : ∀ {Ξ A Γ} → Γ ⊢⋆ Ξ → Ξ ⊢ A → Γ ⊢ A
multicut {∅}     ∙        u = mono⊢ bot⊆ u
multicut {Ξ , B} (ts , t) u = app (multicut ts (lam u)) t

-- Transitivity.

trans⊢⋆ : ∀ {Γ″ Γ′ Γ} → Γ ⊢⋆ Γ′ → Γ′ ⊢⋆ Γ″ → Γ ⊢⋆ Γ″
trans⊢⋆ {∅}      ts ∙        = ∙
trans⊢⋆ {Γ″ , A} ts (us , u) = trans⊢⋆ ts us , multicut ts u

-- Contraction.

ccont : ∀ {A B Γ} → Γ ⊢ (A ▻ A ▻ B) ▻ A ▻ B
ccont = lam (lam (app (app v₁ v₀) v₀))

cont : ∀ {A B Γ} → Γ , A , A ⊢ B → Γ , A ⊢ B
cont t = det (app ccont (lam (lam t)))

-- Exchange, or Schönfinkel’s C combinator.

cexch : ∀ {A B C Γ} → Γ ⊢ (A ▻ B ▻ C) ▻ B ▻ A ▻ C
cexch = lam (lam (lam (app (app v₂ v₀) v₁)))

exch : ∀ {A B C Γ} → Γ , A , B ⊢ C → Γ , B , A ⊢ C
exch t = det (det (app cexch (lam (lam t))))

-- Composition, or Schönfinkel’s B combinator.

ccomp : ∀ {A B C Γ} → Γ ⊢ (B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
ccomp = lam (lam (lam (app v₂ (app v₁ v₀))))

comp : ∀ {A B C Γ} → Γ , B ⊢ C → Γ , A ⊢ B → Γ , A ⊢ C
comp t u = det (app (app ccomp (lam t)) (lam u))

-- Useful theorems in functional form.

dist : ∀ {A B Γ} → Γ ⊢ □ (A ▻ B) → Γ ⊢ □ A → Γ ⊢ □ B
dist t u = multibox ((∙ , t) , u) (app (down v₁) (down v₀))

up : ∀ {A Γ} → Γ ⊢ □ A → Γ ⊢ □ □ A
up t = multibox (∙ , t) v₀

distup : ∀ {A B Γ} → Γ ⊢ □ (□ A ▻ B) → Γ ⊢ □ A → Γ ⊢ □ B
distup t u = dist t (up u)

box : ∀ {A Γ} → ∅ ⊢ A → Γ ⊢ □ A
box t = multibox ∙ t

unbox : ∀ {A C Γ} → Γ ⊢ □ A → Γ , □ A ⊢ C → Γ ⊢ C
unbox t u = app (lam u) t

-- Useful theorems in combinatory form.

ci : ∀ {A Γ} → Γ ⊢ A ▻ A
ci = lam v₀

ck : ∀ {A B Γ} → Γ ⊢ A ▻ B ▻ A
ck = lam (lam v₁)

cs : ∀ {A B C Γ} → Γ ⊢ (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
cs = lam (lam (lam (app (app v₂ v₀) (app v₁ v₀))))

cdist : ∀ {A B Γ} → Γ ⊢ □ (A ▻ B) ▻ □ A ▻ □ B
cdist = lam (lam (dist v₁ v₀))

cup : ∀ {A Γ} → Γ ⊢ □ A ▻ □ □ A
cup = lam (up v₀)

cdown : ∀ {A Γ} → Γ ⊢ □ A ▻ A
cdown = lam (down v₀)

cdistup : ∀ {A B Γ} → Γ ⊢ □ (□ A ▻ B) ▻ □ A ▻ □ B
cdistup = lam (lam (dist v₁ (up v₀)))

cunbox : ∀ {A C Γ} → Γ ⊢ □ A ▻ (□ A ▻ C) ▻ C
cunbox = lam (lam (app v₀ v₁))

cpair : ∀ {A B Γ} → Γ ⊢ A ▻ B ▻ A ∧ B
cpair = lam (lam (pair v₁ v₀))

cfst : ∀ {A B Γ} → Γ ⊢ A ∧ B ▻ A
cfst = lam (fst v₀)

csnd : ∀ {A B Γ} → Γ ⊢ A ∧ B ▻ B
csnd = lam (snd v₀)

-- Internalisation, or lifting, and additional theorems.

lift : ∀ {Γ A} → Γ ⊢ A → □⋆ Γ ⊢ □ A
lift {∅}     t = box t
lift {Γ , B} t = det (app cdist (lift (lam t)))

hypup : ∀ {A B Γ} → Γ ⊢ A ▻ B → Γ ⊢ □ A ▻ B
hypup t = lam (app (mono⊢ weak⊆ t) (down v₀))

hypdown : ∀ {A B Γ} → Γ ⊢ □ □ A ▻ B → Γ ⊢ □ A ▻ B
hypdown t = lam (app (mono⊢ weak⊆ t) (up v₀))

cxup : ∀ {Γ A} → Γ ⊢ A → □⋆ Γ ⊢ A
cxup {∅}     t = t
cxup {Γ , B} t = det (hypup (cxup (lam t)))

cxdown : ∀ {Γ A} → □⋆ □⋆ Γ ⊢ A → □⋆ Γ ⊢ A
cxdown {∅}     t = t
cxdown {Γ , B} t = det (hypdown (cxdown (lam t)))

box⋆ : ∀ {Ξ Γ} → ∅ ⊢⋆ Ξ → Γ ⊢⋆ □⋆ Ξ
box⋆ {∅}     ∙        = ∙
box⋆ {Ξ , A} (ts , t) = box⋆ ts , box t

lift⋆ : ∀ {Ξ Γ} → Γ ⊢⋆ Ξ → □⋆ Γ ⊢⋆ □⋆ Ξ
lift⋆ {∅}     ∙        = ∙
lift⋆ {Ξ , A} (ts , t) = lift⋆ ts , lift t

up⋆ : ∀ {Ξ Γ} → Γ ⊢⋆ □⋆ Ξ → Γ ⊢⋆ □⋆ □⋆ Ξ
up⋆ {∅}     ∙        = ∙
up⋆ {Ξ , A} (ts , t) = up⋆ ts , up t

down⋆ : ∀ {Ξ Γ} → Γ ⊢⋆ □⋆ Ξ → Γ ⊢⋆ Ξ
down⋆ {∅}     ∙        = ∙
down⋆ {Ξ , A} (ts , t) = down⋆ ts , down t

dist′ : ∀ {A B Γ} → Γ ⊢ □ (A ▻ B) → Γ ⊢ □ A ▻ □ B
dist′ t = lam (dist (mono⊢ weak⊆ t) v₀)

mpair : ∀ {A B Γ} → Γ ⊢ □ A → Γ ⊢ □ B → Γ ⊢ □ (A ∧ B)
mpair t u = multibox ((∙ , t) , u) (pair (down v₁) (down v₀))

mfst : ∀ {A B Γ} → Γ ⊢ □ (A ∧ B) → Γ ⊢ □ A
mfst t = multibox (∙ , t) (fst (down v₀))

msnd : ∀ {A B Γ} → Γ ⊢ □ (A ∧ B) → Γ ⊢ □ B
msnd t = multibox (∙ , t) (snd (down v₀))

-- Closure under context concatenation.

concat : ∀ {A B Γ} Γ′ → Γ , A ⊢ B → Γ′ ⊢ A → Γ ⧺ Γ′ ⊢ B
concat Γ′ t u = app (mono⊢ (weak⊆⧺₁ Γ′) (lam t)) (mono⊢ weak⊆⧺₂ u)

-- Substitution.

mutual
  [_≔_]_ : ∀ {A B Γ} → (i : A ∈ Γ) → Γ ∖ i ⊢ A → Γ ⊢ B → Γ ∖ i ⊢ B
  [ i ≔ s ] var j         with i ≟∈ j
  [ i ≔ s ] var .i        | same   = s
  [ i ≔ s ] var ._        | diff j = var j
  [ i ≔ s ] lam t         = lam ([ pop i ≔ mono⊢ weak⊆ s ] t)
  [ i ≔ s ] app t u       = app ([ i ≔ s ] t) ([ i ≔ s ] u)
  [ i ≔ s ] multibox ts u = multibox ([ i ≔ s ]⋆ ts) u
  [ i ≔ s ] down t        = down ([ i ≔ s ] t)
  [ i ≔ s ] pair t u      = pair ([ i ≔ s ] t) ([ i ≔ s ] u)
  [ i ≔ s ] fst t         = fst ([ i ≔ s ] t)
  [ i ≔ s ] snd t         = snd ([ i ≔ s ] t)
  [ i ≔ s ] unit          = unit

  [_≔_]⋆_ : ∀ {Ξ A Γ} → (i : A ∈ Γ) → Γ ∖ i ⊢ A → Γ ⊢⋆ Ξ → Γ ∖ i ⊢⋆ Ξ
  [_≔_]⋆_ {∅}     i s ∙        = ∙
  [_≔_]⋆_ {Ξ , B} i s (ts , t) = [ i ≔ s ]⋆ ts , [ i ≔ s ] t

-- Convertibility.

data _⋙_ {Γ : Cx Ty} : ∀ {A} → Γ ⊢ A → Γ ⊢ A → Set where
  refl⋙      : ∀ {A} → {t : Γ ⊢ A}
                      → t ⋙ t

  trans⋙     : ∀ {A} → {t t′ t″ : Γ ⊢ A}
                      → t ⋙ t′ → t′ ⋙ t″
                      → t ⋙ t″

  sym⋙       : ∀ {A} → {t t′ : Γ ⊢ A}
                      → t ⋙ t′
                      → t′ ⋙ t

  conglam⋙   : ∀ {A B} → {t t′ : Γ , A ⊢ B}
                        → t ⋙ t′
                        → lam t ⋙ lam t′

  congapp⋙   : ∀ {A B} → {t t′ : Γ ⊢ A ▻ B} → {u u′ : Γ ⊢ A}
                        → t ⋙ t′ → u ⋙ u′
                        → app t u ⋙ app t′ u′

  -- TODO: What about multibox?
  congdown⋙  : ∀ {A} → {t t′ : Γ ⊢ □ A}
                      → t ⋙ t′
                      → down t ⋙ down t′

  congpair⋙  : ∀ {A B} → {t t′ : Γ ⊢ A} → {u u′ : Γ ⊢ B}
                        → t ⋙ t′ → u ⋙ u′
                        → pair t u ⋙ pair t′ u′

  congfst⋙   : ∀ {A B} → {t t′ : Γ ⊢ A ∧ B}
                        → t ⋙ t′
                        → fst t ⋙ fst t′

  congsnd⋙   : ∀ {A B} → {t t′ : Γ ⊢ A ∧ B}
                        → t ⋙ t′
                        → snd t ⋙ snd t′

  beta▻⋙     : ∀ {A B} → {t : Γ , A ⊢ B} → {u : Γ ⊢ A}
                        → app (lam t) u ⋙ ([ top ≔ u ] t)

  eta▻⋙      : ∀ {A B} → {t : Γ ⊢ A ▻ B}
                        → t ⋙ lam (app (mono⊢ weak⊆ t) v₀)

  -- TODO: What about beta and eta for □?
  beta∧₁⋙    : ∀ {A B} → {t : Γ ⊢ A} → {u : Γ ⊢ B}
                        → fst (pair t u) ⋙ t

  beta∧₂⋙    : ∀ {A B} → {t : Γ ⊢ A} → {u : Γ ⊢ B}
                        → snd (pair t u) ⋙ u

  eta∧⋙      : ∀ {A B} → {t : Γ ⊢ A ∧ B}
                        → t ⋙ pair (fst t) (snd t)

  eta⊤⋙     : ∀ {t : Γ ⊢ ⊤} → t ⋙ unit

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
module Not-named-according-to-the-Haskell-lexical-syntax where

postulate
  IO : Set -> Set

{-# BUILTIN IO IO #-}
{-# COMPILED_TYPE IO IO #-}

postulate
  return : {A : Set} -> A -> IO A

{-# COMPILED return (\_ -> return :: a -> IO a) #-}
{-# COMPILED_EPIC return (u1 : Unit, a : Any) -> Any = ioreturn(a) #-}

data Unit : Set where
  unit : Unit

{-# COMPILED_DATA Unit () () #-}

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module examplesPaperJFP.NativeIOSafe where

open import Data.Maybe.Base using (Maybe; nothing; just) public
open import Data.String.Base using (String) public

record Unit : Set where
  constructor unit

{-# COMPILE GHC Unit = () #-}

postulate
  NativeIO     : Set → Set
  nativeReturn : {A : Set} → A → NativeIO A
  _native>>=_  : {A B : Set} → NativeIO A → (A → NativeIO B) → NativeIO B

{-# BUILTIN IO NativeIO #-}
{-# COMPILE GHC NativeIO = IO #-}   -- IO.FF-I.AgdaIO
{-# COMPILE GHC _native>>=_ = (\_ _ -> (>>=) :: IO a -> (a -> IO b) -> IO b) #-}
{-# COMPILE GHC nativeReturn = (\_ -> return :: a -> IO a) #-}

postulate
  nativeGetLine   : NativeIO (Maybe String)
  nativePutStrLn  : String → NativeIO Unit

{-# FOREIGN GHC import Data.Text #-}
{-# FOREIGN GHC import System.IO.Error #-}

{-# COMPILE GHC nativePutStrLn = (\ s -> putStrLn (Data.Text.unpack s)) #-}
{-# COMPILE GHC nativeGetLine = (fmap (Just . Data.Text.pack) getLine `System.IO.Error.catchIOError` \ err -> if System.IO.Error.isEOFError err then return Nothing else ioError err) #-}

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module Data.String.Instance where

open import Agda.Builtin.String
open import Class.Equality
open import Class.Monoid
open import Class.Show
open import Data.String renaming (_≟_ to _≟S_)

instance
  String-Eq : Eq String
  String-Eq = record { _≟_ = _≟S_ }

  String-EqB : EqB String
  String-EqB = record { _≣_ = primStringEquality }

  String-Monoid : Monoid String
  String-Monoid = record { mzero = "" ; _+_ = _++_ }

  String-Show : Show String
  String-Show = record { show = λ x -> x }

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
module Numeral.Natural.Function.Proofs where

import      Lvl
open import Data.Tuple
open import Functional
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Numeral.Natural
open import Numeral.Natural.Function
open import Numeral.Natural.Relation.Order as ≤ using (_≤_ ; _≥_)
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Oper.Proofs.Order
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Function.Domain
import      Structure.Operator.Names as Names
open import Structure.Operator.Properties
open import Structure.Relator.Properties
open import Syntax.Transitivity

max-0ₗ : ∀{b} → (max 𝟎 b ≡ b)
max-0ₗ {𝟎}   = [≡]-intro
max-0ₗ {𝐒 b} = [≡]-intro
{-# REWRITE max-0ₗ #-}

max-0ᵣ : ∀{a} → (max a 𝟎 ≡ a)
max-0ᵣ {𝟎}   = [≡]-intro
max-0ᵣ {𝐒 a} = [≡]-intro
{-# REWRITE max-0ᵣ #-}

min-0ₗ : ∀{b} → (min 𝟎 b ≡ 𝟎)
min-0ₗ {𝟎}   = [≡]-intro
min-0ₗ {𝐒 b} = [≡]-intro
{-# REWRITE min-0ₗ #-}

min-0ᵣ : ∀{a} → (min a 𝟎 ≡ 𝟎)
min-0ᵣ {𝟎}   = [≡]-intro
min-0ᵣ {𝐒 a} = [≡]-intro
{-# REWRITE min-0ᵣ #-}

instance
  min-idempotence : Idempotence(min)
  min-idempotence = intro proof where
    proof : Names.Idempotence(min)
    proof{𝟎}   = [≡]-intro
    proof{𝐒 x} = [≡]-with(𝐒) (proof{x})

instance
  max-idempotence : Idempotence(max)
  max-idempotence = intro proof where
    proof : Names.Idempotence(max)
    proof{𝟎}   = [≡]-intro
    proof{𝐒 x} = [≡]-with(𝐒) (proof{x})

max-elementary : ∀{a b} → (max(a)(b) ≡ a + (b −₀ a))
max-elementary {𝟎}    {𝟎}    = [≡]-intro
max-elementary {𝟎}    {𝐒(b)} = [≡]-intro
max-elementary {𝐒(a)} {𝟎}    = [≡]-intro
max-elementary {𝐒(a)} {𝐒(b)} = [≡]-with(𝐒) (max-elementary {a} {b})

min-elementary : ∀{a b} → (min(a)(b) ≡ b −₀ (b −₀ a))
min-elementary {𝟎}    {𝟎}    = [≡]-intro
min-elementary {𝟎}    {𝐒(b)} = [≡]-intro
min-elementary {𝐒(a)} {𝟎}    = [≡]-intro
min-elementary {𝐒(a)} {𝐒(b)} = ([≡]-with(𝐒) (min-elementary {a} {b})) 🝖 (symmetry(_≡_) ([↔]-to-[→] [−₀][𝐒]ₗ-equality ([−₀]-lesser {b}{a})))

instance
  min-commutativity : Commutativity(min)
  Commutativity.proof(min-commutativity) = proof where
    proof : Names.Commutativity(min)
    proof{𝟎}   {𝟎}    = [≡]-intro
    proof{𝟎}   {𝐒(b)} = [≡]-intro
    proof{𝐒(a)}{𝟎}    = [≡]-intro
    proof{𝐒(a)}{𝐒(b)} = [≡]-with(𝐒) (proof{a}{b})

instance
  min-associativity : Associativity(min)
  Associativity.proof(min-associativity) = proof where
    proof : Names.Associativity(min)
    proof{𝟎}   {𝟎}   {𝟎}    = [≡]-intro
    proof{𝟎}   {𝟎}   {𝐒(c)} = [≡]-intro
    proof{𝟎}   {𝐒(b)}{𝟎}    = [≡]-intro
    proof{𝐒(a)}{𝟎}   {𝟎}    = [≡]-intro
    proof{𝟎}   {𝐒(b)}{𝐒(c)} = [≡]-intro
    proof{𝐒(a)}{𝟎}   {𝐒(c)} = [≡]-intro
    proof{𝐒(a)}{𝐒(b)}{𝟎}    = [≡]-intro
    proof{𝐒(a)}{𝐒(b)}{𝐒(c)} = [≡]-with(𝐒) (proof{a}{b}{c})
    -- min(min(𝐒x)(𝐒y))(𝐒z)
    -- = min(𝐒min(x)(y))(𝐒z)
    -- = 𝐒(min(min(x)(y))(z))
    -- = 𝐒(min(x)(min(y)(z)))
    -- = min(𝐒x)(𝐒min(y)(z))
    -- = min(𝐒x)(min(𝐒y)(𝐒z)

instance
  min-orderₗ : ∀{a b} → (min(a)(b) ≤ a)
  min-orderₗ {𝟎}   {𝟎}    = [≤]-minimum {𝟎}
  min-orderₗ {𝐒(a)}{𝟎}    = [≤]-minimum {𝐒(a)}
  min-orderₗ {𝟎}   {𝐒(b)} = [≤]-minimum {𝟎}
  min-orderₗ {𝐒(a)}{𝐒(b)} = [≤]-with-[𝐒] ⦃ min-orderₗ {a}{b} ⦄

instance
  min-orderᵣ : ∀{a b} → (min(a)(b) ≤ b)
  min-orderᵣ {𝟎}   {𝟎}    = [≤]-minimum {𝟎}
  min-orderᵣ {𝐒(a)}{𝟎}    = [≤]-minimum {𝟎}
  min-orderᵣ {𝟎}   {𝐒(b)} = [≤]-minimum {𝐒(b)}
  min-orderᵣ {𝐒(a)}{𝐒(b)} = [≤]-with-[𝐒] ⦃ min-orderᵣ {a}{b} ⦄

min-arg : ∀{a b} → (min(a)(b) ≡ a) ∨ (min(a)(b) ≡ b)
min-arg {𝟎}   {𝟎}    = [∨]-introₗ([≡]-intro)
min-arg {𝟎}   {𝐒(b)} = [∨]-introₗ([≡]-intro)
min-arg {𝐒(a)}{𝟎}    = [∨]-introᵣ([≡]-intro)
min-arg {𝐒(a)}{𝐒(b)} = constructive-dilemma ([≡]-with(𝐒)) ([≡]-with(𝐒)) (min-arg {a}{b})

min-defₗ : ∀{a b} → (a ≤ b) ↔ (min(a)(b) ≡ a)
min-defₗ {a}{b} = [↔]-intro (l{a}{b}) (r{a}{b}) where
  l : ∀{a b} → (a ≤ b) ← (min(a)(b) ≡ a)
  l {𝟎}   {𝟎}    _      = [≤]-minimum {𝟎}
  l {𝟎}   {𝐒(b)} _      = [≤]-minimum {𝐒(b)}
  l {𝐒(_)}{𝟎}    ()
  l {𝐒(a)}{𝐒(b)} minaba = [≤]-with-[𝐒] ⦃ l{a}{b} (injective(𝐒) (minaba)) ⦄

  r : ∀{a b} → (a ≤ b) → (min(a)(b) ≡ a)
  r {𝟎}   {𝟎}    _                     = [≡]-intro
  r {𝟎}   {𝐒(b)} _                     = [≡]-intro
  r {𝐒(_)}{𝟎}    ()
  r {𝐒(a)}{𝐒(b)} (≤.succ ab) = [≡]-with(𝐒) (r{a}{b} (ab))

min-defᵣ : ∀{a b} → (b ≤ a) ↔ (min(a)(b) ≡ b)
min-defᵣ {a}{b} = [≡]-substitutionᵣ (commutativity(min)) {expr ↦ (b ≤ a) ↔ (expr ≡ b)} (min-defₗ{b}{a})

instance
  max-commutativity : Commutativity(max)
  Commutativity.proof(max-commutativity) = proof where
    proof : Names.Commutativity(max)
    proof{𝟎}   {𝟎}    = [≡]-intro
    proof{𝟎}   {𝐒(b)} = [≡]-intro
    proof{𝐒(a)}{𝟎}    = [≡]-intro
    proof{𝐒(a)}{𝐒(b)} = [≡]-with(𝐒) (proof{a}{b})

instance
  max-associativity : Associativity(max)
  Associativity.proof(max-associativity) = proof where
    proof : Names.Associativity(max)
    proof{𝟎}   {𝟎}   {𝟎}    = [≡]-intro
    proof{𝟎}   {𝟎}   {𝐒(c)} = [≡]-intro
    proof{𝟎}   {𝐒(b)}{𝟎}    = [≡]-intro
    proof{𝐒(a)}{𝟎}   {𝟎}    = [≡]-intro
    proof{𝟎}   {𝐒(b)}{𝐒(c)} = [≡]-intro
    proof{𝐒(a)}{𝟎}   {𝐒(c)} = [≡]-intro
    proof{𝐒(a)}{𝐒(b)}{𝟎}    = [≡]-intro
    proof{𝐒(a)}{𝐒(b)}{𝐒(c)} = [≡]-with(𝐒) (proof{a}{b}{c})

-- max-[+]-distributivityₗ : Distributivityₗ(max)
-- max-[+]-distributivityᵣ : Distributivityᵣ(max)

instance
  max-orderₗ : ∀{a b} → (max(a)(b) ≥ a)
  max-orderₗ {𝟎}   {𝟎}    = [≤]-minimum {max(𝟎)(𝟎)}
  max-orderₗ {𝐒(a)}{𝟎}    = reflexivity(_≥_)
  max-orderₗ {𝟎}   {𝐒(b)} = [≤]-minimum {max(𝟎)(𝐒(b))}
  max-orderₗ {𝐒(a)}{𝐒(b)} = [≤]-with-[𝐒] ⦃ max-orderₗ {a}{b} ⦄

instance
  max-orderᵣ : ∀{a b} → (max(a)(b) ≥ b)
  max-orderᵣ {𝟎}   {𝟎}    = [≤]-minimum {max(𝟎)(𝟎)}
  max-orderᵣ {𝐒(a)}{𝟎}    = [≤]-minimum {max(𝐒(a))(𝟎)}
  max-orderᵣ {𝟎}   {𝐒(b)} = reflexivity(_≥_)
  max-orderᵣ {𝐒(a)}{𝐒(b)} = [≤]-with-[𝐒] ⦃ max-orderᵣ {a}{b} ⦄

max-arg : ∀{a b} → (max(a)(b) ≡ a)∨(max(a)(b) ≡ b)
max-arg {𝟎}   {𝟎}    = [∨]-introₗ([≡]-intro)
max-arg {𝟎}   {𝐒(b)} = [∨]-introᵣ([≡]-intro)
max-arg {𝐒(a)}{𝟎}    = [∨]-introₗ([≡]-intro)
max-arg {𝐒(a)}{𝐒(b)} = constructive-dilemma ([≡]-with(𝐒)) ([≡]-with(𝐒)) (max-arg {a}{b})

max-defₗ : ∀{a b} → (a ≥ b) ↔ (max(a)(b) ≡ a)
max-defₗ {a}{b} = [↔]-intro (l{a}{b}) (r{a}{b}) where
  l : ∀{a b} → (a ≥ b) ← (max(a)(b) ≡ a)
  l {𝟎}   {𝟎}    _      = [≤]-minimum {𝟎}
  l {𝟎}   {𝐒(_)} ()
  l {𝐒(a)}{𝟎}    _      = [≤]-minimum {𝐒(a)}
  l {𝐒(a)}{𝐒(b)} maxaba = [≤]-with-[𝐒] ⦃ l{a}{b}(injective(𝐒) (maxaba)) ⦄

  r : ∀{a b} → (a ≥ b) → (max(a)(b) ≡ a)
  r {𝟎}   {𝟎}    _                     = [≡]-intro
  r {𝟎}   {𝐒(_)} ()
  r {𝐒(_)}{𝟎}    _                     = [≡]-intro
  r {𝐒(a)}{𝐒(b)} (≤.succ ab) = [≡]-with(𝐒) (r{a}{b} (ab))

max-defᵣ : ∀{a b} → (b ≥ a) ↔ (max(a)(b) ≡ b)
max-defᵣ {a}{b} = [≡]-substitutionᵣ (commutativity(max)) {expr ↦ (b ≥ a) ↔ (expr ≡ b)} (max-defₗ{b}{a})

min-with-max : ∀{a b} → (min(a)(b) ≡ (a + b) −₀ max(a)(b))
min-with-max {a}{b} =
  min(a)(b)                 🝖-[ min-elementary{a}{b} ]
  b −₀ (b −₀ a)             🝖-[ [−₀][+]ₗ-nullify {a}{b}{b −₀ a} ]-sym
  (a + b) −₀ (a + (b −₀ a)) 🝖-[ [≡]-with((a + b) −₀_) (max-elementary{a}{b}) ]-sym
  (a + b) −₀ max(a)(b)      🝖-end

max-with-min : ∀{a b} → (max(a)(b) ≡ (a + b) −₀ min(a)(b))
max-with-min {a}{b} with [≤][>]-dichotomy {a}{b}
... | [∨]-introₗ ab =
  max(a)(b)            🝖-[ [↔]-to-[→] max-defᵣ ab ]
  b                    🝖-[ [−₀]ₗ[+]ₗ-nullify {a}{b} ]-sym
  (a + b) −₀ a         🝖-[ [≡]-with((a + b) −₀_) ([↔]-to-[→] min-defₗ ab) ]-sym
  (a + b) −₀ min(a)(b) 🝖-end
... | [∨]-introᵣ 𝐒ba with ba ← [≤]-predecessor 𝐒ba =
  max(a)(b)            🝖-[ [↔]-to-[→] max-defₗ ba ]
  a                    🝖-[ [−₀]ₗ[+]ᵣ-nullify {a}{b} ]-sym
  (a + b) −₀ b         🝖-[ [≡]-with((a + b) −₀_) ([↔]-to-[→] min-defᵣ ba) ]-sym
  (a + b) −₀ min(a)(b) 🝖-end

[≤]-conjunction-min : ∀{a b c} → ((a ≤ b) ∧ (a ≤ c)) ↔ (a ≤ min b c)
[≤]-conjunction-min {a}{b}{c} = [↔]-intro (a≤bc ↦ [∧]-intro (a≤bc 🝖 min-orderₗ) (a≤bc 🝖 min-orderᵣ)) (uncurry r) where
  r : ∀{a b c} → (a ≤ b) → (a ≤ c) → (a ≤ min b c)
  r {.0}     {b}      {c}     ≤.min  ≤.min = ≤.min
  r {.(𝐒 a)} {.(𝐒 b)} {.(𝐒 c)} (≤.succ {a} {b} ab) (≤.succ {y = c} ac) = [≤]-with-[𝐒] ⦃ r {a}{b}{c} ab ac ⦄

[≤]-conjunction-max : ∀{a b c} → ((a ≤ c) ∧ (b ≤ c)) ↔ (max a b ≤ c)
[≤]-conjunction-max {a}{b}{c} = [↔]-intro (ab≤c ↦ [∧]-intro (max-orderₗ 🝖 ab≤c) ((max-orderᵣ 🝖 ab≤c))) (uncurry r) where
  r : ∀{a b c} → (a ≤ c) → (b ≤ c) → (max a b ≤ c)
  r {.0}     {b@(𝐒 _)}{c}      ≤.min  bc     = bc
  r {a}      {.0}     {c}      ac     ≤.min  = ac
  r {𝐒 a} {𝐒 b} {𝐒 c} (≤.succ ac) (≤.succ bc) = [≤]-with-[𝐒] ⦃ r {a}{b}{c} ac bc ⦄

[≤]-disjunction-min : ∀{a b c} → ((a ≤ c) ∨ (b ≤ c)) ↔ (min a b ≤ c)
[≤]-disjunction-min = [↔]-intro
  (ab≤c ↦ [∨]-elim2
    ((_🝖 ab≤c) ∘ [≡]-to-[≤] ∘ symmetry(_≡_))
    ((_🝖 ab≤c) ∘ [≡]-to-[≤] ∘ symmetry(_≡_))
    min-arg
  )
  ([∨]-elim
    (min-orderₗ 🝖_)
    (min-orderᵣ 🝖_)
  )

[≤]-disjunction-max : ∀{a b c} → ((a ≤ b) ∨ (a ≤ c)) ↔ (a ≤ max b c)
[≤]-disjunction-max = [↔]-intro
  (a≤bc ↦ [∨]-elim2
    ((_🝖 a≤bc) ∘ [≡]-to-[≤])
    ((_🝖 a≤bc) ∘ [≡]-to-[≤])
    max-arg
  )
  ([∨]-elim
    (_🝖 max-orderₗ)
    (_🝖 max-orderᵣ)
  )

min-order-max : ∀{a b} → (min(a)(b) ≤ max(a)(b))
min-order-max {𝟎}   {b}   = [≤]-minimum
min-order-max {𝐒 a} {𝟎}   = [≤]-minimum
min-order-max {𝐒 a} {𝐒 b} = [≤]-with-[𝐒] ⦃ min-order-max {a}{b} ⦄

max-order-[+] : ∀{a b} → (max(a)(b) ≤ a + b)
max-order-[+] {a}{b} = [↔]-to-[→] [≤]-conjunction-max ([∧]-intro [≤]-of-[+]ₗ ([≤]-of-[+]ᵣ {a}{b}))