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

module Cubical.Categories.NaturalTransformation.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism renaming (iso to iIso)
open import Cubical.Data.Sigma
open import Cubical.Categories.Category
open import Cubical.Categories.Functor.Base
open import Cubical.Categories.Morphism renaming (isIso to isIsoC)
open import Cubical.Categories.NaturalTransformation.Base

private
  variable
    ℓC ℓC' ℓD ℓD' : Level

open isIsoC
open NatIso
open NatTrans
open Category
open Functor
open Iso

module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where
  private
    _⋆ᴰ_ : ∀ {x y z} (f : D [ x , y ]) (g : D [ y , z ]) → D [ x , z ]
    f ⋆ᴰ g = f ⋆⟨ D ⟩ g

  -- natural isomorphism is symmetric
  symNatIso : ∀ {F G : Functor C D}
            → F ≅ᶜ G
            → G ≅ᶜ F
  symNatIso η .trans .N-ob x = η .nIso x .inv
  symNatIso η .trans .N-hom _ = sqLL η
  symNatIso η .nIso x .inv = η .trans .N-ob x
  symNatIso η .nIso x .sec = η .nIso x .ret
  symNatIso η .nIso x .ret = η .nIso x .sec

  -- Properties

  -- path helpers
  module NatTransP where

    module _ {F G : Functor C D} where

      -- same as Sigma version
      NatTransΣ : Type (ℓ-max (ℓ-max ℓC ℓC') ℓD')
      NatTransΣ = Σ[ ob ∈ ((x : C .ob) → D [(F .F-ob x) , (G .F-ob x)]) ]
                     ({x y : _ } (f : C [ x , y ]) → (F .F-hom f) ⋆ᴰ (ob y) ≡ (ob x) ⋆ᴰ (G .F-hom f))

      NatTransIsoΣ : Iso (NatTrans F G) NatTransΣ
      NatTransIsoΣ .fun (natTrans N-ob N-hom) = N-ob , N-hom
      NatTransIsoΣ .inv (N-ob , N-hom) = (natTrans N-ob N-hom)
      NatTransIsoΣ .rightInv _ = refl
      NatTransIsoΣ .leftInv _ = refl

      NatTrans≡Σ : NatTrans F G ≡ NatTransΣ
      NatTrans≡Σ = isoToPath NatTransIsoΣ

      -- introducing paths
      NatTrans-≡-intro : ∀ {αo βo : N-ob-Type F G}
                           {αh : N-hom-Type F G αo}
                           {βh : N-hom-Type F G βo}
                       → (p : αo ≡ βo)
                       → PathP (λ i → ({x y : C .ob} (f : C [ x , y ]) → (F .F-hom f) ⋆ᴰ (p i y) ≡ (p i x) ⋆ᴰ (G .F-hom f))) αh βh
                       → natTrans {F = F} {G} αo αh ≡ natTrans βo βh
      NatTrans-≡-intro p q i = natTrans (p i) (q i)

  module _ {F G : Functor C D} {α β : NatTrans F G} where
      open Iso
      private
        αOb = α .N-ob
        βOb = β .N-ob
        αHom = α .N-hom
        βHom = β .N-hom
      -- path between natural transformations is the same as a pair of paths (between ob and hom)
      NTPathIsoPathΣ : Iso (α ≡ β)
                         (Σ[ p ∈ (αOb ≡ βOb) ]
                              (PathP (λ i → ({x y : _} (f : _) → F ⟪ f ⟫ ⋆ᴰ (p i y) ≡ (p i x) ⋆ᴰ G ⟪ f ⟫))
                                  αHom
                                  βHom))
      NTPathIsoPathΣ .fun p = (λ i → p i .N-ob) , (λ i → p i .N-hom)
      NTPathIsoPathΣ .inv (po , ph) i = record { N-ob = po i ; N-hom = ph i }
      NTPathIsoPathΣ .rightInv pσ = refl
      NTPathIsoPathΣ .leftInv p = refl

      NTPath≃PathΣ = isoToEquiv NTPathIsoPathΣ

      NTPath≡PathΣ = ua NTPath≃PathΣ

  module _ where
    open NatTransP

    -- if the target category has hom Sets, then any natural transformation is a set
    isSetNatTrans : {F G : Functor C D} → isSet (NatTrans F G)
    isSetNatTrans =
      isSetRetract (fun NatTransIsoΣ) (inv NatTransIsoΣ) (leftInv NatTransIsoΣ)
                   (isSetΣSndProp (isSetΠ (λ _ → isSetHom D))
                                  (λ _ → isPropImplicitΠ2 (λ _ _ → isPropΠ (λ _ → isSetHom D _ _))))

max_stars_repo_name: FernandoLarrain/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Divisibility
------------------------------------------------------------------------

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

module Data.Nat.Divisibility where

open import Algebra
open import Data.Nat as Nat
open import Data.Nat.DivMod
open import Data.Nat.Properties
open import Data.Nat.Solver
open import Data.Fin using (Fin; zero; suc; toℕ)
import Data.Fin.Properties as FP
open import Data.Product
open import Function
open import Function.Equivalence using (_⇔_; equivalence)
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Binary
import Relation.Binary.Reasoning.PartialOrder as POR
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst)

open +-*-Solver

------------------------------------------------------------------------
-- m ∣ n is inhabited iff m divides n. Some sources, like Hardy and
-- Wright's "An Introduction to the Theory of Numbers", require m to
-- be non-zero. However, some things become a bit nicer if m is
-- allowed to be zero. For instance, _∣_ becomes a partial order, and
-- the gcd of 0 and 0 becomes defined.

infix 4 _∣_ _∤_

record _∣_ (m n : ℕ) : Set where
  constructor divides
  field quotient : ℕ
        equality : n ≡ quotient * m
open _∣_ using (quotient) public

_∤_ : Rel ℕ _
m ∤ n = ¬ (m ∣ n)

------------------------------------------------------------------------
-- _∣_ is a partial order

∣⇒≤ : ∀ {m n} → m ∣ suc n → m ≤ suc n
∣⇒≤         (divides zero    ())
∣⇒≤ {m} {n} (divides (suc q) eq) = begin
  m          ≤⟨ m≤m+n m (q * m) ⟩
  suc q * m  ≡⟨ sym eq ⟩
  suc n      ∎
  where open ≤-Reasoning

∣-reflexive : _≡_ ⇒ _∣_
∣-reflexive {n} refl = divides 1 (sym (*-identityˡ n))

∣-refl : Reflexive _∣_
∣-refl = ∣-reflexive refl

∣-trans : Transitive _∣_
∣-trans (divides p refl) (divides q refl) =
  divides (q * p) (sym (*-assoc q p _))

∣-antisym : Antisymmetric _≡_ _∣_
∣-antisym {m} {0} _ (divides q eq) = trans eq (*-comm q 0)
∣-antisym {0} {n} (divides p eq) _ = sym (trans eq (*-comm p 0))
∣-antisym {suc m} {suc n} (divides p eq₁) (divides q eq₂) =
  ≤-antisym (∣⇒≤ (divides p eq₁)) (∣⇒≤ (divides q eq₂))

∣-isPreorder : IsPreorder _≡_ _∣_
∣-isPreorder = record
  { isEquivalence = PropEq.isEquivalence
  ; reflexive     = ∣-reflexive
  ; trans         = ∣-trans
  }

∣-preorder : Preorder _ _ _
∣-preorder = record { isPreorder = ∣-isPreorder }

∣-isPartialOrder : IsPartialOrder _≡_ _∣_
∣-isPartialOrder = record
  { isPreorder = ∣-isPreorder
  ; antisym    = ∣-antisym
  }

poset : Poset _ _ _
poset = record
  { Carrier        = ℕ
  ; _≈_            = _≡_
  ; _≤_            = _∣_
  ; isPartialOrder = ∣-isPartialOrder
  }

module ∣-Reasoning = POR poset
  hiding   (_≈⟨_⟩_)
  renaming (_≤⟨_⟩_ to _∣⟨_⟩_)

------------------------------------------------------------------------
-- Simple properties of _∣_

infix 10 1∣_ _∣0

1∣_ : ∀ n → 1 ∣ n
1∣ n = divides n (sym (*-identityʳ n))

_∣0 : ∀ n → n ∣ 0
n ∣0 = divides 0 refl

n∣n : ∀ {n} → n ∣ n
n∣n = ∣-refl

n∣m*n : ∀ m {n} → n ∣ m * n
n∣m*n m = divides m refl

m∣m*n : ∀ {m} n → m ∣ m * n
m∣m*n n = divides n (*-comm _ n)

0∣⇒≡0 : ∀ {n} → 0 ∣ n → n ≡ 0
0∣⇒≡0 {n} 0∣n = ∣-antisym (n ∣0) 0∣n

∣1⇒≡1 : ∀ {n} → n ∣ 1 → n ≡ 1
∣1⇒≡1 {n} n∣1 = ∣-antisym n∣1 (1∣ n)

------------------------------------------------------------------------
-- Operators and divisibility

module _ where

  open PropEq.≡-Reasoning

  ∣m⇒∣m*n : ∀ {i m} n → i ∣ m → i ∣ m * n
  ∣m⇒∣m*n {i} {m} n (divides q eq) = divides (q * n) $ begin
    m * n       ≡⟨ cong (_* n) eq ⟩
    q * i * n   ≡⟨ *-assoc q i n ⟩
    q * (i * n) ≡⟨ cong (q *_) (*-comm i n) ⟩
    q * (n * i) ≡⟨ sym (*-assoc q n i) ⟩
    q * n * i ∎

  ∣n⇒∣m*n : ∀ {i} m {n} → i ∣ n → i ∣ m * n
  ∣n⇒∣m*n {i} m {n} (divides q eq) = divides (m * q) $ begin
    m * n       ≡⟨ cong (m *_) eq ⟩
    m * (q * i) ≡⟨ sym (*-assoc m q i) ⟩
    m * q * i ∎

  ∣m∣n⇒∣m+n : ∀ {i m n} → i ∣ m → i ∣ n → i ∣ m + n
  ∣m∣n⇒∣m+n (divides p refl) (divides q refl) =
    divides (p + q) (sym (*-distribʳ-+ _ p q))

  ∣m+n∣m⇒∣n : ∀ {i m n} → i ∣ m + n → i ∣ m → i ∣ n
  ∣m+n∣m⇒∣n {i} {m} {n} (divides p m+n≡p*i) (divides q m≡q*i) =
    divides (p ∸ q) $ begin
      n             ≡⟨ sym (m+n∸n≡m n m) ⟩
      n + m ∸ m     ≡⟨ cong (_∸ m) (+-comm n m) ⟩
      m + n ∸ m     ≡⟨ cong₂ _∸_ m+n≡p*i m≡q*i ⟩
      p * i ∸ q * i ≡⟨ sym (*-distribʳ-∸ i p q) ⟩
      (p ∸ q) * i   ∎

  ∣m∸n∣n⇒∣m : ∀ i {m n} → n ≤ m → i ∣ m ∸ n → i ∣ n → i ∣ m
  ∣m∸n∣n⇒∣m i {m} {n} n≤m (divides p m∸n≡p*i) (divides q n≡q*o) =
    divides (p + q) $ begin
      m             ≡⟨ sym (m+n∸m≡n n≤m) ⟩
      n + (m ∸ n)   ≡⟨ +-comm n (m ∸ n) ⟩
      m ∸ n + n     ≡⟨ cong₂ _+_ m∸n≡p*i n≡q*o ⟩
      p * i + q * i ≡⟨ sym (*-distribʳ-+ i p q)  ⟩
      (p + q) * i   ∎

  *-cong : ∀ {i j} k → i ∣ j → k * i ∣ k * j
  *-cong {i} {j} k (divides q j≡q*i) = divides q $ begin
    k * j        ≡⟨ cong (_*_ k) j≡q*i ⟩
    k * (q * i)  ≡⟨ sym (*-assoc k q i) ⟩
    (k * q) * i  ≡⟨ cong (_* i) (*-comm k q) ⟩
    (q * k) * i  ≡⟨ *-assoc q k i ⟩
    q * (k * i)  ∎

  /-cong : ∀ {i j} k → suc k * i ∣ suc k * j → i ∣ j
  /-cong {i} {j} k (divides q eq) =
    divides q (*-cancelʳ-≡ j (q * i) (begin
      j * (suc k)        ≡⟨ *-comm j (suc k) ⟩
      (suc k) * j        ≡⟨ eq ⟩
      q * ((suc k) * i)  ≡⟨ cong (q *_) (*-comm (suc k) i) ⟩
      q * (i * (suc k))  ≡⟨ sym (*-assoc q i (suc k)) ⟩
      (q * i) * (suc k)  ∎))

  m%n≡0⇒n∣m : ∀ m n → m % (suc n) ≡ 0 → suc n ∣ m
  m%n≡0⇒n∣m m n eq = divides (m div (suc n)) (begin
    m                                     ≡⟨ a≡a%n+[a/n]*n m n ⟩
    m % (suc n) + m div (suc n) * (suc n) ≡⟨ cong₂ _+_ eq refl ⟩
    m div (suc n) * (suc n)               ∎)

  n∣m⇒m%n≡0 : ∀ m n → suc n ∣ m → m % (suc n) ≡ 0
  n∣m⇒m%n≡0 m n (divides v eq) = begin
    m           % (suc n) ≡⟨ cong (_% (suc n)) eq ⟩
    (v * suc n) % (suc n) ≡⟨ kn%n≡0 v n ⟩
    0                     ∎

  m%n≡0⇔n∣m : ∀ m n → m % (suc n) ≡ 0 ⇔ suc n ∣ m
  m%n≡0⇔n∣m m n = equivalence (m%n≡0⇒n∣m m n) (n∣m⇒m%n≡0 m n)

-- Divisibility is decidable.

infix 4 _∣?_

_∣?_ : Decidable _∣_
zero  ∣? zero   = yes (0 ∣0)
zero  ∣? suc m  = no ((λ()) ∘′ 0∣⇒≡0)
suc n ∣? m      = Dec.map (m%n≡0⇔n∣m m n) (m % (suc n) ≟ 0)

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

∣-+ = ∣m∣n⇒∣m+n
{-# WARNING_ON_USAGE ∣-+
"Warning: ∣-+ was deprecated in v0.14.
Please use ∣m∣n⇒∣m+n instead."
#-}
∣-∸ = ∣m+n∣m⇒∣n
{-# WARNING_ON_USAGE ∣-∸
"Warning: ∣-∸ was deprecated in v0.14.
Please use ∣m+n∣m⇒∣n instead."
#-}
∣-* = n∣m*n
{-# WARNING_ON_USAGE ∣-*
"Warning: ∣-* was deprecated in v0.14.
Please use n∣m*n instead."
#-}

nonZeroDivisor-lemma : ∀ m q (r : Fin (1 + m)) → toℕ r ≢ 0 →
                       1 + m ∤ toℕ r + q * (1 + m)
nonZeroDivisor-lemma m zero r r≢zero (divides zero eq) = r≢zero $ begin
  toℕ r      ≡⟨ sym (*-identityˡ (toℕ r)) ⟩
  1 * toℕ r  ≡⟨ eq ⟩
  0          ∎
  where open PropEq.≡-Reasoning
nonZeroDivisor-lemma m zero r r≢zero (divides (suc q) eq) =
  i+1+j≰i m $ begin
    m + suc (q * suc m) ≡⟨ +-suc m (q * suc m) ⟩
    suc (m + q * suc m) ≡⟨ sym eq ⟩
    1 * toℕ r           ≡⟨ *-identityˡ (toℕ r) ⟩
    toℕ r               ≤⟨ FP.toℕ≤pred[n] r ⟩
    m                   ∎
  where open ≤-Reasoning
nonZeroDivisor-lemma m (suc q) r r≢zero d =
  nonZeroDivisor-lemma m q r r≢zero (∣m+n∣m⇒∣n d' ∣-refl)
  where
  lem = solve 3 (λ m r q → r :+ (m :+ q)  :=  m :+ (r :+ q))
                refl (suc m) (toℕ r) (q * suc m)
  d' = subst (1 + m ∣_) lem d
{-# WARNING_ON_USAGE nonZeroDivisor-lemma
"Warning: nonZeroDivisor-lemma was deprecated in v0.17."
#-}

ext: agda


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

   Copyright (c) 2020, 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.Prelude
open import LibraBFT.Base.Types
open import LibraBFT.Impl.Base.Types
open import LibraBFT.Abstract.Types.EpochConfig UID NodeId
open WithAbsVote

module LibraBFT.Concrete.Obligations.VotesOnce
  (𝓔 : EpochConfig)
  (𝓥 : VoteEvidence 𝓔)
 where
 open import LibraBFT.Abstract.Abstract      UID _≟UID_ NodeId 𝓔 𝓥
 open import LibraBFT.Concrete.Intermediate                    𝓔 𝓥

 -------------------
 -- * VotesOnce * --
 -------------------

 module _ {ℓ}(𝓢 : IntermediateSystemState ℓ) where
  open IntermediateSystemState 𝓢
  Type : Set ℓ
  Type = ∀{α v v'}
       → Meta-Honest-Member α
       → vMember v  ≡ α → HasBeenSent v
       → vMember v' ≡ α → HasBeenSent v'
       → vRound v ≡ vRound v'
       → vBlockUID v ≡ vBlockUID v'
       -- NOTE: It is interesting that this does not require the timeout signature (or even
       -- presence/lack thereof) to be the same.  The abstract proof goes through without out it, so I
       -- am leaving it out for now, but I'm curious what if anything could go wrong if an honest
       -- author can send different votes for the same epoch and round that differ on timeout
       -- signature.  Maybe something for liveness?

  proof : Type → VotesOnlyOnceRule InSys
  proof glob-inv α hα {q} {q'} q∈sys q'∈sys va va' VO≡
     with ∈QC⇒HasBeenSent q∈sys  hα va
        | ∈QC⇒HasBeenSent q'∈sys hα va'
  ...| sent-cv | sent-cv'
     with glob-inv hα (sym (∈QC-Member q  va))  sent-cv
                      (sym (∈QC-Member q' va')) sent-cv'
                      VO≡
  ...| bId≡
     = Vote-η VO≡ (trans (sym (∈QC-Member q va)) (∈QC-Member q' va'))
                  bId≡

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
------------------------------------------------------------------------------
-- Testing the use of local hints
------------------------------------------------------------------------------

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

module LocalHints where

postulate
  D    : Set
  zero : D

data N : D → Set where
  zN : N zero

postulate 0-N : N zero
{-# ATP prove 0-N zN #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


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

-- Free join semilattice
module Algebra.Construct.Free.Semilattice where

open import Algebra.Construct.Free.Semilattice.Definition public
open import Algebra.Construct.Free.Semilattice.Eliminators public
open import Algebra.Construct.Free.Semilattice.Union public using (_∪_; 𝒦-semilattice)
open import Algebra.Construct.Free.Semilattice.Homomorphism public using (μ; ∙-hom)

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
open import Agda.Primitive
open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality

record R {A : Set} {B : A → Set} p@ab : Set where
  field
    prf : p ≡ p

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
module PreludeList where

open import AlonzoPrelude as Prelude
open import PreludeNat

infixr 50 _::_ _++_

data List (A : Set) : Set where
  []   : List A
  _::_ : A -> List A -> List A

{-# BUILTIN LIST List #-}
{-# BUILTIN NIL  []   #-}
{-# BUILTIN CONS _::_ #-}

[_] : {A : Set} -> A -> List A
[ x ] = x :: []

length : {A : Set} -> List A -> Nat
length []        = 0
length (_ :: xs) = 1 + length xs

map : {A B : Set} -> (A -> B) -> List A -> List B
map f []        = []
map f (x :: xs) = f x :: map f xs

_++_ : {A : Set} -> List A -> List A -> List A
[]        ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

zipWith : {A B C : Set} -> (A -> B -> C) -> List A -> List B -> List C
zipWith f []        []        = []
zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys
zipWith f []        (_ :: _)  = []
zipWith f (_ :: _)  []        = []

foldr : {A B : Set} -> (A -> B -> B) -> B -> List A -> B
foldr f z []        = z
foldr f z (x :: xs) = f x (foldr f z xs)

foldl : {A B : Set} -> (B -> A -> B) -> B -> List A -> B
foldl f z []        = z
foldl f z (x :: xs) = foldl f (f z x) xs

replicate : {A : Set} -> Nat -> A -> List A
replicate  zero   x = []
replicate (suc n) x = x :: replicate n x

iterate : {A : Set} -> Nat -> (A -> A) -> A -> List A
iterate  zero   f x = []
iterate (suc n) f x = x :: iterate n f (f x)

splitAt : {A : Set} -> Nat -> List A -> List A × List A
splitAt  zero   xs        = < [] , xs >
splitAt (suc n) []        = < [] , [] >
splitAt (suc n) (x :: xs) = add x $ splitAt n xs
  where
    add : _ -> List _ × List _ -> List _ × List _
    add x < ys , zs > = < x :: ys , zs >

reverse : {A : Set} -> List A -> List A
reverse xs = foldl (flip _::_) [] xs

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import Categories.Category

module Categories.Functor.Core where

open import Level
open import Function renaming (id to id→; _∘_ to _●_) using ()
open import Relation.Binary hiding (_⇒_)

import Relation.Binary.Reasoning.Setoid as SetoidR

import Categories.Morphism as M

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

record Functor (C : Category o ℓ e) (D : Category o′ ℓ′ e′) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  eta-equality
  private module C = Category C
  private module D = Category D

  field
    F₀ : C.Obj → D.Obj
    F₁ : ∀ {A B} (f : C [ A , B ]) → D [ F₀ A , F₀ B ]

    identity     : ∀ {A} → D [ F₁ (C.id {A}) ≈ D.id ]
    homomorphism : ∀ {X Y Z} {f : C [ X , Y ]} {g : C [ Y , Z ]} →
                     D [ F₁ (C [ g ∘ f ]) ≈ D [ F₁ g ∘ F₁ f ] ]
    F-resp-≈     : ∀ {A B} {f g : C [ A , B ]} → C [ f ≈ g ] → D [ F₁ f ≈ F₁ g ]

  op : Functor C.op D.op
  op = record
    { F₀           = F₀
    ; F₁           = F₁
    ; identity     = identity
    ; homomorphism = homomorphism
    ; F-resp-≈     = F-resp-≈
    }

Endofunctor : Category o ℓ e → Set _
Endofunctor C = Functor C C

id : ∀ {C : Category o ℓ e} → Endofunctor C
id {C = C} = record
  { F₀           = id→
  ; F₁           = id→
  ; identity     = refl
  ; homomorphism = refl
  ; F-resp-≈     = id→
  }
  where open Category.Equiv C

infixr 9 _∘F_

-- note that this definition could be shortened a lot by inlining the definitions for
-- identity′ and homomorphism′, but the definitions below are simpler to understand.
_∘F_ : ∀ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {E : Category o′′ ℓ′′ e′′}
    → Functor D E → Functor C D → Functor C E
_∘F_ {C = C} {D = D} {E = E} F G = record
  { F₀ = F₀ ● G₀
  ; F₁ = F₁ ● G₁
  ; identity = identity′
  ; homomorphism = homomorphism′
  ; F-resp-≈ =  F-resp-≈ ● G-resp-≈
  }
  where
  module C = Category C
  module D = Category D
  module E = Category E
  module F = Functor F
  module G = Functor G
  open F
  open G renaming (F₀ to G₀; F₁ to G₁; F-resp-≈ to G-resp-≈)

  identity′ : ∀ {A} → E [ F₁ (G₁ (C.id {A})) ≈ E.id ]
  identity′ = begin
    F₁ (G₁ C.id) ≈⟨ F-resp-≈ G.identity ⟩
    F₁ D.id      ≈⟨ F.identity ⟩
    E.id         ∎
    where open SetoidR E.hom-setoid

  homomorphism′ : ∀ {X Y Z} {f : C [ X , Y ]} {g : C [ Y , Z ]}
                 → E [ F₁ (G₁ (C [ g ∘ f ])) ≈ E [ F₁ (G₁ g) ∘ F₁ (G₁ f) ] ]
  homomorphism′ {f = f} {g = g} = begin
    F₁ (G₁ (C [ g ∘ f ]))       ≈⟨ F-resp-≈ G.homomorphism ⟩
    F₁ (D [ G₁ g ∘ G₁ f ])      ≈⟨ F.homomorphism ⟩
    E [ F₁ (G₁ g) ∘ F₁ (G₁ f) ] ∎
    where open SetoidR E.hom-setoid

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
module *-comm where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)

open import Induction′ using (+-assoc; +-comm; +-suc)
open import +-swap using (+-swap)

*-comm : ∀ (m n : ℕ) → m * n ≡ n * m
*-comm zero zero = refl
*-comm zero (suc n) =
  begin
    zero * (suc n)
  ≡⟨⟩
    zero
  ≡⟨⟩
    zero + (zero * n)
  ≡⟨ *-comm zero n ⟩
    zero + (n * zero)
  ≡⟨⟩
    (suc n) * zero
  ∎
*-comm (suc m) zero =
  begin
    (suc m) * zero
  ≡⟨⟩
    zero + (m * zero)
  ≡⟨ *-comm m zero ⟩
    (zero * m)
  ≡⟨⟩
    zero
  ≡⟨⟩
    zero * (suc m)
  ∎
*-comm (suc m) (suc n) =
  begin
    (suc m) * (suc n)
  ≡⟨⟩
    (suc n) + (m * (suc n))
  ≡⟨ cong ((suc n) +_) (*-comm m (suc n)) ⟩
    (suc n) + ((suc n) * m)
  ≡⟨⟩
    (suc n) + (m + (n * m))
  ≡⟨ +-swap (suc n) m (n * m) ⟩
    m + ((suc n) + (n * m))
  ≡⟨ sym (+-assoc m (suc n) (n * m)) ⟩
    (m + (suc n)) + (n * m)
  ≡⟨ cong (_+ (n * m)) (+-suc m n) ⟩
    suc (m + n) + (n * m)
  ≡⟨ cong suc (+-assoc m n (n * m)) ⟩
    (suc m) + (n + (n * m))
  ≡⟨ cong (λ m*n → (suc m) + (n + m*n)) (*-comm n m) ⟩
    (suc m) + (n + (m * n))
  ≡⟨⟩
    (suc m) + ((suc m) * n)
  ≡⟨ cong ((suc m) +_) (*-comm ((suc m)) n) ⟩
    (suc m) + (n * (suc m))
  ≡⟨⟩
    (suc n) * (suc m)
  ∎

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
{-

  Maybe structure: X ↦ Maybe (S X)

-}
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Structures.Relational.Maybe where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Foundations.RelationalStructure
open import Cubical.Data.Unit
open import Cubical.Data.Empty
open import Cubical.Data.Maybe
open import Cubical.Data.Sigma

open import Cubical.Structures.Maybe

private
  variable
    ℓ ℓ₁ ℓ₁' : Level

-- Structured relations

preservesSetsMaybe : {S : Type ℓ → Type ℓ₁} → preservesSets S → preservesSets (MaybeStructure S)
preservesSetsMaybe p setX = isOfHLevelMaybe 0 (p setX)

MaybeRelStr : {S : Type ℓ → Type ℓ₁} {ℓ₁' : Level}
  → StrRel S ℓ₁' → StrRel (λ X → Maybe (S X)) ℓ₁'
MaybeRelStr ρ R = MaybeRel (ρ R)

open SuitableStrRel

maybeSuitableRel : {S : Type ℓ → Type ℓ₁} {ρ : StrRel S ℓ₁'}
  → SuitableStrRel S ρ
  → SuitableStrRel (MaybeStructure S) (MaybeRelStr ρ)
maybeSuitableRel θ .quo (X , nothing) R _ .fst = nothing , _
maybeSuitableRel θ .quo (X , nothing) R _ .snd (nothing , _) = refl
maybeSuitableRel θ .quo (X , just s) R c .fst =
  just (θ .quo (X , s) R c .fst .fst) , θ .quo (X , s) R c .fst .snd
maybeSuitableRel θ .quo (X , just s) R c .snd (just s' , r) =
  cong (λ {(t , r') → just t , r'}) (θ .quo (X , s) R c .snd (s' , r))
maybeSuitableRel θ .symmetric R {nothing} {nothing} r = _
maybeSuitableRel θ .symmetric R {just s} {just t} r = θ .symmetric R r
maybeSuitableRel θ .transitive R R' {nothing} {nothing} {nothing} r r' = _
maybeSuitableRel θ .transitive R R' {just s} {just t} {just u} r r' = θ .transitive R R' r r'
maybeSuitableRel θ .prop propR nothing nothing = isOfHLevelLift 1 isPropUnit
maybeSuitableRel θ .prop propR nothing (just y) = isOfHLevelLift 1 isProp⊥
maybeSuitableRel θ .prop propR (just x) nothing = isOfHLevelLift 1 isProp⊥
maybeSuitableRel θ .prop propR (just x) (just y) = θ .prop propR x y

maybeRelMatchesEquiv : {S : Type ℓ → Type ℓ₁} (ρ : StrRel S ℓ₁') {ι : StrEquiv S ℓ₁'}
  → StrRelMatchesEquiv ρ ι
  → StrRelMatchesEquiv (MaybeRelStr ρ) (MaybeEquivStr ι)
maybeRelMatchesEquiv ρ μ (X , nothing) (Y , nothing) _ = idEquiv _
maybeRelMatchesEquiv ρ μ (X , nothing) (Y , just y) _ = idEquiv _
maybeRelMatchesEquiv ρ μ (X , just x) (Y , nothing) _ = idEquiv _
maybeRelMatchesEquiv ρ μ (X , just x) (Y , just y) = μ (X , x) (Y , y)

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


text:
{-# OPTIONS --sized-types #-}

module SizedTypesVarSwap where

postulate
  Size : Set
  _^   : Size -> Size
  ∞    : Size

{-# BUILTIN SIZE Size  #-}
{-# BUILTIN SIZESUC _^ #-}
{-# BUILTIN SIZEINF ∞  #-}

data Nat : {size : Size} -> Set where
  zero : {size : Size} -> Nat {size ^}
  suc  : {size : Size} -> Nat {size} -> Nat {size ^}

bad : {i j : Size} -> Nat {i} -> Nat {j} -> Nat {∞}
bad (suc x) y = bad (suc y) x
bad zero y = y


text:
module Pi.Opsem where
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Base
open import Pi.Syntax

infix  1  _↦_

-- Base combinators
base : ∀ {A B} (c : A ↔ B) → Set
base unite₊l = ⊤
base uniti₊l = ⊤
base swap₊ = ⊤
base assocl₊ = ⊤
base assocr₊ = ⊤
base unite⋆l = ⊤
base uniti⋆l = ⊤
base swap⋆ = ⊤
base assocl⋆ = ⊤
base assocr⋆ = ⊤
base absorbr = ⊤
base factorzl = ⊤
base dist = ⊤
base factor = ⊤
base _ = ⊥

base-is-prop : ∀ {A B} (c : A ↔ B) → is-prop (base c)
base-is-prop unite₊l tt tt = refl
base-is-prop uniti₊l tt tt = refl
base-is-prop swap₊ tt tt = refl
base-is-prop assocl₊ tt tt = refl
base-is-prop assocr₊ tt tt = refl
base-is-prop unite⋆l tt tt = refl
base-is-prop uniti⋆l tt tt = refl
base-is-prop swap⋆ tt tt = refl
base-is-prop assocl⋆ tt tt = refl
base-is-prop assocr⋆ tt tt = refl
base-is-prop absorbr tt tt = refl
base-is-prop factorzl tt tt = refl
base-is-prop dist tt tt = refl
base-is-prop factor tt tt = refl

-- Evaluator for base combinators
δ : ∀ {A B} (c : A ↔ B) {_ : base c} → ⟦ A ⟧ → ⟦ B ⟧
δ unite₊l (inj₂ v) = v
δ uniti₊l v = inj₂ v
δ swap₊ (inj₁ x) = inj₂ x
δ swap₊ (inj₂ y) = inj₁ y
δ assocl₊ (inj₁ v) = inj₁ (inj₁ v)
δ assocl₊ (inj₂ (inj₁ v)) = inj₁ (inj₂ v)
δ assocl₊ (inj₂ (inj₂ v)) = inj₂ v
δ assocr₊ (inj₁ (inj₁ v)) = inj₁ v
δ assocr₊ (inj₁ (inj₂ v)) = inj₂ (inj₁ v)
δ assocr₊ (inj₂ v) = inj₂ (inj₂ v)
δ unite⋆l (tt , v) = v
δ uniti⋆l v = (tt , v)
δ swap⋆ (x , y) = (y , x)
δ assocl⋆ (v₁ , (v₂ , v₃)) = ((v₁ , v₂) , v₃)
δ assocr⋆ ((v₁ , v₂) , v₃) = (v₁ , (v₂ , v₃))
δ absorbr ()
δ factorzl ()
δ dist (inj₁ v₁ , v₃) = inj₁ (v₁ , v₃)
δ dist (inj₂ v₂ , v₃) = inj₂ (v₂ , v₃)
δ factor (inj₁ (v₁ , v₃)) = (inj₁ v₁ , v₃)
δ factor (inj₂ (v₂ , v₃)) = (inj₂ v₂ , v₃)

-- Context
data Context : {A B : 𝕌} → Set where
  ☐ : ∀ {A B} → Context {A} {B}
  ☐⨾_•_ : ∀ {A B C} → (c₂ : B ↔ C) → Context {A} {C} → Context {A} {B}
  _⨾☐•_ : ∀ {A B C} → (c₁ : A ↔ B) → Context {A} {C} → Context {B} {C}
  ☐⊕_•_ : ∀ {A B C D} → (c₂ : C ↔ D) → Context {A +ᵤ C} {B +ᵤ D} → Context {A} {B}
  _⊕☐•_ : ∀ {A B C D} → (c₁ : A ↔ B) → Context {A +ᵤ C} {B +ᵤ D} → Context {C} {D}
  ☐⊗[_,_]•_ : ∀ {A B C D} → (c₂ : C ↔ D) → ⟦ C ⟧ → Context {A ×ᵤ C} {B ×ᵤ D} → Context {A} {B}
  [_,_]⊗☐•_ : ∀ {A B C D} → (c₁ : A ↔ B) → ⟦ B ⟧ → Context {A ×ᵤ C} {B ×ᵤ D} → Context {C} {D}

-- Machine state
data State : Set where
  ⟨_∣_∣_⟩ : ∀ {A B} → (c : A ↔ B) → ⟦ A ⟧ → Context {A} {B} → State
  ［_∣_∣_］ : ∀ {A B} → (c : A ↔ B) → ⟦ B ⟧ → Context {A} {B} → State

-- Reduction relation
data _↦_ : State → State → Set where
  ↦₁  : ∀ {A B} {c : A ↔ B} {b : base c} {v : ⟦ A ⟧} {κ : Context} → ⟨ c ∣ v ∣ κ ⟩ ↦ ［ c ∣ δ c {b} v ∣ κ ］
  ↦₂  : ∀ {A} {v : ⟦ A ⟧} {κ : Context} → ⟨ id↔ ∣ v ∣ κ ⟩ ↦ ［ id↔ ∣ v ∣ κ ］
  ↦₃  : ∀ {A B C} {c₁ : A ↔ B} {c₂ : B ↔ C} {v : ⟦ A ⟧} {κ : Context}
      → ⟨ c₁ ⨾ c₂ ∣ v ∣ κ ⟩ ↦ ⟨ c₁ ∣ v ∣ ☐⨾ c₂ • κ ⟩
  ↦₄  : ∀ {A B C D} {c₁ : A ↔ B} {c₂ : C ↔ D} {x : ⟦ A ⟧} {κ : Context}
      → ⟨ c₁ ⊕ c₂ ∣ inj₁ x ∣ κ ⟩ ↦ ⟨ c₁ ∣ x ∣ ☐⊕ c₂ • κ ⟩
  ↦₅  : ∀ {A B C D} {c₁ : A ↔ B} {c₂ : C ↔ D} {y : ⟦ C ⟧} {κ : Context}
      → ⟨ c₁ ⊕ c₂ ∣ inj₂ y ∣ κ ⟩ ↦ ⟨ c₂ ∣ y ∣ c₁ ⊕☐• κ ⟩
  ↦₆  : ∀ {A B C D} {c₁ : A ↔ B} {c₂ : C ↔ D} {x : ⟦ A ⟧} {y : ⟦ C ⟧} {κ : Context}
      → ⟨ c₁ ⊗ c₂ ∣ (x , y) ∣ κ ⟩ ↦ ⟨ c₁ ∣ x ∣ ☐⊗[ c₂ , y ]• κ ⟩
  ↦₇  : ∀ {A B C} {c₁ : A ↔ B} {c₂ : B ↔ C} {v : ⟦ B ⟧} {κ : Context}
      → ［ c₁ ∣ v ∣ ☐⨾ c₂ • κ ］ ↦ ⟨ c₂ ∣ v ∣ (c₁ ⨾☐• κ) ⟩
  ↦₈  : ∀ {A B C D} {c₁ : A ↔ B} {c₂ : C ↔ D} {x : ⟦ B ⟧} {y : ⟦ C ⟧} {κ : Context}
      → ［ c₁ ∣ x ∣ ☐⊗[ c₂ , y ]• κ ］ ↦ ⟨ c₂ ∣ y ∣ [ c₁ , x ]⊗☐• κ ⟩
  ↦₉  : ∀ {A B C D} {c₁ : A ↔ B} {c₂ : C ↔ D} {x : ⟦ B ⟧} {y : ⟦ D ⟧} {κ : Context}
      → ［ c₂ ∣ y ∣ [ c₁ , x ]⊗☐• κ ］ ↦ ［ c₁ ⊗ c₂ ∣ (x , y) ∣ κ ］
  ↦₁₀ : ∀ {A B C} {c₁ : A ↔ B} {c₂ : B ↔ C} {v : ⟦ C ⟧} {κ : Context}
      → ［ c₂ ∣ v ∣ (c₁ ⨾☐• κ) ］ ↦ ［ c₁ ⨾ c₂ ∣ v ∣ κ ］
  ↦₁₁ : ∀ {A B C D} {c₁ : A ↔ B} {c₂ : C ↔ D} {x : ⟦ B ⟧} {κ : Context}
      → ［ c₁ ∣ x ∣ ☐⊕ c₂ • κ ］ ↦ ［ c₁ ⊕ c₂ ∣ inj₁ x ∣ κ ］
  ↦₁₂ : ∀ {A B C D} {c₁ : A ↔ B} {c₂ : C ↔ D} {y : ⟦ D ⟧} {κ : Context}
      → ［ c₂ ∣ y ∣ c₁ ⊕☐• κ ］ ↦ ［ c₁ ⊕ c₂ ∣ inj₂ y ∣ κ ］


text:
------------------------------------------------------------------------
-- Atoms
------------------------------------------------------------------------

module Atom where

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

open import Bag-equivalence equality-with-J
open import Bijection equality-with-J as Bijection using (_↔_)
open import Equality.Decidable-UIP equality-with-J
open import Equality.Path.Isomorphisms.Univalence equality-with-paths
open import Equivalence equality-with-J as Eq using (_≃_)
open import Finite-subset.Listed equality-with-paths as S
  using (Finite-subset-of; _∉_)
open import Function-universe equality-with-J hiding (id)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional equality-with-paths
  using (∥_∥; ∣_∣)
open import Injection equality-with-J using (Injective)
import Nat equality-with-J as Nat
open import Univalence-axiom equality-with-J

-- Atoms.

record Atoms : Type₁ where
  field
    -- The type of atoms.

    Name : Type

    -- The type must be countably infinite.

    countably-infinite : Name ↔ ℕ

  -- Atoms have decidable equality.

  _≟_ : Decidable-equality Name
  _≟_ = Bijection.decidable-equality-respects
          (inverse countably-infinite) Nat._≟_

  -- Membership test.

  member : (x : Name) (xs : List Name) → Dec (x ∈ xs)
  member x []       = no (λ ())
  member x (y ∷ xs) with x ≟ y
  ... | yes x≡y = yes (inj₁ x≡y)
  ... | no  x≢y with member x xs
  ...   | yes x∈xs = yes (inj₂ x∈xs)
  ...   | no  x∉xs = no [ x≢y , x∉xs ]

  -- Conversions.

  name : ℕ → Name
  name = _↔_.from countably-infinite

  code : Name → ℕ
  code = _↔_.to countably-infinite

  -- The name function is injective.

  name-injective : Injective name
  name-injective = _↔_.injective (inverse countably-infinite)

  -- Distinct natural numbers are mapped to distinct names.

  distinct-codes→distinct-names : ∀ {m n} → m ≢ n → name m ≢ name n
  distinct-codes→distinct-names {m} {n} m≢n =
    name m ≡ name n  ↝⟨ name-injective ⟩
    m ≡ n            ↝⟨ m≢n ⟩□
    ⊥                □

  -- One can always find a name that is distinct from the names in a
  -- given finite set of names.

  fresh :
    (ns : Finite-subset-of Name) →
    ∃ λ (n : Name) → n ∉ ns
  fresh ns =
    Σ-map name
      (λ {m} →
         →-cong-→
           (name m S.∈ ns                        ↝⟨ (λ ∈ns → ∣ name m , ∈ns
                                                             , _↔_.right-inverse-of countably-infinite _
                                                             ∣) ⟩
            ∥ (∃ λ n → n S.∈ ns × code n ≡ m) ∥  ↔⟨ inverse S.∈map≃ ⟩□
            m S.∈ S.map code ns                  □)
           id)
      (S.fresh (S.map code ns))

  -- Name is a set.

  Name-set : Is-set Name
  Name-set = decidable⇒set _≟_

-- One implementation of atoms, using natural numbers.

ℕ-atoms : Atoms
Atoms.Name               ℕ-atoms = ℕ
Atoms.countably-infinite ℕ-atoms = Bijection.id

-- Two sets of atoms, one for constants and one for variables.

record χ-atoms : Type₁ where
  field
    const-atoms var-atoms : Atoms

  module C = Atoms const-atoms renaming (Name to Const)
  module V = Atoms var-atoms   renaming (Name to Var)

  open C public using (Const)
  open V public using (Var)

-- One implementation of χ-atoms, using natural numbers.

χ-ℕ-atoms : χ-atoms
χ-atoms.const-atoms χ-ℕ-atoms = ℕ-atoms
χ-atoms.var-atoms   χ-ℕ-atoms = ℕ-atoms

-- The type of atoms is isomorphic to the unit type.

Atoms↔⊤ : Atoms ↔ ⊤
Atoms↔⊤ =
  Atoms                           ↝⟨ eq ⟩
  (∃ λ (Name : Type) → Name ↔ ℕ)  ↝⟨ ∃-cong (λ _ → Eq.↔↔≃′ ext ℕ-set) ⟩
  (∃ λ (Name : Type) → Name ≃ ℕ)  ↝⟨ singleton-with-≃-↔-⊤ ext univ ⟩□
  ⊤                               □
  where
  open Atoms

  eq : Atoms ↔ ∃ λ (Name : Type) → Name ↔ ℕ
  eq = record
    { surjection = record
      { logical-equivalence = record
        { to   = λ a → Name a , countably-infinite a
        ; from = uncurry λ N c →
                   record { Name = N; countably-infinite = c }
        }
      ; right-inverse-of = λ _ → refl
      }
    ; left-inverse-of = λ _ → refl
    }

-- The χ-atoms type is isomorphic to the unit type.

χ-atoms↔⊤ : χ-atoms ↔ ⊤
χ-atoms↔⊤ =
  χ-atoms        ↝⟨ eq ⟩
  Atoms × Atoms  ↝⟨ Atoms↔⊤ ×-cong Atoms↔⊤ ⟩
  ⊤ × ⊤          ↝⟨ ×-right-identity ⟩□
  ⊤              □
  where
  open χ-atoms

  eq : χ-atoms ↔ Atoms × Atoms
  eq = record
    { surjection = record
      { logical-equivalence = record
        { to   = λ a → const-atoms a , var-atoms a
        ; from = uncurry λ c v →
                   record { const-atoms = c; var-atoms = v }
        }
      ; right-inverse-of = λ _ → refl
      }
    ; left-inverse-of = λ _ → refl
    }

-- If a property holds for one choice of atoms, then it holds for any
-- other choice of atoms.

invariant :
  ∀ {p} (P : χ-atoms → Type p) →
  ∀ a₁ a₂ → P a₁ → P a₂
invariant P a₁ a₂ =
  subst P (mono₁ 0 (_⇔_.from contractible⇔↔⊤ χ-atoms↔⊤) a₁ a₂)

-- If a property holds for χ-ℕ-atoms, then it holds for any choice of
-- atoms.

one-can-restrict-attention-to-χ-ℕ-atoms :
  ∀ {p} (P : χ-atoms → Type p) →
  P χ-ℕ-atoms → ∀ a → P a
one-can-restrict-attention-to-χ-ℕ-atoms P p a =
  invariant P χ-ℕ-atoms a p

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi


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

open import Level using (Level)

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import Data.Nat using (ℕ; zero; suc)
open import Data.Vec using (Vec; []; _∷_; _++_; foldr; map; replicate)
open import Data.Vec.Properties

open import FLA.Algebra.Structures
open import FLA.Algebra.Properties.Field
open import FLA.Algebra.LinearAlgebra
open import FLA.Data.Vec.Properties

module FLA.Algebra.LinearAlgebra.Properties where

private
  variable
    ℓ : Level
    A : Set ℓ
    m n p q : ℕ

module _ ⦃ F : Field A ⦄ where
  open Field F

  +ⱽ-assoc : (v₁ v₂ v₃ : Vec A n)
           → v₁ +ⱽ v₂ +ⱽ v₃ ≡ v₁ +ⱽ (v₂ +ⱽ v₃)
  +ⱽ-assoc [] [] [] = refl
  +ⱽ-assoc (v₁ ∷ vs₁) (v₂ ∷ vs₂) (v₃ ∷ vs₃) rewrite
      +ⱽ-assoc vs₁ vs₂ vs₃
    | +-assoc v₁ v₂ v₃
      = refl

  +ⱽ-comm : (v₁ v₂ : Vec A n) → v₁ +ⱽ v₂ ≡ v₂ +ⱽ v₁
  +ⱽ-comm [] [] = refl
  +ⱽ-comm (x₁ ∷ vs₁) (x₂ ∷ vs₂) =
    begin
      x₁ + x₂ ∷ vs₁ +ⱽ vs₂ ≡⟨ cong ((x₁ + x₂) ∷_) (+ⱽ-comm vs₁ vs₂) ⟩
      x₁ + x₂ ∷ vs₂ +ⱽ vs₁ ≡⟨ cong (_∷ vs₂ +ⱽ vs₁) (+-comm x₁ x₂) ⟩
      x₂ + x₁ ∷ vs₂ +ⱽ vs₁ ∎

  v+0ᶠⱽ≡v : (v : Vec A n) → v +ⱽ (replicate 0ᶠ) ≡ v
  v+0ᶠⱽ≡v [] = refl
  v+0ᶠⱽ≡v (v ∷ vs) = cong₂ _∷_ (+0ᶠ v) (v+0ᶠⱽ≡v vs)

  0ᶠⱽ+v≡v : (v : Vec A n) → (replicate 0ᶠ) +ⱽ v ≡ v
  0ᶠⱽ+v≡v v = trans (+ⱽ-comm (replicate 0ᶠ) v) (v+0ᶠⱽ≡v v)

  0ᶠ∘ⱽv≡0ᶠⱽ : (v : Vec A n) → 0ᶠ ∘ⱽ v ≡ replicate 0ᶠ
  0ᶠ∘ⱽv≡0ᶠⱽ [] = refl
  0ᶠ∘ⱽv≡0ᶠⱽ (v ∷ vs) = cong₂ _∷_ (0ᶠ*a≡0ᶠ v) (0ᶠ∘ⱽv≡0ᶠⱽ vs)

  c∘ⱽ0ᶠⱽ≡0ᶠⱽ : {n : ℕ} → (c : A) → c ∘ⱽ replicate {n = n} 0ᶠ ≡ replicate 0ᶠ
  c∘ⱽ0ᶠⱽ≡0ᶠⱽ {zero} c = refl
  c∘ⱽ0ᶠⱽ≡0ᶠⱽ {suc n} c = cong₂ _∷_ (a*0ᶠ≡0ᶠ c) (c∘ⱽ0ᶠⱽ≡0ᶠⱽ c)

  v*ⱽ0ᶠⱽ≡0ᶠⱽ : {n : ℕ} → (v : Vec A n) → v *ⱽ replicate 0ᶠ ≡ replicate 0ᶠ
  v*ⱽ0ᶠⱽ≡0ᶠⱽ [] = refl
  v*ⱽ0ᶠⱽ≡0ᶠⱽ (v ∷ vs) = cong₂ _∷_ (a*0ᶠ≡0ᶠ v) (v*ⱽ0ᶠⱽ≡0ᶠⱽ vs)

  map-*c-≡c∘ⱽ : (c : A) (v : Vec A n) → map (_* c) v ≡ c ∘ⱽ v
  map-*c-≡c∘ⱽ c [] = refl
  map-*c-≡c∘ⱽ c (v ∷ vs) = cong₂ _∷_ (*-comm v c) (map-*c-≡c∘ⱽ c vs)

  replicate-distr-+ : {n : ℕ} → (u v : A)
                    → replicate {n = n} (u + v) ≡ replicate u +ⱽ replicate v
  replicate-distr-+ u v = sym (zipWith-replicate _+_ u v)

  -- This should work for any linear function (I think), instead of just -_,
  *ⱽ-map--ⱽ : (a v : Vec A n)
            → a *ⱽ (map -_ v) ≡ map -_ (a *ⱽ v)
  *ⱽ-map--ⱽ [] [] = refl
  *ⱽ-map--ⱽ (a ∷ as) (v ∷ vs) = begin
      (a ∷ as) *ⱽ map -_ (v ∷ vs)
    ≡⟨⟩
      (a * - v) ∷ (as *ⱽ map -_ vs)
    ≡⟨ cong ((a * - v) ∷_) (*ⱽ-map--ⱽ as vs) ⟩
      (a * - v) ∷ (map -_ (as *ⱽ vs))
    ≡⟨ cong (_∷ (map -_ (as *ⱽ vs))) (a*-b≡-[a*b] a v) ⟩
      (- (a * v)) ∷ (map -_ (as *ⱽ vs))
    ≡⟨⟩
      map -_ ((a ∷ as) *ⱽ (v ∷ vs))
    ∎

  -ⱽ≡-1ᶠ∘ⱽ : (v : Vec A n) → map -_ v ≡ (- 1ᶠ) ∘ⱽ v
  -ⱽ≡-1ᶠ∘ⱽ [] = refl
  -ⱽ≡-1ᶠ∘ⱽ (v ∷ vs) = begin
      map -_ (v ∷ vs)           ≡⟨⟩
      (- v) ∷ map -_ vs         ≡⟨ cong₂ (_∷_) (-a≡-1ᶠ*a v) (-ⱽ≡-1ᶠ∘ⱽ vs) ⟩
      (- 1ᶠ * v) ∷ (- 1ᶠ) ∘ⱽ vs ≡⟨⟩
      (- 1ᶠ) ∘ⱽ (v ∷ vs)        ∎

  *ⱽ-assoc : (v₁ v₂ v₃ : Vec A n)
           → v₁ *ⱽ v₂ *ⱽ v₃ ≡ v₁ *ⱽ (v₂ *ⱽ v₃)
  *ⱽ-assoc [] [] [] = refl
  *ⱽ-assoc (v₁ ∷ vs₁) (v₂ ∷ vs₂) (v₃ ∷ vs₃) rewrite
      *ⱽ-assoc vs₁ vs₂ vs₃
    | *-assoc v₁ v₂ v₃
    = refl

  *ⱽ-comm : (v₁ v₂ : Vec A n) → v₁ *ⱽ v₂ ≡ v₂ *ⱽ v₁
  *ⱽ-comm [] [] = refl
  *ⱽ-comm (v₁ ∷ vs₁) (v₂ ∷ vs₂) rewrite
      *ⱽ-comm vs₁ vs₂
    | *-comm v₁ v₂
    = refl

  *ⱽ-distr-+ⱽ : (a u v : Vec A n)
              → a *ⱽ (u +ⱽ v) ≡ a *ⱽ u +ⱽ a *ⱽ v
  *ⱽ-distr-+ⱽ [] [] [] = refl
  *ⱽ-distr-+ⱽ (a ∷ as) (u ∷ us) (v ∷ vs) rewrite
      *ⱽ-distr-+ⱽ as us vs
    | *-distr-+ a u v
    = refl

  *ⱽ-distr--ⱽ : (a u v : Vec A n)
              → a *ⱽ (u -ⱽ v) ≡ a *ⱽ u -ⱽ a *ⱽ v
  *ⱽ-distr--ⱽ a u v = begin
    a *ⱽ (u -ⱽ v)               ≡⟨⟩
    a *ⱽ (u +ⱽ (map (-_) v))    ≡⟨ *ⱽ-distr-+ⱽ a u (map -_ v) ⟩
    a *ⱽ u +ⱽ a *ⱽ (map -_ v)   ≡⟨ cong (a *ⱽ u +ⱽ_) (*ⱽ-map--ⱽ a v) ⟩
    a *ⱽ u +ⱽ (map -_ (a *ⱽ v)) ≡⟨⟩
    a *ⱽ u -ⱽ a *ⱽ v            ∎

  -- Homogeneity of degree 1 for linear maps
  *ⱽ∘ⱽ≡∘ⱽ*ⱽ : (c : A) (u v : Vec A n)
            → u *ⱽ c ∘ⱽ v ≡ c ∘ⱽ (u *ⱽ v)
  *ⱽ∘ⱽ≡∘ⱽ*ⱽ c [] [] = refl
  *ⱽ∘ⱽ≡∘ⱽ*ⱽ c (u ∷ us) (v ∷ vs) rewrite
      *ⱽ∘ⱽ≡∘ⱽ*ⱽ c us vs
    | *-assoc u c v
    | *-comm u c
    | sym (*-assoc c u v)
    = refl

  ∘ⱽ*ⱽ-assoc : (c : A) (u v : Vec A n)
             → c ∘ⱽ (u *ⱽ v) ≡ (c ∘ⱽ u) *ⱽ v
  ∘ⱽ*ⱽ-assoc c [] [] = refl
  ∘ⱽ*ⱽ-assoc c (u ∷ us) (v ∷ vs) = cong₂ (_∷_) (*-assoc c u v)
                                               (∘ⱽ*ⱽ-assoc c us vs)

  ∘ⱽ-distr-+ⱽ : (c : A) (u v : Vec A n)
              → c ∘ⱽ (u +ⱽ v) ≡ c ∘ⱽ u +ⱽ c ∘ⱽ v
  ∘ⱽ-distr-+ⱽ c [] [] = refl
  ∘ⱽ-distr-+ⱽ c (u ∷ us) (v ∷ vs) rewrite
      ∘ⱽ-distr-+ⱽ c us vs
    | *-distr-+ c u v
    = refl

  ∘ⱽ-comm : (a b : A) (v : Vec A n) → a ∘ⱽ (b ∘ⱽ v) ≡ b ∘ⱽ (a ∘ⱽ v)
  ∘ⱽ-comm a b [] = refl
  ∘ⱽ-comm a b (v ∷ vs) = cong₂ _∷_ (trans (trans (*-assoc a b v)
                                          (cong (_* v) (*-comm a b)))
                                          (sym (*-assoc b a v)))
                                   (∘ⱽ-comm a b vs)

  +ⱽ-flip-++ : (a b : Vec A n) → (c d : Vec A m)
             → (a ++ c) +ⱽ (b ++ d) ≡ a +ⱽ b ++ c +ⱽ d
  +ⱽ-flip-++ [] [] c d = refl
  +ⱽ-flip-++ (a ∷ as) (b ∷ bs) c d rewrite +ⱽ-flip-++ as bs c d = refl

  ∘ⱽ-distr-++ : (c : A) (a : Vec A n) (b : Vec A m)
              → c ∘ⱽ (a ++ b) ≡ (c ∘ⱽ a) ++ (c ∘ⱽ b)
  ∘ⱽ-distr-++ c [] b = refl
  ∘ⱽ-distr-++ c (a ∷ as) b rewrite ∘ⱽ-distr-++ c as b = refl

  replicate[a*b]≡a∘ⱽreplicate[b] : {n : ℕ} (a b : A) →
                                   replicate {n = n} (a * b) ≡ a ∘ⱽ replicate b
  replicate[a*b]≡a∘ⱽreplicate[b] {n = n} a b = sym (map-replicate (a *_) b n)

  replicate[a*b]≡b∘ⱽreplicate[a] : {n : ℕ} (a b : A) →
                                   replicate {n = n} (a * b) ≡ b ∘ⱽ replicate a
  replicate[a*b]≡b∘ⱽreplicate[a] a b = trans (cong replicate (*-comm a b))
                                             (replicate[a*b]≡a∘ⱽreplicate[b] b a)

  sum[0ᶠⱽ]≡0ᶠ : {n : ℕ} → sum (replicate {n = n} 0ᶠ) ≡ 0ᶠ
  sum[0ᶠⱽ]≡0ᶠ {n = zero} = refl
  sum[0ᶠⱽ]≡0ᶠ {n = suc n} = begin
      sum (0ᶠ ∷ replicate {n = n} 0ᶠ) ≡⟨⟩
      0ᶠ + sum (replicate {n = n} 0ᶠ) ≡⟨ cong (0ᶠ +_) (sum[0ᶠⱽ]≡0ᶠ {n})  ⟩
      0ᶠ + 0ᶠ                         ≡⟨ 0ᶠ+0ᶠ≡0ᶠ ⟩
      0ᶠ                              ∎

  sum-distr-+ⱽ : (v₁ v₂ : Vec A n) → sum (v₁ +ⱽ v₂) ≡ sum v₁ + sum v₂
  sum-distr-+ⱽ [] [] = sym (0ᶠ+0ᶠ≡0ᶠ)
  sum-distr-+ⱽ (v₁ ∷ vs₁) (v₂ ∷ vs₂) rewrite
      sum-distr-+ⱽ vs₁ vs₂
    | +-assoc (v₁ + v₂) (foldr (λ v → A) _+_ 0ᶠ vs₁) (foldr (λ v → A) _+_ 0ᶠ vs₂)
    | sym (+-assoc v₁ v₂ (foldr (λ v → A) _+_ 0ᶠ vs₁))
    | +-comm v₂ (foldr (λ v → A) _+_ 0ᶠ vs₁)
    | +-assoc v₁ (foldr (λ v → A) _+_ 0ᶠ vs₁) v₂
    | sym (+-assoc (v₁ + (foldr (λ v → A) _+_ 0ᶠ vs₁)) v₂ (foldr (λ v → A) _+_ 0ᶠ vs₂))
    = refl

  sum[c∘ⱽv]≡c*sum[v] : (c : A) (v : Vec A n) → sum (c ∘ⱽ v) ≡ c * sum v
  sum[c∘ⱽv]≡c*sum[v] c [] = sym (a*0ᶠ≡0ᶠ c)
  sum[c∘ⱽv]≡c*sum[v] c (v ∷ vs) = begin
      sum (c ∘ⱽ (v ∷ vs))   ≡⟨⟩
      c * v + sum (c ∘ⱽ vs) ≡⟨ cong (c * v +_) (sum[c∘ⱽv]≡c*sum[v] c vs) ⟩
      c * v + c * sum vs    ≡⟨ sym (*-distr-+ c v (sum vs)) ⟩
      c * (v + sum vs)      ≡⟨⟩
      c * sum (v ∷ vs)      ∎

  ⟨⟩-comm : (v₁ v₂ : Vec A n)
          → ⟨ v₁ , v₂ ⟩ ≡ ⟨ v₂ , v₁ ⟩
  ⟨⟩-comm v₁ v₂ = cong sum (*ⱽ-comm v₁ v₂)

  -- Should we show bilinearity?
  --   ∀ λ ∈ F, B(λv, w) ≡ B(v, λw) ≡ λB(v, w)
  --   B(v₁ + v₂, w) ≡ B(v₁, w) + B(v₂, w) ∧ B(v, w₁ + w₂) ≡ B(v, w₁) + B(v, w₂)
  -- Additivity in both arguments
  ⟨x+y,z⟩≡⟨x,z⟩+⟨y,z⟩ : (x y z : Vec A n)
                      → ⟨ x +ⱽ y , z ⟩ ≡ (⟨ x , z ⟩) + (⟨ y , z ⟩)
  ⟨x+y,z⟩≡⟨x,z⟩+⟨y,z⟩ x y z = begin
    ⟨ x +ⱽ y , z ⟩
    ≡⟨⟩
    sum ((x +ⱽ y) *ⱽ z )
    ≡⟨ cong sum (*ⱽ-comm (x +ⱽ y) z) ⟩
    sum (z *ⱽ (x +ⱽ y))
    ≡⟨ cong sum (*ⱽ-distr-+ⱽ z x y) ⟩
    sum (z *ⱽ x +ⱽ z *ⱽ y)
    ≡⟨ sum-distr-+ⱽ (z *ⱽ x) (z *ⱽ y) ⟩
    sum (z *ⱽ x) + sum (z *ⱽ y)
    ≡⟨⟩
    ⟨ z , x ⟩ + ⟨ z , y ⟩
    ≡⟨ cong (_+ ⟨ z , y ⟩) (⟨⟩-comm z x) ⟩
    ⟨ x , z ⟩ + ⟨ z , y ⟩
    ≡⟨ cong (⟨ x , z ⟩ +_ ) (⟨⟩-comm z y) ⟩
    ⟨ x , z ⟩ + ⟨ y , z ⟩
    ∎

  ⟨x,y+z⟩≡⟨x,y⟩+⟨x,z⟩ : (x y z : Vec A n)
                      → ⟨ x , y +ⱽ z ⟩ ≡ (⟨ x , y ⟩) + (⟨ x , z ⟩)
  ⟨x,y+z⟩≡⟨x,y⟩+⟨x,z⟩ x y z =
    begin
      ⟨ x , y +ⱽ z ⟩        ≡⟨ ⟨⟩-comm x (y +ⱽ z) ⟩
      ⟨ y +ⱽ z , x ⟩        ≡⟨ ⟨x+y,z⟩≡⟨x,z⟩+⟨y,z⟩ y z x ⟩
      ⟨ y , x ⟩ + ⟨ z , x ⟩ ≡⟨ cong (_+ ⟨ z , x ⟩) (⟨⟩-comm y x) ⟩
      ⟨ x , y ⟩ + ⟨ z , x ⟩ ≡⟨ cong (⟨ x , y ⟩ +_ ) (⟨⟩-comm z x) ⟩
      ⟨ x , y ⟩ + ⟨ x , z ⟩ ∎

  ⟨a++b,c++d⟩≡⟨a,c⟩+⟨b,d⟩ : (a : Vec A m) → (b : Vec A n) → (c : Vec A m) → (d : Vec A n)
                          → ⟨ a ++ b , c ++ d ⟩ ≡ ⟨ a , c ⟩ + ⟨ b ,  d ⟩
  ⟨a++b,c++d⟩≡⟨a,c⟩+⟨b,d⟩ [] b [] d rewrite 0ᶠ+ (⟨ b , d ⟩) = refl
  ⟨a++b,c++d⟩≡⟨a,c⟩+⟨b,d⟩ (a ∷ as) b (c ∷ cs) d =
    begin
        ⟨ a ∷ as ++ b , c ∷ cs ++ d ⟩
      ≡⟨⟩
        (a * c) + ⟨ as ++ b , cs ++ d ⟩
      ≡⟨ cong ((a * c) +_) (⟨a++b,c++d⟩≡⟨a,c⟩+⟨b,d⟩ as b cs d) ⟩
        (a * c) + (⟨ as , cs ⟩ + ⟨ b , d ⟩)
      ≡⟨ +-assoc (a * c) ⟨ as , cs ⟩ ⟨ b , d ⟩ ⟩
        ((a * c) + ⟨ as , cs ⟩) + ⟨ b , d ⟩
      ≡⟨⟩
        ⟨ a ∷ as , c ∷ cs ⟩ + ⟨ b , d ⟩
    ∎

  ⟨a,b⟩+⟨c,d⟩≡⟨a++c,b++d⟩ : (a b : Vec A m) → (c d : Vec A n)
                          → ⟨ a , b ⟩ + ⟨ c ,  d ⟩ ≡ ⟨ a ++ c , b ++ d ⟩
  ⟨a,b⟩+⟨c,d⟩≡⟨a++c,b++d⟩ a b c d = sym (⟨a++b,c++d⟩≡⟨a,c⟩+⟨b,d⟩ a c b d)

max_stars_repo_name: turion/functional-linear-algebra

max_issues_repo_name: turion/functional-linear-algebra

max_forks_repo_name: turion/functional-linear-algebra


text:
module Problem1 where

-- 1.1

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

-- 1.2

infixl 60 _+_

_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

-- 1.3

infixl 70 _*_

_*_ : Nat -> Nat -> Nat
zero  * m = zero
suc n * m = m + n * m

-- 1.4

infix 30 _==_

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

cong : {A B : Set}(f : A -> B){x y : A} -> x == y -> f x == f y
cong f refl = refl

assoc : (x y z : Nat) -> x + (y + z) == (x + y) + z
assoc zero    y z = refl
assoc (suc x) y z = cong suc (assoc x y z)

-- Alternative solution using 'with'. Note that in order
-- to be able to pattern match on the induction hypothesis
-- we have to abstract (using with) over the left hand side
-- of the equation.

assoc' : (x y z : Nat) -> x + (y + z) == (x + y) + z
assoc' zero    y z = refl
assoc' (suc x) y z with x + (y + z) | assoc x y z
...                | .((x + y) + z) | refl = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Solver for monoid equalities
------------------------------------------------------------------------

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

open import Algebra

module Algebra.Solver.Monoid {m₁ m₂} (M : Monoid m₁ m₂) where

open import Data.Fin as Fin hiding (_≟_)
import Data.Fin.Properties as Fin
open import Data.List.Base hiding (lookup)
import Data.List.Relation.Binary.Equality.DecPropositional as ListEq
open import Data.Maybe as Maybe
  using (Maybe; decToMaybe; From-just; from-just)
open import Data.Nat.Base using (ℕ)
open import Data.Product
open import Data.Vec using (Vec; lookup)
open import Function using (_∘_; _$_)
open import Relation.Binary using (Decidable)

open import Relation.Binary.PropositionalEquality as P using (_≡_)
import Relation.Binary.Reflection
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec

open Monoid M
open import Relation.Binary.Reasoning.Setoid setoid

------------------------------------------------------------------------
-- Monoid expressions

-- There is one constructor for every operation, plus one for
-- variables; there may be at most n variables.

infixr 5 _⊕_

data Expr (n : ℕ) : Set where
  var : Fin n → Expr n
  id  : Expr n
  _⊕_ : Expr n → Expr n → Expr n

-- An environment contains one value for every variable.

Env : ℕ → Set _
Env n = Vec Carrier n

-- The semantics of an expression is a function from an environment to
-- a value.

⟦_⟧ : ∀ {n} → Expr n → Env n → Carrier
⟦ var x   ⟧ ρ = lookup ρ x
⟦ id      ⟧ ρ = ε
⟦ e₁ ⊕ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ

------------------------------------------------------------------------
-- Normal forms

-- A normal form is a list of variables.

Normal : ℕ → Set
Normal n = List (Fin n)

-- The semantics of a normal form.

⟦_⟧⇓ : ∀ {n} → Normal n → Env n → Carrier
⟦ []     ⟧⇓ ρ = ε
⟦ x ∷ nf ⟧⇓ ρ = lookup ρ x ∙ ⟦ nf ⟧⇓ ρ

-- A normaliser.

normalise : ∀ {n} → Expr n → Normal n
normalise (var x)   = x ∷ []
normalise id        = []
normalise (e₁ ⊕ e₂) = normalise e₁ ++ normalise e₂

-- The normaliser is homomorphic with respect to _++_/_∙_.

homomorphic : ∀ {n} (nf₁ nf₂ : Normal n) (ρ : Env n) →
              ⟦ nf₁ ++ nf₂ ⟧⇓ ρ ≈ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ)
homomorphic [] nf₂ ρ = begin
  ⟦ nf₂ ⟧⇓ ρ      ≈⟨ sym $ identityˡ _ ⟩
  ε ∙ ⟦ nf₂ ⟧⇓ ρ  ∎
homomorphic (x ∷ nf₁) nf₂ ρ = begin
  lookup ρ x ∙ ⟦ nf₁ ++ nf₂ ⟧⇓ ρ          ≈⟨ ∙-congˡ (homomorphic nf₁ nf₂ ρ) ⟩
  lookup ρ x ∙ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ)  ≈⟨ sym $ assoc _ _ _ ⟩
  lookup ρ x ∙ ⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ    ∎

-- The normaliser preserves the semantics of the expression.

normalise-correct :
  ∀ {n} (e : Expr n) (ρ : Env n) → ⟦ normalise e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ
normalise-correct (var x) ρ = begin
  lookup ρ x ∙ ε  ≈⟨ identityʳ _ ⟩
  lookup ρ x      ∎
normalise-correct id ρ = begin
  ε  ∎
normalise-correct (e₁ ⊕ e₂) ρ = begin
  ⟦ normalise e₁ ++ normalise e₂ ⟧⇓ ρ        ≈⟨ homomorphic (normalise e₁) (normalise e₂) ρ ⟩
  ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ  ≈⟨ ∙-cong (normalise-correct e₁ ρ) (normalise-correct e₂ ρ) ⟩
  ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ                        ∎

------------------------------------------------------------------------
-- "Tactics"

open module R = Relation.Binary.Reflection
                  setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) normalise-correct
  public using (solve; _⊜_)

-- We can decide if two normal forms are /syntactically/ equal.

infix 5 _≟_

_≟_ : ∀ {n} → Decidable {A = Normal n} _≡_
nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂)
  where open ListEq Fin._≟_

-- We can also give a sound, but not necessarily complete, procedure
-- for determining if two expressions have the same semantics.

prove′ : ∀ {n} (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ)
prove′ e₁ e₂ =
  Maybe.map lemma $ decToMaybe (normalise e₁ ≟ normalise e₂)
  where
  lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
  lemma eq ρ =
    R.prove ρ e₁ e₂ (begin
      ⟦ normalise e₁ ⟧⇓ ρ  ≡⟨ P.cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩
      ⟦ normalise e₂ ⟧⇓ ρ  ∎)

-- This procedure can be combined with from-just.

prove : ∀ n (es : Expr n × Expr n) →
        From-just (uncurry prove′ es)
prove _ = from-just ∘ uncurry prove′


text:
open import Oscar.Prelude
open import Oscar.Data.¶
open import Oscar.Data.Fin
open import Oscar.Data.Term

module Oscar.Data.Substitunction where

module Substitunction {𝔭} (𝔓 : Ø 𝔭) where

  open Term 𝔓

  Substitunction : ¶ → ¶ → Ø 𝔭
  Substitunction m n = ¶⟨< m ⟩ → Term n

module SubstitunctionOperator {𝔭} (𝔓 : Ø 𝔭) where

  open Substitunction 𝔓

  _⊸_ = Substitunction


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

open import Cubical.Core.Everything
open import Cubical.Foundations.HLevels

module Cubical.Algebra.Magma.Construct.Free {ℓ} (Aˢ : hSet ℓ) where

open import Cubical.Foundations.Prelude
open import Cubical.Algebra.Magma

open import Cubical.Data.Empty.Polymorphic
open import Cubical.Data.Prod

A = ⟨ Aˢ ⟩
isSetA = Aˢ .snd

------------------------------------------------------------------------
-- The free magma type

data FreeM : Type ℓ where
  inj : A → FreeM
  _•_ : Op₂ FreeM

------------------------------------------------------------------------
-- Proof the free magma is a set

module FreeMPath where
  Cover : FreeM → FreeM → Type ℓ
  Cover (inj x) (inj y) = x ≡ y
  Cover (inj x) (y₁ • y₂) = ⊥
  Cover (x₁ • x₂) (inj y) = ⊥
  Cover (x₁ • x₂) (y₁ • y₂) = Cover x₁ y₁ × Cover x₂ y₂

  isPropCover : ∀ x y → isProp (Cover x y)
  isPropCover (inj x) (inj y) = isSetA x y
  isPropCover (inj x) (y₁ • y₂) = isProp⊥
  isPropCover (x₁ • x₂) (inj y) = isProp⊥
  isPropCover (x₁ • x₂) (y₁ • y₂) = isPropProd (isPropCover x₁ y₁) (isPropCover x₂ y₂)

  reflCover : ∀ x → Cover x x
  reflCover (inj x) = refl
  reflCover (x • y) = reflCover x , reflCover y

  encode : ∀ x y → x ≡ y → Cover x y
  encode x _ = J (λ y _ → Cover x y) (reflCover x)

  encodeRefl : ∀ x → encode x x refl ≡ reflCover x
  encodeRefl x = JRefl (λ y _ → Cover x y) (reflCover x)

  decode : ∀ x y → Cover x y → x ≡ y
  decode (inj x) (inj y) p = cong inj p
  decode (inj x) (y₁ • y₂) ()
  decode (x₁ • x₂) (inj y) ()
  decode (x₁ • x₂) (y₁ • y₂) (p , q) = cong₂ _•_ (decode x₁ y₁ p) (decode x₂ y₂ q)

  decodeRefl : ∀ x → decode x x (reflCover x) ≡ refl
  decodeRefl (inj x) = refl
  decodeRefl (x • y) i j = decodeRefl x i j • decodeRefl y i j

  decodeEncode : ∀ x y → (p : x ≡ y) → decode x y (encode x y p) ≡ p
  decodeEncode x _ =
    J (λ y p → decode x y (encode x y p) ≡ p)
      (cong (decode x x) (encodeRefl x) ? decodeRefl x)

isSetFreeM : isSet FreeM
isSetFreeM x y =
  isOfHLevelRetract 1
    (FreeMPath.encode x y)
    (FreeMPath.decode x y)
    (FreeMPath.decodeEncode x y)
    (FreeMPath.isPropCover x y)

------------------------------------------------------------------------
-- The free magma

FreeM-isMagma : IsMagma FreeM _•_
FreeM-isMagma = record { is-set = isSetFreeM }

FreeMagma : Magma ℓ
FreeMagma = record { isMagma = FreeM-isMagma }


text:
open import SOAS.Common
open import SOAS.Families.Core
open import Categories.Object.Initial
open import SOAS.Coalgebraic.Strength
import SOAS.Metatheory.MetaAlgebra

-- Traversals parametrised by a pointed coalgebra
module SOAS.Metatheory.Traversal {T : Set}
  (⅀F : Functor 𝔽amiliesₛ 𝔽amiliesₛ) (⅀:Str : Strength ⅀F)
  (𝔛 : Familyₛ) (open SOAS.Metatheory.MetaAlgebra ⅀F 𝔛)
  (𝕋:Init : Initial 𝕄etaAlgebras)
  where

open import SOAS.Context
open import SOAS.Variable
open import SOAS.Abstract.Hom
import SOAS.Abstract.Coalgebra as →□ ; open →□.Sorted
import SOAS.Abstract.Box as □ ; open □.Sorted

open import SOAS.Metatheory.Algebra ⅀F
open import SOAS.Metatheory.Semantics ⅀F ⅀:Str 𝔛 𝕋:Init

open Strength ⅀:Str

private
  variable
    Γ Δ Θ Π : Ctx
    α β : T
    𝒫 𝒬 𝒜 : Familyₛ

-- Parametrised interpretation into an internal hom
module Traversal (𝒫ᴮ : Coalgₚ 𝒫)(𝑎𝑙𝑔 : ⅀ 𝒜 ⇾̣ 𝒜)
                 (φ : 𝒫 ⇾̣ 𝒜)(χ : 𝔛 ⇾̣ 〖 𝒜 , 𝒜 〗) where

  open Coalgₚ 𝒫ᴮ

  -- Under the assumptions 𝒜 and 〖 𝒫 , 𝒜 〗 are both meta-algebras
  𝒜ᵃ : MetaAlg 𝒜
  𝒜ᵃ = record { 𝑎𝑙𝑔 = 𝑎𝑙𝑔 ; 𝑣𝑎𝑟 = λ x → φ (η x) ; 𝑚𝑣𝑎𝑟 = χ }

  Travᵃ : MetaAlg 〖 𝒫 , 𝒜 〗
  Travᵃ = record
    { 𝑎𝑙𝑔  = λ t σ → 𝑎𝑙𝑔 (str 𝒫ᴮ 𝒜 t σ)
    ; 𝑣𝑎𝑟  = λ x σ → φ (σ x)
    ; 𝑚𝑣𝑎𝑟 = λ 𝔪 ε σ → χ 𝔪 (λ 𝔫 → ε 𝔫 σ)
    }

  -- 〖 𝒫 , 𝒜 〗 is also a pointed □-coalgebra
  Travᵇ : Coalg 〖 𝒫 , 𝒜 〗
  Travᵇ = record { r = λ h ρ σ → h (σ ∘ ρ) ; counit = refl ; comult = refl }

  Travᴮ : Coalgₚ 〖 𝒫 , 𝒜 〗
  Travᴮ = record { ᵇ = Travᵇ ; η = λ x σ → φ (σ x) ; r∘η = refl }

  open Semantics Travᵃ public renaming (𝕤𝕖𝕞 to 𝕥𝕣𝕒𝕧)

  -- Traversal-specific homomorphism properties that incorporate a substitution
  𝕥⟨𝕧⟩ : {σ : Γ ~[ 𝒫 ]↝ Δ}{x : ℐ α Γ} → 𝕥𝕣𝕒𝕧 (𝕧𝕒𝕣 x) σ ≡ φ (σ x)
  𝕥⟨𝕧⟩ {σ = σ} = cong (λ - → - σ) ⟨𝕧⟩

  𝕥⟨𝕞⟩ : {σ : Γ ~[ 𝒫 ]↝ Δ}{𝔪 : 𝔛 α Π}{ε : Π ~[ 𝕋 ]↝ Γ}
       → 𝕥𝕣𝕒𝕧 (𝕞𝕧𝕒𝕣 𝔪 ε) σ ≡ χ 𝔪 (λ p → 𝕥𝕣𝕒𝕧 (ε p) σ)
  𝕥⟨𝕞⟩ {σ = σ} = cong (λ - → - σ) ⟨𝕞⟩

  𝕥⟨𝕒⟩ : {σ : Γ ~[ 𝒫 ]↝ Δ}{t : ⅀ 𝕋 α Γ}
       → 𝕥𝕣𝕒𝕧 (𝕒𝕝𝕘 t) σ ≡ 𝑎𝑙𝑔 (str 𝒫ᴮ 𝒜 (⅀₁ 𝕥𝕣𝕒𝕧 t) σ)
  𝕥⟨𝕒⟩ {σ = σ} = cong (λ - → - σ) ⟨𝕒⟩

  -- Congruence in the two arguments of 𝕥𝕣𝕒𝕧
  𝕥≈₁ : {σ : Γ ~[ 𝒫 ]↝ Δ}{t₁ t₂ : 𝕋 α Γ} → t₁ ≡ t₂ → 𝕥𝕣𝕒𝕧 t₁ σ ≡ 𝕥𝕣𝕒𝕧 t₂ σ
  𝕥≈₁ {σ = σ} p = cong (λ - → 𝕥𝕣𝕒𝕧 - σ) p

  𝕥≈₂ : {σ₁ σ₂ : Γ ~[ 𝒫 ]↝ Δ}{t : 𝕋 α Γ}
      → ({τ : T}{x : ℐ τ Γ} → σ₁ x ≡ σ₂ x)
      → 𝕥𝕣𝕒𝕧 t σ₁ ≡ 𝕥𝕣𝕒𝕧 t σ₂
  𝕥≈₂ {t = t} p = cong (𝕥𝕣𝕒𝕧 t) (dext′ p)

-- A pointed meta-Λ-algebra induces 𝕒𝕝𝕘 traversal into □ 𝒜
module □Traversal {𝒜} (𝒜ᵃ : MetaAlg 𝒜) =
  Traversal ℐᴮ (MetaAlg.𝑎𝑙𝑔 𝒜ᵃ) (MetaAlg.𝑣𝑎𝑟 𝒜ᵃ) (MetaAlg.𝑚𝑣𝑎𝑟 𝒜ᵃ)

-- Corollary: □ lifts to an endofunctor on pointed meta-Λ-algebras
□ᵃ : (𝒜ᵃ : MetaAlg 𝒜) → MetaAlg (□ 𝒜)
□ᵃ = □Traversal.Travᵃ

-- Helper records for proving equality of maps f, g out of 𝕋,
-- with 0, 1 or 2 parameters
record MapEq₀ (𝒜 : Familyₛ)(f g : 𝕋 ⇾̣ 𝒜) : Set where
  field
    ᵃ : MetaAlg 𝒜
  open Semantics ᵃ
  open 𝒜

  field
    f⟨𝑣⟩ : {x : ℐ α Γ}
         → f (𝕧𝕒𝕣 x) ≡ 𝑣𝑎𝑟 x
    f⟨𝑚⟩ : {𝔪 : 𝔛 α Π}{ε : Π ~[ 𝕋 ]↝ Γ}
         → f (𝕞𝕧𝕒𝕣 𝔪 ε) ≡ 𝑚𝑣𝑎𝑟 𝔪 (f ∘ ε)
    f⟨𝑎⟩ : {t : ⅀ 𝕋 α Γ}
         → f (𝕒𝕝𝕘 t) ≡ 𝑎𝑙𝑔 (⅀₁ f t)
    g⟨𝑣⟩ : {x : ℐ α Γ}
         → g (𝕧𝕒𝕣 x) ≡ 𝑣𝑎𝑟 x
    g⟨𝑚⟩ : {𝔪 : 𝔛 α Π}{ε : Π ~[ 𝕋 ]↝ Γ}
         → g (𝕞𝕧𝕒𝕣 𝔪 ε) ≡ 𝑚𝑣𝑎𝑟 𝔪 (g ∘ ε)
    g⟨𝑎⟩ : {t : ⅀ 𝕋 α Γ}
         → g (𝕒𝕝𝕘 t) ≡ 𝑎𝑙𝑔 (⅀₁ g t)

  fᵃ : MetaAlg⇒ 𝕋ᵃ ᵃ f
  fᵃ = record { ⟨𝑎𝑙𝑔⟩ =  f⟨𝑎⟩ ; ⟨𝑣𝑎𝑟⟩ =  f⟨𝑣⟩ ; ⟨𝑚𝑣𝑎𝑟⟩ =  f⟨𝑚⟩ }
  gᵃ : MetaAlg⇒ 𝕋ᵃ ᵃ g
  gᵃ = record { ⟨𝑎𝑙𝑔⟩ =  g⟨𝑎⟩ ; ⟨𝑣𝑎𝑟⟩ =  g⟨𝑣⟩ ; ⟨𝑚𝑣𝑎𝑟⟩ =  g⟨𝑚⟩ }

  ≈ : (t : 𝕋 α Γ) → f t ≡ g t
  ≈ t = eq fᵃ gᵃ t

record MapEq₁ (𝒫ᴮ : Coalgₚ 𝒫)(𝑎𝑙𝑔 : ⅀ 𝒜 ⇾̣ 𝒜)
              (f g : 𝕋 ⇾̣ 〖 𝒫 , 𝒜 〗) : Set where
  field
    φ : 𝒫 ⇾̣ 𝒜
    χ : 𝔛 ⇾̣ 〖 𝒜 , 𝒜 〗

  open Traversal 𝒫ᴮ 𝑎𝑙𝑔 φ χ

  field
    f⟨𝑣⟩ : {σ : Γ ~[ 𝒫 ]↝ Δ}{x : ℐ α Γ}
         → f (𝕧𝕒𝕣 x) σ ≡ φ (σ x)
    f⟨𝑚⟩ : {σ : Γ ~[ 𝒫 ]↝ Δ}{𝔪 : 𝔛 α Π}{ε : Π ~[ 𝕋 ]↝ Γ}
         → f (𝕞𝕧𝕒𝕣 𝔪 ε) σ ≡ χ 𝔪 (λ p → f (ε p) σ)
    f⟨𝑎⟩ : {σ : Γ ~[ 𝒫 ]↝ Δ}{t : ⅀ 𝕋 α Γ}
         → f (𝕒𝕝𝕘 t) σ ≡ 𝑎𝑙𝑔 (str 𝒫ᴮ 𝒜 (⅀₁ f t) σ)
    g⟨𝑣⟩ : {σ : Γ ~[ 𝒫 ]↝ Δ}{x : ℐ α Γ}
         → g (𝕧𝕒𝕣 x) σ ≡ φ (σ x)
    g⟨𝑚⟩ : {σ : Γ ~[ 𝒫 ]↝ Δ}{𝔪 : 𝔛 α Π}{ε : Π ~[ 𝕋 ]↝ Γ}
         → g (𝕞𝕧𝕒𝕣 𝔪 ε) σ ≡ χ 𝔪 (λ p → g (ε p) σ)
    g⟨𝑎⟩ : {σ : Γ ~[ 𝒫 ]↝ Δ}{t : ⅀ 𝕋 α Γ}
         → g (𝕒𝕝𝕘 t) σ ≡ 𝑎𝑙𝑔 (str 𝒫ᴮ 𝒜 (⅀₁ g t) σ)

  fᵃ : MetaAlg⇒ 𝕋ᵃ Travᵃ f
  fᵃ = record { ⟨𝑎𝑙𝑔⟩ = dext′ f⟨𝑎⟩ ; ⟨𝑣𝑎𝑟⟩ = dext′ f⟨𝑣⟩ ; ⟨𝑚𝑣𝑎𝑟⟩ = dext′ f⟨𝑚⟩ }
  gᵃ : MetaAlg⇒ 𝕋ᵃ Travᵃ g
  gᵃ = record { ⟨𝑎𝑙𝑔⟩ = dext′ g⟨𝑎⟩ ; ⟨𝑣𝑎𝑟⟩ = dext′ g⟨𝑣⟩ ; ⟨𝑚𝑣𝑎𝑟⟩ = dext′ g⟨𝑚⟩ }

  ≈ : {σ : Γ ~[ 𝒫 ]↝ Δ}(t : 𝕋 α Γ) → f t σ ≡ g t σ
  ≈ {σ = σ} t = cong (λ - → - σ) (eq fᵃ gᵃ t)

record MapEq₂ (𝒫ᴮ : Coalgₚ 𝒫)(𝒬ᴮ : Coalgₚ 𝒬)(𝑎𝑙𝑔 : ⅀ 𝒜 ⇾̣ 𝒜)
                (f g : 𝕋 ⇾̣ 〖 𝒫 , 〖 𝒬 , 𝒜 〗 〗) : Set where
  field
    φ : 𝒬 ⇾̣ 𝒜
    ϕ : 𝒫 ⇾̣ 〖 𝒬 , 𝒜 〗
    χ : 𝔛 ⇾̣ 〖 𝒜 , 𝒜 〗

  open Traversal 𝒫ᴮ (Traversal.𝒜.𝑎𝑙𝑔 𝒬ᴮ 𝑎𝑙𝑔 φ χ) ϕ (λ 𝔪 ε σ → χ 𝔪 (λ 𝔫 → ε 𝔫 σ))

  field
    f⟨𝑣⟩ : {σ : Γ ~[ 𝒫 ]↝ Δ}{ς : Δ ~[ 𝒬 ]↝ Θ}{x : ℐ α Γ}
         → f (𝕧𝕒𝕣 x) σ ς ≡ ϕ (σ x) ς
    f⟨𝑚⟩ : {σ : Γ ~[ 𝒫 ]↝ Δ}{ς : Δ ~[ 𝒬 ]↝ Θ}{𝔪 : 𝔛 α Π}{ε : Π ~[ 𝕋 ]↝ Γ}
         → f (𝕞𝕧𝕒𝕣 𝔪 ε) σ ς ≡ χ 𝔪 (λ 𝔫 → f (ε 𝔫) σ ς)
    f⟨𝑎⟩ : {σ : Γ ~[ 𝒫 ]↝ Δ}{ς : Δ ~[ 𝒬 ]↝ Θ}{t : ⅀ 𝕋 α Γ}
         → f (𝕒𝕝𝕘 t) σ ς ≡ 𝑎𝑙𝑔 (str 𝒬ᴮ 𝒜 (str 𝒫ᴮ 〖 𝒬 , 𝒜 〗 (⅀₁ f t) σ) ς)
    g⟨𝑣⟩ : {σ : Γ ~[ 𝒫 ]↝ Δ}{ς : Δ ~[ 𝒬 ]↝ Θ}{x : ℐ α Γ}
         → g (𝕧𝕒𝕣 x) σ ς ≡ ϕ (σ x) ς
    g⟨𝑚⟩ : {σ : Γ ~[ 𝒫 ]↝ Δ}{ς : Δ ~[ 𝒬 ]↝ Θ}{𝔪 : 𝔛 α Π}{ε : Π ~[ 𝕋 ]↝ Γ}
         → g (𝕞𝕧𝕒𝕣 𝔪 ε) σ ς ≡ χ 𝔪 (λ 𝔫 → g (ε 𝔫) σ ς)
    g⟨𝑎⟩ : {σ : Γ ~[ 𝒫 ]↝ Δ}{ς : Δ ~[ 𝒬 ]↝ Θ}{t : ⅀ 𝕋 α Γ}
         → g (𝕒𝕝𝕘 t) σ ς ≡ 𝑎𝑙𝑔 (str 𝒬ᴮ 𝒜 (str 𝒫ᴮ 〖 𝒬 , 𝒜 〗 (⅀₁ g t) σ) ς)

  fᵃ : MetaAlg⇒ 𝕋ᵃ Travᵃ f
  fᵃ = record { ⟨𝑎𝑙𝑔⟩ = dext′ (dext′ f⟨𝑎⟩) ; ⟨𝑣𝑎𝑟⟩ = dext′ (dext′ f⟨𝑣⟩)
              ; ⟨𝑚𝑣𝑎𝑟⟩ = dext′ (dext′ f⟨𝑚⟩) }
  gᵃ : MetaAlg⇒ 𝕋ᵃ Travᵃ g
  gᵃ = record { ⟨𝑎𝑙𝑔⟩ = dext′ (dext′ g⟨𝑎⟩) ; ⟨𝑣𝑎𝑟⟩ = dext′ (dext′ g⟨𝑣⟩)
              ; ⟨𝑚𝑣𝑎𝑟⟩ = dext′ (dext′ g⟨𝑚⟩) }

  ≈ : {σ : Γ ~[ 𝒫 ]↝ Δ}{ς : Δ ~[ 𝒬 ]↝ Θ}(t : 𝕋 α Γ) → f t σ ς ≡ g t σ ς
  ≈ {σ = σ}{ς} t = cong (λ - → - σ ς) (eq fᵃ gᵃ t)

-- Interaction of traversal and interpretation
module _ (𝒫ᴮ : Coalgₚ 𝒫)(𝒜ᵃ : MetaAlg 𝒜)(φ : 𝒫 ⇾̣ 𝒜) where
  open MetaAlg 𝒜ᵃ
  open Coalgₚ 𝒫ᴮ
  open Semantics 𝒜ᵃ
  open Traversal 𝒫ᴮ 𝑎𝑙𝑔 φ 𝑚𝑣𝑎𝑟 using (𝕥𝕣𝕒𝕧 ; 𝕥⟨𝕒⟩ ; 𝕥⟨𝕧⟩ ; 𝕥⟨𝕞⟩)
  open ≡-Reasoning

  -- Traversal with the point of 𝒫 is the same as direct interpretation
  𝕥𝕣𝕒𝕧-η≈𝕤𝕖𝕞 : (φ∘η≈𝑣𝑎𝑟 : ∀{α Γ}{v : ℐ α Γ} → φ (η v) ≡ 𝑣𝑎𝑟 v){t : 𝕋 α Γ}
        → 𝕥𝕣𝕒𝕧 t η ≡ 𝕤𝕖𝕞 t
  𝕥𝕣𝕒𝕧-η≈𝕤𝕖𝕞 φ∘η≈𝑣𝑎𝑟 {t = t} = Semantics.eq 𝒜ᵃ (record
    { ⟨𝑎𝑙𝑔⟩ = λ{ {t = t} → trans 𝕥⟨𝕒⟩ (cong 𝑎𝑙𝑔 (begin
          str 𝒫ᴮ 𝒜 (⅀₁ 𝕥𝕣𝕒𝕧 t) η
      ≡⟨ str-nat₁ (ηᴮ⇒ 𝒫ᴮ) (⅀₁ 𝕥𝕣𝕒𝕧 t) id ⟩
          str ℐᴮ 𝒜 (⅀₁ (λ{ h ρ → h (η ∘ ρ)}) ((⅀₁ 𝕥𝕣𝕒𝕧 t))) id
      ≡⟨ str-unit 𝒜 ((⅀₁ (λ{ h ρ → h (η ∘ ρ)}) ((⅀₁ 𝕥𝕣𝕒𝕧 t)))) ⟩
          ⅀₁ (i 𝒜) (⅀₁ (λ { h ρ → h (η ∘ ρ) }) (⅀₁ 𝕥𝕣𝕒𝕧 t))
      ≡˘⟨ trans ⅀.homomorphism ⅀.homomorphism ⟩
          ⅀₁ (λ t → 𝕥𝕣𝕒𝕧 t η) t
      ∎))}
    ; ⟨𝑣𝑎𝑟⟩ = λ{ {v = v} → trans 𝕥⟨𝕧⟩ φ∘η≈𝑣𝑎𝑟 }
    ; ⟨𝑚𝑣𝑎𝑟⟩ = λ{ {𝔪}{ε} → 𝕥⟨𝕞⟩ } }) 𝕤𝕖𝕞ᵃ⇒ t

-- Traversal with the point of 𝒫 into 𝕋  is the identity
𝕥𝕣𝕒𝕧-η≈id : (𝒫ᴮ : Coalgₚ 𝒫)(open Coalgₚ 𝒫ᴮ)(φ : 𝒫 ⇾̣ 𝕋)
          (φ∘η≈𝑣𝑎𝑟 : ∀{α Γ}{v : ℐ α Γ} → φ (η v) ≡ 𝕧𝕒𝕣 v){t : 𝕋 α Γ}
         → Traversal.𝕥𝕣𝕒𝕧 𝒫ᴮ 𝕒𝕝𝕘 φ 𝕞𝕧𝕒𝕣 t η ≡ t
𝕥𝕣𝕒𝕧-η≈id 𝒫ᴮ φ φ∘η≈𝑣𝑎𝑟 = trans (𝕥𝕣𝕒𝕧-η≈𝕤𝕖𝕞 𝒫ᴮ 𝕋ᵃ φ φ∘η≈𝑣𝑎𝑟) 𝕤𝕖𝕞-id

-- Corollaries for ℐ-parametrised traversals
□𝕥𝕣𝕒𝕧-id≈𝕤𝕖𝕞 : (𝒜ᵃ : MetaAlg 𝒜){t : 𝕋 α Γ}
            → □Traversal.𝕥𝕣𝕒𝕧 𝒜ᵃ t id ≡ Semantics.𝕤𝕖𝕞 𝒜ᵃ t
□𝕥𝕣𝕒𝕧-id≈𝕤𝕖𝕞 𝒜ᵃ {t} = 𝕥𝕣𝕒𝕧-η≈𝕤𝕖𝕞 ℐᴮ 𝒜ᵃ (MetaAlg.𝑣𝑎𝑟 𝒜ᵃ) refl

□𝕥𝕣𝕒𝕧-id≈id : {t : 𝕋 α Γ} → □Traversal.𝕥𝕣𝕒𝕧 𝕋ᵃ t id ≡ t
□𝕥𝕣𝕒𝕧-id≈id = 𝕥𝕣𝕒𝕧-η≈id ℐᴮ 𝕧𝕒𝕣 refl


text:
module Category.Functor.Const where
open import Category.Functor     using (RawFunctor    ; module RawFunctor    )
open import Category.Functor.Lawful
open import Relation.Binary.PropositionalEquality using (refl)

Const : ∀ {l₁ l₂} (R : Set l₂) (_ : Set l₁) → Set l₂
Const R _ = R

constFunctor : ∀ {l₁} {R : Set l₁} → RawFunctor (Const {l₁} R)
constFunctor = record { _<$>_ = λ _ z → z }

constLawfulFunctor : ∀ {l₁} {R : Set l₁} → LawfulFunctorImp (constFunctor {l₁} {R})
constLawfulFunctor = record { <$>-identity = refl ; <$>-compose = refl }

max_stars_repo_name: crisoagf/agda-optics

max_issues_repo_name: crisoagf/agda-optics

max_forks_repo_name: crisoagf/agda-optics


text:
module MLib.Algebra.PropertyCode where

open import MLib.Prelude
open import MLib.Finite

open import MLib.Algebra.PropertyCode.RawStruct public
open import MLib.Algebra.PropertyCode.Core as Core public
  using (Property; Properties; Code; IsSubcode; _∈ₚ_; _⇒ₚ_; ⟦_⟧P)
  renaming (⇒ₚ-weaken to weaken)

open Core.PropKind public
open Core.PropertyC using (_on_; _is_for_; _⟨_⟩ₚ_) public

import Relation.Unary as U using (Decidable)
open import Relation.Binary as B using (Setoid)

open import Data.List.All as All using (All; _∷_; []) public
open import Data.List.Any using (Any; here; there)
open import Data.Bool using (_∨_)

open import Category.Applicative

record Struct {k} (code : Code k) c ℓ : Set (sucˡ (c ⊔ˡ ℓ ⊔ˡ k)) where
  open Code code public

  field
    rawStruct : RawStruct K c ℓ
    Π : Properties code

  open RawStruct rawStruct public

  open Properties Π public

  field
    reify : ∀ {π} → π ∈ₚ Π → ⟦ π ⟧P rawStruct

  Hasₚ : (Π′ : Properties code) → Set
  Hasₚ Π′ = Π′ ⇒ₚ Π

  Has : List (Property K) → Set
  Has = Hasₚ ∘ Core.fromList

  Has₁ : Property K → Set
  Has₁ π = Hasₚ (Core.singleton π)

  use : ∀ π ⦃ hasπ : π ∈ₚ Π ⦄ → ⟦ π ⟧P rawStruct
  use _ ⦃ hasπ ⦄ = reify hasπ

  from : ∀ {Π′} (hasΠ′ : Hasₚ Π′) π ⦃ hasπ : π ∈ₚ Π′ ⦄ → ⟦ π ⟧P rawStruct
  from hasΠ′ _ ⦃ hasπ ⦄ = use _ ⦃ Core.⇒ₚ-MP hasπ hasΠ′ ⦄

  substruct : ∀ {k′} {code′ : Code k′} → IsSubcode code′ code → Struct code′ c ℓ
  substruct isSub = record
    { rawStruct = record
      { Carrier = Carrier
      ; _≈_ = _≈_
      ; appOp = appOp ∘ Core.subK→supK isSub
      ; isRawStruct = isRawStruct′
      }
    ; Π = Core.subcodeProperties isSub Π
    ; reify = Core.reinterpret isSub rawStruct isRawStruct′ _ ∘ reify ∘ Core.fromSubcode isSub
    }
    where
    isRawStruct′ = record
      { isEquivalence = isEquivalence
      ; congⁿ = congⁿ ∘ Core.subK→supK isSub
      }

  toSubstruct :
    ∀ {k′} {code′ : Code k′} (isSub : IsSubcode code′ code) →
    ∀ {Π′ : Properties code′} (hasΠ′ : Hasₚ (Core.supcodeProperties isSub Π′)) →
    Π′ ⇒ₚ Core.subcodeProperties isSub Π
  toSubstruct isSub hasΠ′ = Core.→ₚ-⇒ₚ λ π hasπ →
    Core.fromSupcode isSub
      (Core.⇒ₚ-→ₚ hasΠ′
        (Core.mapProperty (Core.subK→supK isSub) π)
        (Core.fromSupcode′ isSub hasπ))


text:
{-# OPTIONS --safe #-}
module Cubical.Data.FinData.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Nat using (ℕ; zero; suc; _+_; _·_; +-assoc)
open import Cubical.Data.Bool.Base
open import Cubical.Relation.Nullary

private
  variable
    ℓ : Level
    A B : Type ℓ

data Fin : ℕ → Type₀ where
  zero : {n : ℕ} → Fin (suc n)
  suc  : {n : ℕ} (i : Fin n) → Fin (suc n)

-- useful patterns
pattern one = suc zero
pattern two = suc one

toℕ : ∀ {n} → Fin n → ℕ
toℕ zero    = 0
toℕ (suc i) = suc (toℕ i)

fromℕ : (n : ℕ) → Fin (suc n)
fromℕ zero    = zero
fromℕ (suc n) = suc (fromℕ n)

toFromId : ∀ (n : ℕ) → toℕ (fromℕ n) ≡ n
toFromId zero = refl
toFromId (suc n) = cong suc (toFromId n)

¬Fin0 : ¬ Fin 0
¬Fin0 ()

_==_ : ∀ {n} → Fin n → Fin n → Bool
zero == zero   = true
zero == suc _  = false
suc _ == zero  = false
suc m == suc n = m == n

weakenFin : {n : ℕ} → Fin n → Fin (suc n)
weakenFin zero = zero
weakenFin (suc i) = suc (weakenFin i)

predFin : {n : ℕ} → Fin (suc (suc n)) → Fin (suc n)
predFin zero = zero
predFin (suc x) = x

foldrFin : ∀ {n} → (A → B → B) → B → (Fin n → A) → B
foldrFin {n = zero}  _ b _ = b
foldrFin {n = suc n} f b l = f (l zero) (foldrFin f b (l ∘ suc))

elim
  : ∀(P : ∀{k} → Fin k → Type ℓ)
  → (∀{k} → P {suc k} zero)
  → (∀{k} → {fn : Fin k} → P fn → P (suc fn))
  → {k : ℕ} → (fn : Fin k) → P fn

elim P fz fs {zero} = ⊥.rec ∘ ¬Fin0
elim P fz fs {suc k} zero = fz
elim P fz fs {suc k} (suc fj) = fs (elim P fz fs fj)

rec : ∀{k} → (a0 aS : A) → Fin k → A
rec a0 aS zero = a0
rec a0 aS (suc x) = aS

FinVec : (A : Type ℓ) (n : ℕ) → Type ℓ
FinVec A n = Fin n → A

replicateFinVec : (n : ℕ) → A → FinVec A n
replicateFinVec _ a _ = a

_++Fin_ : {n m : ℕ} → FinVec A n → FinVec A m → FinVec A (n + m)
_++Fin_ {n = zero} _ W i = W i
_++Fin_ {n = suc n} V _ zero = V zero
_++Fin_ {n = suc n} V W (suc i) = ((V ∘ suc) ++Fin W) i

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module Issue784.Values where

open import Data.Bool using (Bool; true; false; not)
open import Data.String public using (String)
open import Data.String.Properties public using (_≟_)

open import Function public
open import Data.List using (List; []; _∷_; _++_; [_]; filterᵇ) renaming (map to mapL)
open import Data.List.Relation.Unary.Any public using (Any; here; there) renaming (map to mapA; any to anyA)
open import Data.Product public using (Σ; Σ-syntax; proj₁; proj₂; _,_; _×_) renaming (map to mapΣ)
open import Data.Unit public using (⊤)
open import Data.Unit.NonEta public using (Unit; unit)
open import Data.Empty public using (⊥; ⊥-elim)
open import Relation.Binary.Core hiding (_⇔_) public
open import Relation.Nullary hiding (Irrelevant) public
import Level

open import Relation.Binary.PropositionalEquality public hiding ([_]) renaming (cong to ≡-cong; cong₂ to ≡-cong₂)
open import Relation.Binary.PropositionalEquality.Core public renaming (sym to ≡-sym; trans to ≡-trans)
{-
≢-sym : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≢ y → y ≢ x
≢-sym x≢y = x≢y ∘ ≡-sym
-}
≡-elim : ∀ {ℓ} {X Y : Set ℓ} → X ≡ Y → X → Y
≡-elim refl p = p

≡-elim′ : ∀ {a ℓ} {A : Set a} {x y : A} → (P : A → Set ℓ) → x ≡ y → P x → P y
≡-elim′ P = ≡-elim ∘ (≡-cong P)

Named : ∀ {ℓ} (A : Set ℓ) → Set ℓ
Named A = String × A

NamedType : ∀ ℓ → Set (Level.suc ℓ)
NamedType ℓ = Named (Set ℓ)

NamedValue : ∀ ℓ → Set (Level.suc ℓ)
NamedValue ℓ = Named (Σ[ A ∈ Set ℓ ] A)

Names : Set
Names = List String

Types : ∀ ℓ → Set (Level.suc ℓ)
Types ℓ = List (NamedType ℓ)

Values : ∀ ℓ → Set (Level.suc ℓ)
Values ℓ = List (NamedValue ℓ)

names : ∀ {ℓ} {A : Set ℓ} → List (Named A) → Names
names = mapL proj₁

types : ∀ {ℓ} → Values ℓ → Types ℓ
types = mapL (mapΣ id proj₁)

infix 4 _∈_ _∉_

_∈_ : ∀ {ℓ} {A : Set ℓ} → A → List A → Set ℓ
x ∈ xs = Any (_≡_ x) xs

_∉_ : ∀ {ℓ} {A : Set ℓ} → A → List A → Set ℓ
x ∉ xs = ¬ x ∈ xs

x∉y∷l⇒x≢y : ∀ {ℓ} {A : Set ℓ} {x y : A} {l : List A} → x ∉ y ∷ l → x ≢ y
x∉y∷l⇒x≢y x∉y∷l x≡y = x∉y∷l $ here x≡y

x∉y∷l⇒x∉l : ∀ {ℓ} {A : Set ℓ} {x y : A} {l : List A} → x ∉ y ∷ l → x ∉ l
x∉y∷l⇒x∉l x∉y∷l x∈l = x∉y∷l $ there x∈l

x≢y⇒x∉l⇒x∉y∷l : ∀ {ℓ} {A : Set ℓ} {x y : A} {l : List A} → x ≢ y → x ∉ l → x ∉ y ∷ l
x≢y⇒x∉l⇒x∉y∷l x≢y x∉l (here x≡y) = x≢y x≡y
x≢y⇒x∉l⇒x∉y∷l x≢y x∉l (there x∈l) = x∉l x∈l

infix 5 _∋!_ _∈?_

_∈?_ : (s : String) (n : Names) → Dec (s ∈ n)
s ∈? [] = no λ()
s ∈? (h ∷ t) with s ≟ h
... | yes s≡h = yes $ here s≡h
... | no s≢h with s ∈? t
...        | yes s∈t = yes $ there s∈t
...        | no s∉t = no $ x≢y⇒x∉l⇒x∉y∷l s≢h s∉t

_∋!_ : Names → String → Bool
l ∋! e with e ∈? l
... | yes _ = true
... | no _ = false

infix 4 _⊆_ _⊈_

_⊆_ : ∀ {ℓ} {A : Set ℓ} → List A → List A → Set ℓ
xs ⊆ ys = ∀ {x} → x ∈ xs → x ∈ ys

_⊈_ : ∀ {ℓ} {A : Set ℓ} → List A → List A → Set ℓ
xs ⊈ ys = ¬ xs ⊆ ys

infixl 5 _∪_

_∪_ : ∀ {ℓ} {A : Set ℓ} → List A → List A → List A
_∪_ = _++_

infixl 6 _∩_

_∩_ : Names → Names → Names
x ∩ y = filterᵇ (_∋!_ y) x

infixl 6 _∖_ _∖∖_

_∖_ : Names → Names → Names
_∖_ x y = filterᵇ (not ∘ _∋!_ y) x

_∖∖_ : ∀ {ℓ} {A : Set ℓ} → List (Named A) → Names → List (Named A)
_∖∖_ l n = filterᵇ (not ∘ _∋!_ n ∘ proj₁) l

filter-∈ : ∀ {ℓ} {A : Set ℓ} → List (Named A) → Names → List (Named A)
filter-∈ l n = filterᵇ (_∋!_ n ∘ proj₁) l

infixr 5 _∷_

data NonRepetitive {ℓ} {A : Set ℓ} : List A → Set ℓ where
  [] : NonRepetitive []
  _∷_ : ∀ {x xs} → x ∉ xs → NonRepetitive xs → NonRepetitive (x ∷ xs)

infix 4 _≋_

data _≋_ {ℓ} {A : Set ℓ} : List A → List A → Set ℓ where
  refl : ∀ {l} → l ≋ l
  perm : ∀ {l} l₁ x₁ x₂ l₂ → l ≋ l₁ ++ x₂ ∷ x₁ ∷ l₂ → l ≋ l₁ ++ x₁ ∷ x₂ ∷ l₂

NonRepetitiveNames : ∀ {ℓ} {A : Set ℓ} → List (Named A) → Set
NonRepetitiveNames = NonRepetitive ∘ names

NonRepetitiveTypes : ∀ ℓ → Set (Level.suc ℓ)
NonRepetitiveTypes ℓ = Σ[ t ∈ Types ℓ ] NonRepetitiveNames t

-- lemmas

∪-assoc : ∀ {l} {A : Set l} (x y z : List A) → (x ∪ y) ∪ z ≡ x ∪ (y ∪ z)
∪-assoc [] y z = refl
∪-assoc (x ∷ xs) y z = ≡-elim′ (λ e → x ∷ e ≡ (x ∷ xs) ∪ (y ∪ z)) (≡-sym $ ∪-assoc xs y z) refl

≡⇒≋ : ∀ {ℓ} {A : Set ℓ} {x y : List A} → x ≡ y → x ≋ y
≡⇒≋ refl = refl

private
    ∈-perm : ∀ {ℓ} {A : Set ℓ} {x : A} (l₁ : List A) (e₁ : A) (e₂ : A) (l₂ : List A) → x ∈ l₁ ++ e₁ ∷ e₂ ∷ l₂ → x ∈ l₁ ++ e₂ ∷ e₁ ∷ l₂
    ∈-perm [] e₁ e₂ l₂ (here .{e₁} .{e₂ ∷ l₂} px) = there $ here px
    ∈-perm [] e₁ e₂ l₂ (there .{e₁} .{e₂ ∷ l₂} (here .{e₂} .{l₂} px)) = here px
    ∈-perm [] e₁ e₂ l₂ (there .{e₁} .{e₂ ∷ l₂} (there .{e₂} .{l₂} pxs)) = there $ there pxs
    ∈-perm (h₁ ∷ t₁) e₁ e₂ l₂ (here .{h₁} .{t₁ ++ e₁ ∷ e₂ ∷ l₂} px) = here px
    ∈-perm (h₁ ∷ t₁) e₁ e₂ l₂ (there .{h₁} .{t₁ ++ e₁ ∷ e₂ ∷ l₂} pxs) = there $ ∈-perm t₁ e₁ e₂ l₂ pxs

≋⇒⊆ : ∀ {ℓ} {A : Set ℓ} {x y : List A} → x ≋ y → x ⊆ y
≋⇒⊆ refl p = p
≋⇒⊆ {x = x} {y = .(l₁ ++ x₁ ∷ x₂ ∷ l₂)} (perm l₁ x₁ x₂ l₂ p) {e} e∈x = ∈-perm l₁ x₂ x₁ l₂ $ ≋⇒⊆ p e∈x

≋-trans : ∀ {l} {A : Set l} {x y z : List A} → x ≋ y → y ≋ z → x ≋ z
≋-trans p refl = p
≋-trans p₁ (perm l₁ x₁ x₂ l₂ p₂) = perm l₁ x₁ x₂ l₂ $ ≋-trans p₁ p₂

≋-sym : ∀ {l} {A : Set l} {x y : List A} → x ≋ y → y ≋ x
≋-sym refl = refl
≋-sym (perm l₁ x₁ x₂ l₂ p) = ≋-trans (perm l₁ x₂ x₁ l₂ refl) (≋-sym p)

≋-del-ins-r : ∀ {l} {A : Set l} (l₁ : List A) (x : A) (l₂ l₃ : List A) → (l₁ ++ x ∷ l₂ ++ l₃) ≋ (l₁ ++ l₂ ++ x ∷ l₃)
≋-del-ins-r l₁ x [] l₃ = refl
≋-del-ins-r l₁ x (h ∷ t) l₃ = ≋-trans p₀ p₅
  where p₀ : (l₁ ++ x ∷ h ∷ t ++ l₃) ≋ (l₁ ++ h ∷ x ∷ t ++ l₃)
        p₀ = perm l₁ h x (t ++ l₃) refl

        p₁ : ((l₁ ++ [ h ]) ++ x ∷ t ++ l₃) ≋ ((l₁ ++ [ h ]) ++ t ++ x ∷ l₃)
        p₁ = ≋-del-ins-r (l₁ ++ [ h ]) x t l₃

        p₂ : (l₁ ++ [ h ]) ++ t ++ x ∷ l₃ ≡ l₁ ++ h ∷ t ++ x ∷ l₃
        p₂ = ∪-assoc l₁ [ h ] (t ++ x ∷ l₃)

        p₃ : (l₁ ++ [ h ]) ++ x ∷ t ++ l₃ ≡ l₁ ++ h ∷ x ∷ t ++ l₃
        p₃ = ∪-assoc l₁ [ h ] (x ∷ t ++ l₃)

        p₄ : ((l₁ ++ [ h ]) ++ x ∷ t ++ l₃) ≋ (l₁ ++ h ∷ t ++ x ∷ l₃)
        p₄ = ≡-elim′ (λ y → ((l₁ ++ [ h ]) ++ x ∷ t ++ l₃) ≋ y) p₂ p₁

        p₅ : (l₁ ++ h ∷ x ∷ t ++ l₃) ≋ (l₁ ++ h ∷ t ++ x ∷ l₃)
        p₅ = ≡-elim′ (λ y → y ≋ (l₁ ++ h ∷ t ++ x ∷ l₃)) p₃ p₄

≋-del-ins-l : ∀ {l} {A : Set l} (l₁ l₂ : List A) (x : A) (l₃ : List A) → (l₁ ++ l₂ ++ x ∷ l₃) ≋ (l₁ ++ x ∷ l₂ ++ l₃)
≋-del-ins-l l₁ l₂ x l₃ = ≋-sym $ ≋-del-ins-r l₁ x l₂ l₃

x∪[]≡x : ∀ {ℓ} {A : Set ℓ} (x : List A) → x ∪ [] ≡ x
x∪[]≡x [] = refl
x∪[]≡x (h ∷ t) = ≡-trans p₀ p₁
  where p₀ : (h ∷ t) ++ [] ≡ h ∷ t ++ []
        p₀ = ∪-assoc [ h ] t []
        p₁ : h ∷ t ++ [] ≡ h ∷ t
        p₁ = ≡-cong (λ x → h ∷ x) (x∪[]≡x t)

x∖[]≡x : (x : Names) → x ∖ [] ≡ x
x∖[]≡x [] = refl
x∖[]≡x (h ∷ t) = ≡-cong (_∷_ h) (x∖[]≡x t)

t∖[]≡t : ∀ {ℓ} {A : Set ℓ} (t : List (Named A)) → t ∖∖ [] ≡ t
t∖[]≡t [] = refl
t∖[]≡t (h ∷ t) = ≡-cong (_∷_ h) (t∖[]≡t t)

e∷x≋e∷y : ∀ {ℓ} {A : Set ℓ} (e : A) {x y : List A} → x ≋ y → e ∷ x ≋ e ∷ y
e∷x≋e∷y _ refl = refl
e∷x≋e∷y x (perm l₁ e₁ e₂ l₂ p) = perm (x ∷ l₁) e₁ e₂ l₂ (e∷x≋e∷y x p)

∪-sym : ∀ {ℓ} {A : Set ℓ} (x y : List A) → x ∪ y ≋ y ∪ x
∪-sym [] y = ≡-elim′ (λ z → y ≋ z) (≡-sym $ x∪[]≡x y) refl
∪-sym x [] = ≡-elim′ (λ z → z ≋ x) (≡-sym $ x∪[]≡x x) refl
∪-sym x (y ∷ ys) = ≡-elim′ (λ z → x ++ (y ∷ ys) ≋ z) p₃ (≋-trans p₁ p₂) where
    p₁ : x ++ (y ∷ ys) ≋ y ∷ (x ++ ys)
    p₁ = ≋-del-ins-l [] x y ys
    p₂ : y ∷ (x ++ ys) ≋ y ∷ (ys ++ x)
    p₂ = e∷x≋e∷y y $ ∪-sym x ys
    p₃ : y ∷ (ys ++ x) ≡ (y ∷ ys) ++ x
    p₃ = ∪-assoc [ y ] ys x

y≋ỳ⇒x∪y≋x∪ỳ : ∀ {ℓ} {A : Set ℓ} (x : List A) {y ỳ : List A} → y ≋ ỳ → x ∪ y ≋ x ∪ ỳ
y≋ỳ⇒x∪y≋x∪ỳ [] p = p
y≋ỳ⇒x∪y≋x∪ỳ (h ∷ t) p = e∷x≋e∷y h (y≋ỳ⇒x∪y≋x∪ỳ t p)

x≋x̀⇒x∪y≋x̀∪y : ∀ {ℓ} {A : Set ℓ} {x x̀ : List A} → x ≋ x̀ → (y : List A) → x ∪ y ≋ x̀ ∪ y
x≋x̀⇒x∪y≋x̀∪y {x = x} {x̀ = x̀} p y = ≋-trans (∪-sym x y) $ ≋-trans (y≋ỳ⇒x∪y≋x∪ỳ y p) (∪-sym y x̀)

x⊆y≋z : ∀ {ℓ} {A : Set ℓ} {x y z : List A} → x ⊆ y → y ≋ z → x ⊆ z
x⊆y≋z x⊆y refl = x⊆y
x⊆y≋z {x = x} {y = y} {z = .(l₁ ++ x₁ ∷ x₂ ∷ l₂)} x⊆y (perm l₁ x₁ x₂ l₂ p) = ∈-perm l₁ x₂ x₁ l₂ ∘ x⊆y≋z x⊆y p

x≋y⊆z : ∀ {ℓ} {A : Set ℓ} {x y z : List A} → x ≋ y → x ⊆ z → y ⊆ z
x≋y⊆z refl x⊆z = x⊆z
x≋y⊆z {y = .(l₁ ++ x₁ ∷ x₂ ∷ l₂)} {z = z} (perm l₁ x₁ x₂ l₂ p) x⊆z = x≋y⊆z p x⊆z ∘ ∈-perm l₁ x₁ x₂ l₂

x⊆x∪y : ∀ {ℓ} {A : Set ℓ} (x y : List A) → x ⊆ x ∪ y
x⊆x∪y .(x ∷ xs) y (here  {x} {xs} px) = here px
x⊆x∪y .(x ∷ xs) y (there {x} {xs} pxs) = there $ x⊆x∪y xs y pxs

x∪y⊆z⇒x⊆z : ∀ {ℓ} {A : Set ℓ} (x y : List A) {z : List A} → x ∪ y ⊆ z → x ⊆ z
x∪y⊆z⇒x⊆z x y x∪y⊆z = x∪y⊆z ∘ x⊆x∪y x y

x∪y⊆z⇒y⊆z : ∀ {ℓ} {A : Set ℓ} (x y : List A) {z : List A} → x ∪ y ⊆ z → y ⊆ z
x∪y⊆z⇒y⊆z x y = x∪y⊆z⇒x⊆z y x ∘ x≋y⊆z (∪-sym x y)

n-x∪y : ∀ {ℓ} {A : Set ℓ} (x y : List (Named A)) → names (x ∪ y) ≡ names x ∪ names y
n-x∪y [] _ = refl
n-x∪y {ℓ} (x ∷ xs) y = ≡-trans p₁ p₂ where
    nx = [ proj₁ x ]
    nxs = names xs
    ny = names y
    p₁ : nx ∪ names (xs ∪ y) ≡ nx ∪ (nxs ∪ ny)
    p₁ = ≡-cong (λ z → nx ∪ z) (n-x∪y xs y)
    p₂ : nx ∪ (nxs ∪ ny) ≡ (nx ∪ nxs) ∪ ny
    p₂ = ≡-sym $ ∪-assoc nx nxs ny

t-x∪y : ∀ {ℓ} (x y : Values ℓ) → types (x ∪ y) ≡ types x ∪ types y
t-x∪y [] _ = refl
t-x∪y (x ∷ xs) y = ≡-trans p₁ p₂ where
    nx = types [ x ]
    nxs = types xs
    ny = types y
    p₁ : nx ∪ types (xs ∪ y) ≡ nx ∪ (nxs ∪ ny)
    p₁ = ≡-cong (λ z → nx ∪ z) (t-x∪y xs y)
    p₂ : nx ∪ (nxs ∪ ny) ≡ (nx ∪ nxs) ∪ ny
    p₂ = ≡-sym $ ∪-assoc nx nxs ny

n-x≋y : ∀ {ℓ} {A : Set ℓ} {x y : List (Named A)} → x ≋ y → names x ≋ names y
n-x≋y refl = refl
n-x≋y (perm {x} l₁ e₁ e₂ l₂ p) = p₃ where
    n-l₁e₁e₂l₂ : ∀ e₁ e₂ → names (l₁ ++ e₁ ∷ e₂ ∷ l₂) ≡ names l₁ ++ names [ e₁ ] ++ names [ e₂ ] ++ names l₂
    n-l₁e₁e₂l₂ e₁ e₂ = ≡-trans p₁ $ ≡-trans p₂ p₃ where
        p₁ : names (l₁ ++ e₁ ∷ e₂ ∷ l₂) ≡ names l₁ ++ names (e₁ ∷ e₂ ∷ l₂)
        p₁ = n-x∪y l₁ (e₁ ∷ e₂ ∷ l₂)
        p₂ : names l₁ ++ names (e₁ ∷ e₂ ∷ l₂) ≡ names l₁ ++ names [ e₁ ] ++ names (e₂ ∷ l₂)
        p₂ = ≡-cong (λ z → names l₁ ++ z) (n-x∪y [ e₁ ] (e₂ ∷ l₂))
        p₃ : names l₁ ++ names [ e₁ ] ++ names (e₂ ∷ l₂) ≡ names l₁ ++ names [ e₁ ] ++ names [ e₂ ] ++ names l₂
        p₃ = ≡-cong (λ z → names l₁ ++ names [ e₁ ] ++ z) (n-x∪y [ e₂ ] l₂)

    p₁ : names x ≋ names l₁ ++ proj₁ e₂ ∷ proj₁ e₁ ∷ names l₂
    p₁ = ≡-elim′ (λ z → names x ≋ z) (n-l₁e₁e₂l₂ e₂ e₁) (n-x≋y p)
    p₂ : names x ≋ names l₁ ++ proj₁ e₁ ∷ proj₁ e₂ ∷ names l₂
    p₂ = perm (names l₁) (proj₁ e₁) (proj₁ e₂) (names l₂) p₁

    p₃ : names x ≋ names (l₁ ++ e₁ ∷ e₂ ∷ l₂)
    p₃ = ≡-elim′ (λ z → names x ≋ z) (≡-sym $ n-l₁e₁e₂l₂ e₁ e₂) p₂

n-types : ∀ {ℓ} (x : Values ℓ) → names (types x) ≡ names x
n-types [] = refl
n-types (x ∷ xs) = ≡-cong (λ z → proj₁ x ∷ z) (n-types xs)

nr-x≋y : ∀ {ℓ} {A : Set ℓ} {x y : List A} → x ≋ y → NonRepetitive x → NonRepetitive y
nr-x≋y refl u = u
nr-x≋y {y = .(l₁ ++ e₁ ∷ e₂ ∷ l₂)} (perm l₁ e₁ e₂ l₂ p) u = ≋-step l₁ e₂ e₁ l₂ (nr-x≋y p u) where
    ∉-step : ∀ {ℓ} {A : Set ℓ} {x : A} (l₁ : List A) (e₁ : A) (e₂ : A) (l₂ : List A) → x ∉ l₁ ++ e₁ ∷ e₂ ∷ l₂ → x ∉ l₁ ++ e₂ ∷ e₁ ∷ l₂
    ∉-step l₁ e₁ e₂ l₂ x∉l x∈l = ⊥-elim $ x∉l $ ∈-perm l₁ e₂ e₁ l₂ x∈l

    ≋-step : ∀ {ℓ} {A : Set ℓ} (l₁ : List A) (e₁ : A) (e₂ : A) (l₂ : List A) → NonRepetitive (l₁ ++ e₁ ∷ e₂ ∷ l₂) → NonRepetitive (l₁ ++ e₂ ∷ e₁ ∷ l₂)
    ≋-step [] e₁ e₂ l₂ (_∷_ .{e₁} .{e₂ ∷ l₂} e₁∉e₂∷l₂ (_∷_ .{e₂} .{l₂} e₂∉l₂ pU)) = e₂∉e₁∷l₂ ∷ e₁∉l₂ ∷ pU where
        e₁∉l₂ = e₁ ∉ l₂ ∋ x∉y∷l⇒x∉l e₁∉e₂∷l₂
        e₂∉e₁∷l₂ = e₂ ∉ e₁ ∷ l₂ ∋ x≢y⇒x∉l⇒x∉y∷l (≢-sym $ x∉y∷l⇒x≢y e₁∉e₂∷l₂) e₂∉l₂
    ≋-step (h₁ ∷ t₁) e₁ e₂ l₂ (_∷_ .{h₁} .{t₁ ++ e₁ ∷ e₂ ∷ l₂} p∉ pU) = ∉-step t₁ e₁ e₂ l₂ p∉ ∷ ≋-step t₁ e₁ e₂ l₂ pU

nr-x⇒nr-t-x : ∀ {ℓ} {x : Values ℓ} → NonRepetitiveNames x → NonRepetitiveNames (types x)
nr-x⇒nr-t-x {x = x} = ≡-elim′ NonRepetitive (≡-sym $ n-types x)

n-x∖y : ∀ {ℓ} {A : Set ℓ} (x : List (Named A)) (y : Names) → names (x ∖∖ y) ≡ names x ∖ y
n-x∖y [] _ = refl
n-x∖y (x ∷ xs) ny with not $ ny ∋! proj₁ x
... | false = n-x∖y xs ny
... | true = ≡-trans p₁ p₂ where
        p₁ : names (x ∷ (xs ∖∖ ny)) ≡ proj₁ x ∷ names (xs ∖∖ ny)
        p₁ = n-x∪y [ x ] (xs ∖∖ ny)
        p₂ : proj₁ x ∷ names (xs ∖∖ ny) ≡ proj₁ x ∷ (names xs ∖ ny)
        p₂ = ≡-cong (λ z → proj₁ x ∷ z) (n-x∖y xs ny)

t-x∖y : ∀ {ℓ} (x : Values ℓ) (y : Names) → types (x ∖∖ y) ≡ types x ∖∖ y
t-x∖y [] _ = refl
t-x∖y (x ∷ xs) ny with not $ ny ∋! proj₁ x
... | false = t-x∖y xs ny
... | true = ≡-trans p₁ p₂ where
        x̀ = types [ x ]
        p₁ : types (x ∷ (xs ∖∖ ny)) ≡ x̀ ∪ types (xs ∖∖ ny)
        p₁ = t-x∪y [ x ] (xs ∖∖ ny)
        p₂ : x̀ ∪ types (xs ∖∖ ny) ≡ x̀ ∪ (types xs ∖∖ ny)
        p₂ = ≡-cong (λ z → x̀ ∪ z) (t-x∖y xs ny)

n-filter-∈ : ∀ {ℓ} {A : Set ℓ} (x : List (Named A)) (y : Names) → names (filter-∈ x y) ≡ names x ∩ y
n-filter-∈ [] _ = refl
n-filter-∈ (x ∷ xs) ny with ny ∋! proj₁ x
... | false = n-filter-∈ xs ny
... | true = ≡-trans p₁ p₂ where
        p₁ : names (x ∷ (filter-∈ xs ny)) ≡ proj₁ x ∷ names (filter-∈ xs ny)
        p₁ = n-x∪y [ x ] (filter-∈ xs ny)
        p₂ : proj₁ x ∷ names (filter-∈ xs ny) ≡ proj₁ x ∷ (names xs ∩ ny)
        p₂ = ≡-cong (λ z → proj₁ x ∷ z) (n-filter-∈ xs ny)

t-filter-∈ : ∀ {ℓ} (x : Values ℓ) (y : Names) → types (filter-∈ x y) ≡ filter-∈ (types x) y
t-filter-∈ [] _ = refl
t-filter-∈ (x ∷ xs) ny with ny ∋! proj₁ x
... | false = t-filter-∈ xs ny
... | true = ≡-trans p₁ p₂ where
        x̀ = types [ x ]
        p₁ : types (x ∷ filter-∈ xs ny) ≡ x̀ ∪ types (filter-∈ xs ny)
        p₁ = t-x∪y [ x ] (filter-∈ xs ny)
        p₂ : x̀ ∪ types (filter-∈ xs ny) ≡ x̀ ∪ filter-∈ (types xs) ny
        p₂ = ≡-cong (λ z → x̀ ∪ z) (t-filter-∈ xs ny)

[]⊆x : ∀ {ℓ} {A : Set ℓ} (x : List A) → [] ⊆ x
[]⊆x _ ()

∀x∉[] : ∀ {ℓ} {A : Set ℓ} {x : A} → x ∉ []
∀x∉[] ()

x⊆[]⇒x≡[] : ∀ {ℓ} {A : Set ℓ} {x : List A} → x ⊆ [] → x ≡ []
x⊆[]⇒x≡[] {x = []} _ = refl
x⊆[]⇒x≡[] {x = _ ∷ _} x⊆[] = ⊥-elim $ ∀x∉[] $ x⊆[] (here refl)

x∩y⊆x : ∀ {ℓ} {A : Set ℓ} (x : List (Named A)) (y : Names) → filter-∈ x y ⊆ x
x∩y⊆x [] _ = λ()
x∩y⊆x (h ∷ t) y with y ∋! proj₁ h
... | false = there ∘ x∩y⊆x t y
... | true = f where
             f : h ∷ filter-∈ t y ⊆ h ∷ t
             f (here {x = .h} p) = here p
             f (there {xs = .(filter-∈ t y)} p) = there $ x∩y⊆x t y p

e∈x⇒e∈y∪x : ∀ {ℓ} {A : Set ℓ} {e : A} {x : List A} (y : List A) → e ∈ x → e ∈ y ∪ x
e∈x⇒e∈y∪x [] = id
e∈x⇒e∈y∪x (h ∷ t) = there ∘ e∈x⇒e∈y∪x t

e∈x⇒e∈x∪y : ∀ {ℓ} {A : Set ℓ} {e : A} {x : List A} (y : List A) → e ∈ x → e ∈ x ∪ y
e∈x⇒e∈x∪y {e = e} {x = x} y e∈x = x⊆y≋z f (∪-sym y x) (e ∈ [ e ] ∋ here refl) where
    f : [ e ] ⊆ y ∪ x
    f {è} (here {x = .e} p) = ≡-elim′ (λ z → z ∈ y ∪ x) (≡-sym p) (e∈x⇒e∈y∪x y e∈x)
    f (there ())

x∪y⊆x̀∪ỳ : ∀ {ℓ} {A : Set ℓ} {x x̀ y ỳ : List A} → x ⊆ x̀ → y ⊆ ỳ → x ∪ y ⊆ x̀ ∪ ỳ
x∪y⊆x̀∪ỳ {x = []} {x̀ = []} _ y⊆ỳ = y⊆ỳ
x∪y⊆x̀∪ỳ {x = []} {x̀ = _ ∷ t̀} _ y⊆ỳ = there ∘ x∪y⊆x̀∪ỳ ([]⊆x t̀) y⊆ỳ
x∪y⊆x̀∪ỳ {x = h ∷ t} {x̀ = x̀} {y = y} {ỳ = ỳ} x⊆x̀ y⊆ỳ = f where
    f : (h ∷ t) ∪ y ⊆ x̀ ∪ ỳ
    f {e} (here {x = .h} e≡h) = e∈x⇒e∈x∪y ỳ (x⊆x̀ $ here e≡h)
    f {e} (there {xs = .(t ∪ y)} p) = x∪y⊆x̀∪ỳ (x∪y⊆z⇒y⊆z [ h ] t x⊆x̀) y⊆ỳ p

x∖y⊆x : (x y : Names) → x ∖ y ⊆ x
x∖y⊆x [] _ = λ()
x∖y⊆x (h ∷ t) y with y ∋! h
... | true = there ∘ x∖y⊆x t y
... | false = x∪y⊆x̀∪ỳ (≋⇒⊆ $ ≡⇒≋ $ refl {x = [ h ]}) (x∖y⊆x t y)

t≋t∖n∪t∩n : ∀ {ℓ} {A : Set ℓ} (t : List (Named A)) (n : Names) → t ≋ (t ∖∖ n) ∪ filter-∈ t n
t≋t∖n∪t∩n [] _ = refl
t≋t∖n∪t∩n (h ∷ t) n with n ∋! proj₁ h
... | false = e∷x≋e∷y h $ t≋t∖n∪t∩n t n
... | true = ≋-trans p₁ p₂ where
           p₁ : h ∷ t ≋ (h ∷ (t ∖∖ n)) ∪ filter-∈ t n
           p₁ = e∷x≋e∷y h $ t≋t∖n∪t∩n t n
           p₂ : (h ∷ (t ∖∖ n)) ∪ filter-∈ t n ≋ (t ∖∖ n) ∪ (h ∷ filter-∈ t n)
           p₂ = ≋-del-ins-r [] h (t ∖∖ n) (filter-∈ t n)

e₁∈x⇒e₂∉x⇒e≢e₂ : ∀ {ℓ} {A : Set ℓ} {e₁ e₂ : A} {x : List A} → e₁ ∈ x → e₂ ∉ x → e₁ ≢ e₂
e₁∈x⇒e₂∉x⇒e≢e₂ e₁∈x e₂∉x refl = e₂∉x e₁∈x

e₁∈e₂∷x⇒e₁≢e₂⇒e₁∈x : ∀ {ℓ} {A : Set ℓ} {e₁ e₂ : A} {x : List A} → e₁ ∈ e₂ ∷ x → e₁ ≢ e₂ → e₁ ∈ x
e₁∈e₂∷x⇒e₁≢e₂⇒e₁∈x (here e₁≡e₂) e₁≢e₂ = ⊥-elim $ e₁≢e₂ e₁≡e₂
e₁∈e₂∷x⇒e₁≢e₂⇒e₁∈x (there e₁∈x) _ = e₁∈x

x⊆e∷y⇒e∉x⇒x⊆y : ∀ {ℓ} {A : Set ℓ} {e : A} {x y : List A} → x ⊆ e ∷ y → e ∉ x → x ⊆ y
x⊆e∷y⇒e∉x⇒x⊆y {e = e} {x = x} {y = y} x⊆e∷y e∉x {è} è∈x = e₁∈e₂∷x⇒e₁≢e₂⇒e₁∈x (x⊆e∷y è∈x) (e₁∈x⇒e₂∉x⇒e≢e₂ è∈x e∉x)

n-e∉l⇒e∉l : ∀ {ℓ} {A : Set ℓ} {e : Named A} {l : List (Named A)} → proj₁ e ∉ names l → e ∉ l
n-e∉l⇒e∉l {e = e} n-e∉l (here {x = è} p) = ⊥-elim $ n-e∉l $ here $ ≡-cong proj₁ p
n-e∉l⇒e∉l n-e∉l (there p) = n-e∉l⇒e∉l (x∉y∷l⇒x∉l n-e∉l) p

nr-names⇒nr : ∀ {ℓ} {A : Set ℓ} {l : List (Named A)} → NonRepetitiveNames l → NonRepetitive l
nr-names⇒nr {l = []} [] = []
nr-names⇒nr {l = _ ∷ _} (nh∉nt ∷ nr-t) = n-e∉l⇒e∉l nh∉nt ∷ nr-names⇒nr nr-t

e∉x⇒e∉y⇒e∉x∪y : ∀ {ℓ} {A : Set ℓ} {e : A} {x y : List A} → e ∉ x → e ∉ y → e ∉ x ∪ y
e∉x⇒e∉y⇒e∉x∪y {x = []} _  e∉y e∈y = ⊥-elim $ e∉y e∈y
e∉x⇒e∉y⇒e∉x∪y {x = h ∷ t} e∉x e∉y (here e≡h) = ⊥-elim $ e∉x $ here e≡h
e∉x⇒e∉y⇒e∉x∪y {x = h ∷ t} e∉x e∉y (there e∈t∪y) = e∉x⇒e∉y⇒e∉x∪y (x∉y∷l⇒x∉l e∉x) e∉y e∈t∪y

nr-x∖y∪y : {x y : Names} → NonRepetitive x → NonRepetitive y → NonRepetitive (x ∖ y ∪ y)
nr-x∖y∪y {x = []} _ nr-y = nr-y
nr-x∖y∪y {x = x ∷ xs} {y = y} (x∉xs ∷ nr-xs) nr-y with x ∈? y
... | yes x∈y = nr-x∖y∪y nr-xs nr-y
... | no x∉y = e∉x⇒e∉y⇒e∉x∪y (⊥-elim ∘ x∉xs ∘ x∖y⊆x xs y) x∉y ∷ nr-x∖y∪y nr-xs nr-y

e∉l∖[e] : (e : String) (l : Names) → e ∉ l ∖ [ e ]
e∉l∖[e] _ [] = λ()
e∉l∖[e] e (h ∷ t) with h ≟ e
... | yes _ = e∉l∖[e] e t
... | no h≢e = x≢y⇒x∉l⇒x∉y∷l (≢-sym h≢e) (e∉l∖[e] e t)

e∉l⇒l∖e≡l : {e : String} {l : Names} → e ∉ l → l ∖ [ e ] ≡ l
e∉l⇒l∖e≡l {e = e} {l = []} _ = refl
e∉l⇒l∖e≡l {e = e} {l = h ∷ t} e∉l with h ∈? [ e ]
... | yes h∈e = ⊥-elim $ x≢y⇒x∉l⇒x∉y∷l (≢-sym $ x∉y∷l⇒x≢y e∉l) (λ()) h∈e
... | no h∉e = ≡-cong (_∷_ h) (e∉l⇒l∖e≡l $ x∉y∷l⇒x∉l e∉l)

e∈l⇒nr-l⇒l∖e∪e≋l : {e : String} {l : Names} → e ∈ l → NonRepetitive l → l ∖ [ e ] ∪ [ e ] ≋ l
e∈l⇒nr-l⇒l∖e∪e≋l {l = []} () _
e∈l⇒nr-l⇒l∖e∪e≋l {e = e} {l = h ∷ t} e∈h∷t (h∉t ∷ nr-t) with h ∈? [ e ]
... | yes (here h≡e) = ≋-trans (≡⇒≋ $ ≡-trans p₁ p₂) (∪-sym t [ h ]) where
          p₁ : t ∖ [ e ] ∪ [ e ] ≡ t ∖ [ h ] ∪ [ h ]
          p₁ = ≡-cong (λ x → t ∖ [ x ] ∪ [ x ]) (≡-sym h≡e)
          p₂ : t ∖ [ h ] ∪ [ h ] ≡ t ∪ [ h ]
          p₂ = ≡-cong (λ x → x ∪ [ h ]) (e∉l⇒l∖e≡l h∉t)
... | yes (there ())
... | no  h∉e with e∈h∷t
...      | here e≡h = ⊥-elim ∘ h∉e ∘ here ∘ ≡-sym $ e≡h
...      | there e∈t = e∷x≋e∷y _ $ e∈l⇒nr-l⇒l∖e∪e≋l e∈t nr-t

nr-x∖y : {x : Names} → NonRepetitive x → (y : Names) → NonRepetitive (x ∖ y)
nr-x∖y {x = []} _ _ = []
nr-x∖y {x = x ∷ xs} (x∉xs ∷ nr-xs) y with x ∈? y
... | yes x∈y = nr-x∖y nr-xs y
... | no  x∉y = ⊥-elim ∘ x∉xs ∘ x∖y⊆x xs y ∷ nr-x∖y nr-xs y

x⊆y⇒e∉y⇒e∉x : ∀ {ℓ} {A : Set ℓ} {e : A} {x y : List A} → x ⊆ y → e ∉ y → e ∉ x
x⊆y⇒e∉y⇒e∉x x⊆y e∉y e∈x = e∉y $ x⊆y e∈x

e∈n-l⇒∃è,n-è≡e×è∈l : ∀ {ℓ} {A : Set ℓ} {e : String} {l : List (Named A)} → e ∈ names l → Σ[ è ∈ Named A ] (e ≡ proj₁ è × è ∈ l)
e∈n-l⇒∃è,n-è≡e×è∈l {l = []} ()
e∈n-l⇒∃è,n-è≡e×è∈l {l = h ∷ t} (here e≡n-h) = h , e≡n-h , here refl
e∈n-l⇒∃è,n-è≡e×è∈l {l = h ∷ t} (there e∈n-t) with e∈n-l⇒∃è,n-è≡e×è∈l e∈n-t
... | è , n-è≡e , è∈l = è , n-è≡e , there è∈l

x⊆y⇒nx⊆ny : ∀ {ℓ} {A : Set ℓ} {x y : List (Named A)} → x ⊆ y → names x ⊆ names y
x⊆y⇒nx⊆ny {x = x} {y = y} x⊆y {e} e∈n-x with e ∈? names y
... | yes e∈n-y = e∈n-y
... | no  e∉n-y with e∈n-l⇒∃è,n-è≡e×è∈l e∈n-x
...              | è , e≡n-è , è∈x = ⊥-elim $ x⊆y⇒e∉y⇒e∉x x⊆y (n-e∉l⇒e∉l $ ≡-elim′ (λ z → z ∉ names y) e≡n-è e∉n-y) è∈x

nr-x⇒nr-x∩y : ∀ {ℓ} {A : Set ℓ} {x : List (Named A)} → NonRepetitiveNames x → (y : Names) → NonRepetitiveNames (filter-∈ x y)
nr-x⇒nr-x∩y {x = []} _ _ = []
nr-x⇒nr-x∩y {x = h ∷ t} (h∉t ∷ nr-t) y with y ∋! proj₁ h
... | false = nr-x⇒nr-x∩y nr-t y
... | true = x⊆y⇒e∉y⇒e∉x (x⊆y⇒nx⊆ny $ x∩y⊆x t y) h∉t ∷ nr-x⇒nr-x∩y nr-t y

e∈l⇒[e]⊆l : ∀ {ℓ} {A : Set ℓ} {e : A} {l : List A} → e ∈ l → [ e ] ⊆ l
e∈l⇒[e]⊆l e∈l (here è≡e) = ≡-elim′ (λ x → x ∈ _) (≡-sym è≡e) e∈l
e∈l⇒[e]⊆l e∈l (there ())

a∈x⇒x≋y⇒a∈y : ∀ {ℓ} {A : Set ℓ} {x y : List A} {a : A} → a ∈ x → x ≋ y → a ∈ y
a∈x⇒x≋y⇒a∈y a∈x x≋y = x⊆y≋z (e∈l⇒[e]⊆l a∈x) x≋y (here refl)

x⊆z⇒y⊆z⇒x∪y⊆z : ∀ {ℓ} {A : Set ℓ} {x y z : List A} → x ⊆ z → y ⊆ z → x ∪ y ⊆ z
x⊆z⇒y⊆z⇒x∪y⊆z {x = []} _ y⊆z = y⊆z
x⊆z⇒y⊆z⇒x∪y⊆z {x = h ∷ t} {y = y} {z = z} x⊆z y⊆z = f where
    f : (h ∷ t) ∪ y ⊆ z
    f {e} (here e≡h) = x⊆z $ here e≡h
    f {e} (there e∈t∪y) = x⊆z⇒y⊆z⇒x∪y⊆z (x∪y⊆z⇒y⊆z [ h ] t x⊆z) y⊆z e∈t∪y

x⊆x∖y∪y : (x y : Names) → x ⊆ x ∖ y ∪ y
x⊆x∖y∪y [] _ = []⊆x _
x⊆x∖y∪y (h ∷ t) y with h ∈? y
x⊆x∖y∪y (h ∷ t) y | yes h∈y = x⊆z⇒y⊆z⇒x∪y⊆z (e∈l⇒[e]⊆l $ e∈x⇒e∈y∪x (t ∖ y) h∈y) (x⊆x∖y∪y t y)
x⊆x∖y∪y (h ∷ t) y | no _ = x∪y⊆x̀∪ỳ ([ h ] ⊆ [ h ] ∋ ≋⇒⊆ refl) (x⊆x∖y∪y t y)

e₁∈l⇒e₁∉l∖e₂⇒e₁≡e₂ : {e₁ e₂ : String} {l : Names} → e₁ ∈ l → e₁ ∉ l ∖ [ e₂ ] → e₁ ≡ e₂
e₁∈l⇒e₁∉l∖e₂⇒e₁≡e₂ {e₁ = e₁} {e₂ = e₂} {l = l} e₁∈l e₁∉l∖e₂ with e₁ ≟ e₂
... | yes e₁≡e₂ = e₁≡e₂
... | no e₁≢e₂ = ⊥-elim $ p₄ e₁∈l where
         p₁ : e₁ ∉ [ e₂ ] ∪ (l ∖ [ e₂ ])
         p₁ = x≢y⇒x∉l⇒x∉y∷l e₁≢e₂ e₁∉l∖e₂
         p₂ : [ e₂ ] ∪ (l ∖ [ e₂ ]) ≋ (l ∖ [ e₂ ]) ∪ [ e₂ ]
         p₂ = ∪-sym [ e₂ ] (l ∖ [ e₂ ])
         p₃ : e₁ ∉ (l ∖ [ e₂ ]) ∪ [ e₂ ]
         p₃ = p₁ ∘ ≋⇒⊆ (∪-sym (l ∖ [ e₂ ]) [ e₂ ])
         p₄ : e₁ ∉ l
         p₄ = x⊆y⇒e∉y⇒e∉x (x⊆x∖y∪y l [ e₂ ]) p₃

e∉x⇒x∩y≋x∩y∖e : {e : String} {x : Names} (y : Names) → e ∉ x → x ∩ y ≡ x ∩ (y ∖ [ e ])
e∉x⇒x∩y≋x∩y∖e {x = []} _ _ = refl
e∉x⇒x∩y≋x∩y∖e {e = e} {x = h ∷ t} y e∉x with h ∈? y | h ∈? (y ∖ [ e ])
... | yes h∈y | yes h∈y∖e = ≡-cong (_∷_ h) $ e∉x⇒x∩y≋x∩y∖e y $ x∉y∷l⇒x∉l e∉x
... | yes h∈y | no  h∉y∖e = ⊥-elim $ e∉x e∈x where
        e∈x : e ∈ h ∷ t
        e∈x = here $ ≡-sym $ e₁∈l⇒e₁∉l∖e₂⇒e₁≡e₂ h∈y h∉y∖e
... | no  h∉y | yes h∈y∖e = ⊥-elim $ h∉y $ x∖y⊆x y [ e ] h∈y∖e
... | no  h∉y | no  h∉y∖e = e∉x⇒x∩y≋x∩y∖e y $ x∉y∷l⇒x∉l e∉x

y⊆x⇒x∩y≋y : {x y : Names} → NonRepetitive y → NonRepetitive x → y ⊆ x → x ∩ y ≋ y
y⊆x⇒x∩y≋y {x = []} _ _ y⊆[] = ≡⇒≋ $ ≡-elim′ (λ y → [] ∩ y ≡ y) (≡-sym $ x⊆[]⇒x≡[] y⊆[]) refl
y⊆x⇒x∩y≋y {x = h ∷ t} {y = y} nr-y (h∉t ∷ nr-t) y⊆h∷t with h ∈? y
... | yes h∈y = ≋-trans (∪-sym [ h ] (t ∩ y)) p₄ where
        p₁ : t ∩ y ≋ t ∩ (y ∖ [ h ])
        p₁ = ≡⇒≋ $ e∉x⇒x∩y≋x∩y∖e y h∉t
        p₂ : t ∩ (y ∖ [ h ]) ≋ y ∖ [ h ]
        p₂ = y⊆x⇒x∩y≋y (nr-x∖y nr-y [ h ]) nr-t $ x⊆e∷y⇒e∉x⇒x⊆y (y⊆h∷t ∘ x∖y⊆x y [ h ]) (e∉l∖[e] h y)
        p₃ : y ∖ [ h ] ∪ [ h ] ≋ y
        p₃ = e∈l⇒nr-l⇒l∖e∪e≋l h∈y nr-y
        p₄ : t ∩ y ∪ [ h ] ≋ y
        p₄ = ≋-trans (x≋x̀⇒x∪y≋x̀∪y (≋-trans p₁ p₂) [ h ]) p₃
... | no  h∉y = y⊆x⇒x∩y≋y nr-y nr-t $ x⊆e∷y⇒e∉x⇒x⊆y y⊆h∷t h∉y

x∪y∖n≡x∖n∪y∖n : ∀ {ℓ} {A : Set ℓ} (x y : List (Named A)) (n : Names) → (x ∪ y) ∖∖ n ≡ (x ∖∖ n) ∪ (y ∖∖ n)
x∪y∖n≡x∖n∪y∖n [] _ _ = refl
x∪y∖n≡x∖n∪y∖n (h ∷ t) y n with proj₁ h ∈? n
... | yes _ = x∪y∖n≡x∖n∪y∖n t y n
... | no  _ = ≡-cong (_∷_ h) (x∪y∖n≡x∖n∪y∖n t y n)

n-x⊆n⇒x∖n≡[] : ∀ {ℓ} {A : Set ℓ} (x : List (Named A)) (n : Names) → names x ⊆ n → x ∖∖ n ≡ []
n-x⊆n⇒x∖n≡[] [] _ _ = refl
n-x⊆n⇒x∖n≡[] (h ∷ t) n n-x⊆n with proj₁ h ∈? n
... | yes _ = n-x⊆n⇒x∖n≡[] t n $ x∪y⊆z⇒y⊆z [ proj₁ h ] (names t) (x≋y⊆z (≡⇒≋ $ n-x∪y [ h ] t) n-x⊆n)
... | no h∉n = ⊥-elim $ h∉n $ n-x⊆n (proj₁ h ∈ proj₁ h ∷ names t ∋ here refl)

x∖x≡[] : ∀ {ℓ} {A : Set ℓ} (x : List (Named A)) → x ∖∖ names x ≡ []
x∖x≡[] x = n-x⊆n⇒x∖n≡[] x (names x) (≋⇒⊆ refl)

nr-[a] : ∀ {ℓ} {A : Set ℓ} {a : A} → NonRepetitive [ a ]
nr-[a] = (λ()) ∷ []

x≋y⇒x∖n≋y∖n : ∀ {ℓ} {A : Set ℓ} {x y : List (Named A)} → x ≋ y → (n : Names) → x ∖∖ n ≋ y ∖∖ n
x≋y⇒x∖n≋y∖n refl _ = refl
x≋y⇒x∖n≋y∖n {x = x} (perm l₁ x₁ x₂ l₂ p) n = ≋-trans p₀ $ ≋-trans (≡⇒≋ p₅) $ ≋-trans pg (≡⇒≋ $ ≡-sym g₅) where
    p₀ : x ∖∖ n ≋ (l₁ ++ x₂ ∷ x₁ ∷ l₂) ∖∖ n
    p₀ = x≋y⇒x∖n≋y∖n p n

    p₁ : (l₁ ++ [ x₂ ] ++ [ x₁ ] ++ l₂) ∖∖ n ≡ l₁ ∖∖ n ++ ([ x₂ ] ++ [ x₁ ] ++ l₂) ∖∖ n
    p₁ = x∪y∖n≡x∖n∪y∖n l₁ ([ x₂ ] ++ [ x₁ ] ++ l₂) n

    p₂ : l₁ ∖∖ n ++ ([ x₂ ] ++ [ x₁ ] ++ l₂) ∖∖ n ≡ l₁ ∖∖ n ++ [ x₂ ] ∖∖ n ++ ([ x₁ ] ++ l₂) ∖∖ n
    p₂ = ≡-cong (λ z → l₁ ∖∖ n ++ z) (x∪y∖n≡x∖n∪y∖n [ x₂ ] ([ x₁ ] ++ l₂) n)

    p₃ : l₁ ∖∖ n ++ [ x₂ ] ∖∖ n ++ ([ x₁ ] ++ l₂) ∖∖ n ≡ l₁ ∖∖ n ++ [ x₂ ] ∖∖ n ++ [ x₁ ] ∖∖ n ++ l₂ ∖∖ n
    p₃ = ≡-cong (λ z → l₁ ∖∖ n ++ [ x₂ ] ∖∖ n ++ z) (x∪y∖n≡x∖n∪y∖n [ x₁ ] l₂ n)

    p₄ : l₁ ∖∖ n ++ [ x₂ ] ∖∖ n ++ [ x₁ ] ∖∖ n ++ l₂ ∖∖ n ≡ l₁ ∖∖ n ++ ([ x₂ ] ∖∖ n ++ [ x₁ ] ∖∖ n) ++ l₂ ∖∖ n
    p₄ = ≡-cong (λ z → l₁ ∖∖ n ++ z) (≡-sym $ ∪-assoc ([ x₂ ] ∖∖ n) ([ x₁ ] ∖∖ n) (l₂ ∖∖ n))

    p₅ : (l₁ ++ [ x₂ ] ++ [ x₁ ] ++ l₂) ∖∖ n ≡ l₁ ∖∖ n ++ ([ x₂ ] ∖∖ n ++ [ x₁ ] ∖∖ n) ++ l₂ ∖∖ n
    p₅ = ≡-trans p₁ $ ≡-trans p₂ $ ≡-trans p₃ p₄

    pg : l₁ ∖∖ n ++ ([ x₂ ] ∖∖ n ++ [ x₁ ] ∖∖ n) ++ l₂ ∖∖ n ≋ l₁ ∖∖ n ++ ([ x₁ ] ∖∖ n ++ [ x₂ ] ∖∖ n) ++ l₂ ∖∖ n
    pg = y≋ỳ⇒x∪y≋x∪ỳ (l₁ ∖∖ n) $ x≋x̀⇒x∪y≋x̀∪y (∪-sym ([ x₂ ] ∖∖ n) ([ x₁ ] ∖∖ n)) (l₂ ∖∖ n)

    g₁ : (l₁ ++ [ x₁ ] ++ [ x₂ ] ++ l₂) ∖∖ n ≡ l₁ ∖∖ n ++ ([ x₁ ] ++ [ x₂ ] ++ l₂) ∖∖ n
    g₁ = x∪y∖n≡x∖n∪y∖n l₁ ([ x₁ ] ++ [ x₂ ] ++ l₂) n

    g₂ : l₁ ∖∖ n ++ ([ x₁ ] ++ [ x₂ ] ++ l₂) ∖∖ n ≡ l₁ ∖∖ n ++ [ x₁ ] ∖∖ n ++ ([ x₂ ] ++ l₂) ∖∖ n
    g₂ = ≡-cong (λ z → l₁ ∖∖ n ++ z) (x∪y∖n≡x∖n∪y∖n [ x₁ ] ([ x₂ ] ++ l₂) n)

    g₃ : l₁ ∖∖ n ++ [ x₁ ] ∖∖ n ++ ([ x₂ ] ++ l₂) ∖∖ n ≡ l₁ ∖∖ n ++ [ x₁ ] ∖∖ n ++ [ x₂ ] ∖∖ n ++ l₂ ∖∖ n
    g₃ = ≡-cong (λ z → l₁ ∖∖ n ++ [ x₁ ] ∖∖ n ++ z) (x∪y∖n≡x∖n∪y∖n [ x₂ ] l₂ n)

    g₄ : l₁ ∖∖ n ++ [ x₁ ] ∖∖ n ++ [ x₂ ] ∖∖ n ++ l₂ ∖∖ n ≡ l₁ ∖∖ n ++ ([ x₁ ] ∖∖ n ++ [ x₂ ] ∖∖ n) ++ l₂ ∖∖ n
    g₄ = ≡-cong (λ z → l₁ ∖∖ n ++ z) (≡-sym $ ∪-assoc ([ x₁ ] ∖∖ n) ([ x₂ ] ∖∖ n) (l₂ ∖∖ n))

    g₅ : (l₁ ++ [ x₁ ] ++ [ x₂ ] ++ l₂) ∖∖ n ≡ l₁ ∖∖ n ++ ([ x₁ ] ∖∖ n ++ [ x₂ ] ∖∖ n) ++ l₂ ∖∖ n
    g₅ = ≡-trans g₁ $ ≡-trans g₂ $ ≡-trans g₃ g₄

nr-x∪y⇒e∈x⇒e∈y⇒⊥ : ∀ {ℓ} {A : Set ℓ} {e : A} {x y : List A} → NonRepetitive (x ∪ y) → e ∈ x → e ∈ y → ⊥
nr-x∪y⇒e∈x⇒e∈y⇒⊥ {x = []} _ ()
nr-x∪y⇒e∈x⇒e∈y⇒⊥ {x = h ∷ t} (h∉t∪y ∷ nr-t∪y) (here e≡h) = h∉t∪y ∘ e∈x⇒e∈y∪x t ∘ ≡-elim′ (λ x → x ∈ _) e≡h
nr-x∪y⇒e∈x⇒e∈y⇒⊥ {x = h ∷ t} (h∉t∪y ∷ nr-t∪y) (there e∈t) = nr-x∪y⇒e∈x⇒e∈y⇒⊥ nr-t∪y e∈t

nr-x∪y⇒x∖y≡x : ∀ {ℓ} {A : Set ℓ} (x y : List (Named A)) → NonRepetitiveNames (x ∪ y) → y ∖∖ names x ≡ y
nr-x∪y⇒x∖y≡x x y nr-x∪y = f₀ y (≋⇒⊆ refl) where
    f₀ : ∀ t → t ⊆ y → t ∖∖ names x ≡ t
    f₀ [] _ = refl
    f₀ (h ∷ t) h∷t⊆y with proj₁ h ∈? names x
    ... | yes h∈x = ⊥-elim $ nr-x∪y⇒e∈x⇒e∈y⇒⊥ (≡-elim′ NonRepetitive (n-x∪y x y) nr-x∪y) h∈x (x⊆y⇒nx⊆ny h∷t⊆y $ here refl)
    ... | no _ = ≡-cong (_∷_ h) (f₀ t $ x∪y⊆z⇒y⊆z [ h ] t h∷t⊆y)

t≋t₁∪t₂⇒t∖t₁≋t₂ : ∀ {ℓ} {A : Set ℓ} {t : List (Named A)} → NonRepetitiveNames t → (t₁ t₂ : List (Named A)) → t ≋ t₁ ∪ t₂ → t ∖∖ names t₁ ≋ t₂
t≋t₁∪t₂⇒t∖t₁≋t₂ {t = t} nr-t t₁ t₂ t≋t₁∪t₂ = ≋-trans p₂ (≡⇒≋ $ nr-x∪y⇒x∖y≡x t₁ t₂ $ nr-x≋y (n-x≋y t≋t₁∪t₂) nr-t) where
    n-t₁ = names t₁
    p₁ : t ∖∖ n-t₁ ≋ (t₁ ∖∖ n-t₁) ∪ (t₂ ∖∖ n-t₁)
    p₁ = ≋-trans (x≋y⇒x∖n≋y∖n t≋t₁∪t₂ n-t₁) (≡⇒≋ $ x∪y∖n≡x∖n∪y∖n t₁ t₂ n-t₁)
    p₂ : t ∖∖ n-t₁ ≋ t₂ ∖∖ n-t₁
    p₂ = ≡-elim′ (λ x → t ∖∖ n-t₁ ≋ x ∪ (t₂ ∖∖ n-t₁)) (x∖x≡[] t₁) p₁

x≋x̀⇒y≋ỳ⇒x∪y≋x̀∪ỳ : ∀ {ℓ} {A : Set ℓ} {x x̀ y ỳ : List A} → x ≋ x̀ → y ≋ ỳ → x ∪ y ≋ x̀ ∪ ỳ
x≋x̀⇒y≋ỳ⇒x∪y≋x̀∪ỳ x≋x̀ (refl {y}) = x≋x̀⇒x∪y≋x̀∪y x≋x̀ y
x≋x̀⇒y≋ỳ⇒x∪y≋x̀∪ỳ {x = x} {x̀ = x̀} {y = y} {ỳ = ._} x≋x̀ (perm l₁ x₁ x₂ l₂ y≋l₁x₂x₁l₂) = ≋-trans p₁ $ ≋-trans p₂ $ ≋-trans p₃ p₄ where
    p₁ : x ∪ y ≋ x̀ ∪ (l₁ ++ x₂ ∷ x₁ ∷ l₂)
    p₁ = x≋x̀⇒y≋ỳ⇒x∪y≋x̀∪ỳ x≋x̀ y≋l₁x₂x₁l₂
    p₂ : x̀ ∪ (l₁ ++ x₂ ∷ x₁ ∷ l₂) ≋ (x̀ ∪ l₁) ++ x₂ ∷ x₁ ∷ l₂
    p₂ = ≡⇒≋ $ ≡-sym $ ∪-assoc x̀ l₁ (x₂ ∷ x₁ ∷ l₂)
    p₃ : (x̀ ∪ l₁) ++ x₂ ∷ x₁ ∷ l₂ ≋ (x̀ ∪ l₁) ++ x₁ ∷ x₂ ∷ l₂
    p₃ = perm (x̀ ∪ l₁) x₁ x₂ l₂ refl
    p₄ : (x̀ ∪ l₁) ++ x₁ ∷ x₂ ∷ l₂ ≋ x̀ ∪ (l₁ ++ x₁ ∷ x₂ ∷ l₂)
    p₄ = ≡⇒≋ $ ∪-assoc x̀ l₁ (x₁ ∷ x₂ ∷ l₂)

x∖y∪y≋y∖x∪x : ∀ {ℓ} {A : Set ℓ} (x y : List (Named A)) →
               let nx = names x
                   ny = names y
               in filter-∈ x ny ≋ filter-∈ y nx → x ∖∖ ny ∪ y ≋ y ∖∖ nx ∪ x
x∖y∪y≋y∖x∪x x y p₀ = ≋-trans p₁ $ ≋-trans p₂ p₃ where
    nx = names x
    ny = names y
    p₁ : x ∖∖ ny ∪ y ≋ x ∖∖ ny ∪ y ∖∖ nx ∪ filter-∈ y nx
    p₁ = ≋-trans (y≋ỳ⇒x∪y≋x∪ỳ (x ∖∖ ny) (t≋t∖n∪t∩n y nx)) (≡⇒≋ $ ≡-sym $ ∪-assoc (x ∖∖ ny) (y ∖∖ nx) (filter-∈ y nx))
    p₂ : (x ∖∖ ny ∪ y ∖∖ nx) ∪ filter-∈ y nx ≋ (y ∖∖ nx ∪ x ∖∖ ny) ∪ filter-∈ x ny
    p₂ = x≋x̀⇒y≋ỳ⇒x∪y≋x̀∪ỳ (∪-sym (x ∖∖ ny) (y ∖∖ nx)) (≋-sym p₀)
    p₃ : y ∖∖ nx ∪ x ∖∖ ny ∪ filter-∈ x ny ≋ y ∖∖ nx ∪ x
    p₃ = ≋-trans (≡⇒≋ $ ∪-assoc (y ∖∖ nx) (x ∖∖ ny) (filter-∈ x ny)) (≋-sym $ y≋ỳ⇒x∪y≋x∪ỳ (y ∖∖ nx) (t≋t∖n∪t∩n x ny))

names⇒named : Names → List (Named Unit)
names⇒named = mapL (λ x → x , unit)

nn-x∪y≡nn-x∪nn-y : ∀ x y → names⇒named (x ∪ y) ≡ names⇒named x ∪ names⇒named y
nn-x∪y≡nn-x∪nn-y [] y = refl
nn-x∪y≡nn-x∪nn-y (h ∷ t) y = ≡-cong (_∷_ _) (nn-x∪y≡nn-x∪nn-y t y)

nn-x≡x : ∀ x → names (names⇒named x) ≡ x
nn-x≡x [] = refl
nn-x≡x (h ∷ t) = ≡-cong (_∷_ h) (nn-x≡x t)

x≋y⇒nn-x≋nn-y : ∀ {x y} → x ≋ y → names⇒named x ≋ names⇒named y
x≋y⇒nn-x≋nn-y refl = refl
x≋y⇒nn-x≋nn-y {x = x} {y = ._} (perm l₁ x₁ x₂ l₂ x≋l₁x₂x₁l₂) = ≋-trans p₁ p₂ where
    p₁ : names⇒named x ≋ names⇒named l₁ ++ (x₂ , unit) ∷ (x₁ , unit) ∷ names⇒named l₂
    p₁ = ≋-trans (x≋y⇒nn-x≋nn-y x≋l₁x₂x₁l₂) (≡⇒≋ $ nn-x∪y≡nn-x∪nn-y l₁ (x₂ ∷ x₁ ∷ l₂))
    p₂ : names⇒named l₁ ++ (x₂ , unit) ∷ (x₁ , unit) ∷ names⇒named l₂ ≋ names⇒named (l₁ ++ x₁ ∷ x₂ ∷ l₂)
    p₂ = ≋-trans (perm (names⇒named l₁) (x₁ , unit) (x₂ , unit) (names⇒named l₂) refl) (≡⇒≋ $ ≡-sym $ nn-x∪y≡nn-x∪nn-y l₁ (x₁ ∷ x₂ ∷ l₂))

x≋y∪z⇒x∖y≋z : {x : Names} → NonRepetitive x → (y z : Names) → x ≋ y ∪ z → x ∖ y ≋ z
x≋y∪z⇒x∖y≋z {x} nr-x y z x≋y∪z = ≋-trans (≡⇒≋ $ ≡-sym $ ≡-trans p₂ p₃) (≋-trans p₁ $ ≡⇒≋ $ nn-x≡x z) where
    ux = names⇒named x
    uy = names⇒named y
    uz = names⇒named z
    ux≋uy∪uz : ux ≋ uy ∪ uz
    ux≋uy∪uz = ≋-trans (x≋y⇒nn-x≋nn-y x≋y∪z) (≡⇒≋ $ nn-x∪y≡nn-x∪nn-y y z)
    p₁ : names (ux ∖∖ names uy) ≋ names uz
    p₁ = n-x≋y $ t≋t₁∪t₂⇒t∖t₁≋t₂ (≡-elim′ NonRepetitive (≡-sym $ nn-x≡x x) nr-x) uy uz ux≋uy∪uz
    p₂ : names (ux ∖∖ names uy) ≡ names ux ∖ names uy
    p₂ = n-x∖y ux (names uy)
    p₃ : names ux ∖ names uy ≡ x ∖ y
    p₃ = ≡-cong₂ _∖_ (nn-x≡x x) (nn-x≡x y)

h∈x⇒∃t,x≋h∷t : ∀ {ℓ} {A : Set ℓ} {h : A} {x : List A} → h ∈ x → NonRepetitive x → Σ[ t ∈ List A ] x ≋ h ∷ t
h∈x⇒∃t,x≋h∷t {h = h} .{x = x ∷ xs} (here {x = x} {xs = xs} h≡x) (x∉xs ∷ nr-xs) = xs , ≡⇒≋ (≡-cong (λ z → z ∷ xs) (≡-sym h≡x))
h∈x⇒∃t,x≋h∷t {h = h} .{x = x ∷ xs} (there {x = x} {xs = xs} h∈xs) (x∉xs ∷ nr-xs) =
    let t , xs≋h∷t = ((Σ[ t ∈ List _ ] xs ≋ h ∷ t) ∋ h∈x⇒∃t,x≋h∷t h∈xs nr-xs)
        p₁ : x ∷ xs ≋ x ∷ h ∷ t
        p₁ = y≋ỳ⇒x∪y≋x∪ỳ [ x ] xs≋h∷t
        p₂ : x ∷ h ∷ t ≋ h ∷ x ∷ t
        p₂ = ≋-del-ins-l [] [ x ] h t
     in x ∷ t , ≋-trans p₁ p₂

nr-x∪y⇒nr-y : ∀ {ℓ} {A : Set ℓ} (x y : List A) → NonRepetitive (x ∪ y) → NonRepetitive y
nr-x∪y⇒nr-y [] _ nr-y = nr-y
nr-x∪y⇒nr-y (h ∷ t) y (_ ∷ nr-t∪y) = nr-x∪y⇒nr-y t y nr-t∪y

x⊆y⇒∃x̀,y≋x∪x̀ : ∀ {ℓ} {A : Set ℓ} {x y : List A} → NonRepetitive x → NonRepetitive y → x ⊆ y → Σ[ x̀ ∈ List A ] y ≋ x ∪ x̀
x⊆y⇒∃x̀,y≋x∪x̀ {x = []} {y = y} _ _ _ = y , refl
x⊆y⇒∃x̀,y≋x∪x̀ {x = h ∷ t} {y = y} (h∉t ∷ nr-t) nr-y h∷t⊆y =
    let ỳ , y≋h∷ỳ = h∈x⇒∃t,x≋h∷t (h∷t⊆y (h ∈ h ∷ t ∋ here refl)) nr-y
        p₁ : t ⊆ ỳ
        p₁ = x⊆e∷y⇒e∉x⇒x⊆y (x⊆y≋z (x∪y⊆z⇒y⊆z [ h ] t h∷t⊆y) y≋h∷ỳ) h∉t
        nr-ỳ = nr-x∪y⇒nr-y [ h ] ỳ $ nr-x≋y y≋h∷ỳ nr-y
        t̀ , ỳ≋t∪t̀ = x⊆y⇒∃x̀,y≋x∪x̀ nr-t nr-ỳ p₁
        p₂ : h ∷ ỳ ≋ (h ∷ t) ∪ t̀
        p₂ = y≋ỳ⇒x∪y≋x∪ỳ [ h ] ỳ≋t∪t̀
     in t̀ , ≋-trans y≋h∷ỳ p₂

t₁⊆t₂⇒t₂≋t₁∪t₂∖nt₁ : ∀ {ℓ} {A : Set ℓ} {t₁ t₂ : List (Named A)} → NonRepetitiveNames t₁ → NonRepetitiveNames t₂ → t₁ ⊆ t₂ → t₂ ≋ t₁ ∪ t₂ ∖∖ names t₁
t₁⊆t₂⇒t₂≋t₁∪t₂∖nt₁ {t₁ = t₁} {t₂ = t₂} nr-nt₁ nr-nt₂ t₁⊆t₂ = ≋-trans p₁ $ y≋ỳ⇒x∪y≋x∪ỳ t₁ p₆ where
    n-t₁ = names t₁
    nr-t₁ = nr-names⇒nr nr-nt₁
    nr-t₂ = nr-names⇒nr nr-nt₂
    t̀₁,t₁∪t̀₁≋t₂ = x⊆y⇒∃x̀,y≋x∪x̀ nr-t₁ nr-t₂ t₁⊆t₂
    t̀₁ = proj₁ t̀₁,t₁∪t̀₁≋t₂
    p₁ : t₂ ≋ t₁ ∪ t̀₁
    p₁ = proj₂ t̀₁,t₁∪t̀₁≋t₂
    p₂ : t₂ ∖∖ n-t₁ ≋ (t₁ ∪ t̀₁) ∖∖ n-t₁
    p₂ = x≋y⇒x∖n≋y∖n p₁ n-t₁
    p₃ : (t₁ ∪ t̀₁) ∖∖ n-t₁ ≡ t₁ ∖∖ n-t₁ ∪ t̀₁ ∖∖ n-t₁
    p₃ = x∪y∖n≡x∖n∪y∖n t₁ t̀₁ n-t₁
    p₄ : t₁ ∖∖ n-t₁ ∪ t̀₁ ∖∖ n-t₁ ≡ t̀₁ ∖∖ n-t₁
    p₄ = ≡-cong (λ x → x ∪ t̀₁ ∖∖ n-t₁) (x∖x≡[] t₁)
    p₅ : t̀₁ ∖∖ n-t₁ ≡ t̀₁
    p₅ = nr-x∪y⇒x∖y≡x t₁ t̀₁ $ nr-x≋y (n-x≋y p₁) nr-nt₂
    p₆ : t̀₁ ≋ t₂ ∖∖ n-t₁
    p₆ = ≋-sym $ ≋-trans p₂ $ ≡⇒≋ $ ≡-trans p₃ $ ≡-trans p₄ p₅

t₁⊆t₂⇒t₁≋f∈-t₂-nt₁ : ∀ {ℓ} {A : Set ℓ} {t₁ t₂ : List (Named A)} → NonRepetitiveNames t₁ → NonRepetitiveNames t₂ → t₁ ⊆ t₂ → t₁ ≋ filter-∈ t₂ (names t₁)
t₁⊆t₂⇒t₁≋f∈-t₂-nt₁ {t₁ = t₁} {t₂ = t₂} nr-t₁ nr-t₂ t₁⊆t₂ = ≋-trans (≋-sym p₃) p₄ where
    nt₁ = names t₁
    p₁ : t₂ ≋ t₂ ∖∖ nt₁ ∪ t₁
    p₁ = ≋-trans (t₁⊆t₂⇒t₂≋t₁∪t₂∖nt₁ nr-t₁ nr-t₂ t₁⊆t₂) (∪-sym t₁ (t₂ ∖∖ nt₁))
    p₂ : t₂ ≋ t₂ ∖∖ nt₁ ∪ filter-∈ t₂ nt₁
    p₂ = t≋t∖n∪t∩n t₂ nt₁
    p₃ : t₂ ∖∖ names (t₂ ∖∖ nt₁) ≋ t₁
    p₃ = t≋t₁∪t₂⇒t∖t₁≋t₂ nr-t₂ (t₂ ∖∖ nt₁) t₁ p₁
    p₄ : t₂ ∖∖ names (t₂ ∖∖ nt₁) ≋ filter-∈ t₂ nt₁
    p₄ = t≋t₁∪t₂⇒t∖t₁≋t₂ nr-t₂ (t₂ ∖∖ nt₁) (filter-∈ t₂ nt₁) p₂

-- /lemmas

-- assertions

infix 4 _s-≢!_
_s-≢!_ : String → String → Set
x s-≢! y with x ≟ y
... | yes _ = ⊥
... | no  _ = ⊤

s-≢!⇒≢? : ∀ {x y} → x s-≢! y → x ≢ y
s-≢!⇒≢? {x} {y} x≢!y with x ≟ y
s-≢!⇒≢? () | yes _
s-≢!⇒≢? _  | no p = p

s-NonRepetitive? : (n : Names) → Dec (NonRepetitive n)
s-NonRepetitive? [] = yes []
s-NonRepetitive? (h ∷ t) with h ∈? t | s-NonRepetitive? t
... | no h∉t | yes nr-t = yes (h∉t ∷ nr-t)
... | yes h∈t | _ = no f where
                    f : NonRepetitive (_ ∷ _) → _
                    f (h∉t ∷ _) = h∉t h∈t
... | _ | no ¬nr-t = no f where
                    f : NonRepetitive (_ ∷ _) → _
                    f (_ ∷ nr-t) = ¬nr-t nr-t

s-NonRepetitive! : Names → Set
s-NonRepetitive! n with s-NonRepetitive? n
... | yes _ = ⊤
... | no _ = ⊥

NonRepetitiveNames! : ∀ {ℓ} {A : Set ℓ} → List (Named A) → Set
NonRepetitiveNames! = s-NonRepetitive! ∘ names

s-nr!⇒nr : {n : Names} → s-NonRepetitive! n → NonRepetitive n
s-nr!⇒nr {n = n} _ with s-NonRepetitive? n
s-nr!⇒nr _ | yes p = p
s-nr!⇒nr () | no _

-- /assertions


text:
{-# OPTIONS --without-K #-}
module mini-lob where
open import common

infixl 2 _▻_
infixl 3 _‘’_
infixr 1 _‘→’_
infixl 3 _‘’ₐ_

mutual
  data Context : Set where
    ε : Context
    _▻_ : (Γ : Context) → Type Γ → Context

  data Type : Context → Set where
    _‘’_ : ∀ {Γ A} → Type (Γ ▻ A) → Term {Γ} A → Type Γ
    ‘Typeε’ : Type ε
    ‘□’ : Type (ε ▻ ‘Typeε’)
    _‘→’_ : ∀ {Γ} → Type Γ → Type Γ → Type Γ
    ‘⊤’ : ∀ {Γ} → Type Γ
    ‘⊥’ : ∀ {Γ} → Type Γ

  data Term : {Γ : Context} → Type Γ → Set where
    ⌜_⌝ : Type ε → Term {ε} ‘Typeε’
    _‘’ₐ_ : ∀ {Γ A B} → Term {Γ} (A ‘→’ B) → Term {Γ} A → Term {Γ} B
    Lӧb : ∀ {X} → Term {ε} (‘□’ ‘’ ⌜ X ⌝ ‘→’ X) → Term {ε} X
    ‘tt’ : ∀ {Γ} → Term {Γ} ‘⊤’

□ : Type ε → Set _
□ = Term {ε}

max-level : Level
max-level = lzero

mutual
  Context⇓ : (Γ : Context) → Set (lsuc max-level)
  Context⇓ ε = ⊤
  Context⇓ (Γ ▻ T) = Σ (Context⇓ Γ) (Type⇓ {Γ} T)

  Type⇓ : {Γ : Context} → Type Γ → Context⇓ Γ → Set max-level
  Type⇓ (T ‘’ x) Γ⇓ = Type⇓ T (Γ⇓ , Term⇓ x Γ⇓)
  Type⇓ ‘Typeε’ Γ⇓ = Lifted (Type ε)
  Type⇓ ‘□’ Γ⇓ = Lifted (Term {ε} (lower (Σ.proj₂ Γ⇓)))
  Type⇓ (A ‘→’ B) Γ⇓ = Type⇓ A Γ⇓ → Type⇓ B Γ⇓
  Type⇓ ‘⊤’ Γ⇓ = ⊤
  Type⇓ ‘⊥’ Γ⇓ = ⊥

  Term⇓ : ∀ {Γ : Context} {T : Type Γ} → Term T → (Γ⇓ : Context⇓ Γ) → Type⇓ T Γ⇓
  Term⇓ ⌜ x ⌝ Γ⇓ = lift x
  Term⇓ (f ‘’ₐ x) Γ⇓ = Term⇓ f Γ⇓ (Term⇓ x Γ⇓)
  Term⇓ (Lӧb □‘X’→X) Γ⇓ = Term⇓ □‘X’→X Γ⇓ (lift (Lӧb □‘X’→X))
  Term⇓ ‘tt’ Γ⇓ = tt

⌞_⌟ : Type ε → Set _
⌞ T ⌟ = Type⇓ T tt

‘¬’_ : ∀ {Γ} → Type Γ → Type Γ
‘¬’ T = T ‘→’ ‘⊥’

lӧb : ∀ {‘X’} → □ (‘□’ ‘’ ⌜ ‘X’ ⌝ ‘→’ ‘X’) → ⌞ ‘X’ ⌟
lӧb f = Term⇓ (Lӧb f) tt

incompleteness : ¬ □ (‘¬’ (‘□’ ‘’ ⌜ ‘⊥’ ⌝))
incompleteness = lӧb

soundness : ¬ □ ‘⊥’
soundness x = Term⇓ x tt

non-emptyness : Σ (Type ε) (λ T → □ T)
non-emptyness = ‘⊤’ , ‘tt’

max_stars_repo_name: JasonGross/lob

max_issues_repo_name: JasonGross/lob

max_forks_repo_name: JasonGross/lob