text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Interleavings of lists using propositional equality
------------------------------------------------------------------------

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

open import Relation.Binary using (Setoid)

module Data.List.Relation.Ternary.Interleaving.Propositional {a} {A : Set a} where

open import Level using (_⊔_)
open import Data.List.Base as List using (List; []; _∷_; _++_)
open import Data.List.Relation.Binary.Pointwise as Pw using ()
open import Data.List.Relation.Ternary.Interleaving.Properties
open import Data.List.Relation.Binary.Permutation.Inductive as Perm using (_↭_)
open import Data.List.Relation.Binary.Permutation.Inductive.Properties using (shift)
import Data.List.Relation.Ternary.Interleaving.Setoid as General
open import Relation.Binary.PropositionalEquality using (setoid; refl)
open Perm.PermutationReasoning

------------------------------------------------------------------------
-- Re-export the basic combinators

open General hiding (Interleaving) public

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

Interleaving : List A → List A → List A → Set a
Interleaving = General.Interleaving (setoid A)

pattern consˡ xs = refl ∷ˡ xs
pattern consʳ xs = refl ∷ʳ xs

------------------------------------------------------------------------
-- New combinators

toPermutation : ∀ {l r as} → Interleaving l r as → as ↭ l ++ r
toPermutation []         = Perm.refl
toPermutation (consˡ sp) = Perm.prep _ (toPermutation sp)
toPermutation {l} {r ∷ rs} {a ∷ as} (consʳ sp) = begin
  a ∷ as       ↭⟨ Perm.prep a (toPermutation sp) ⟩
  a ∷ l ++ rs  ↭⟨ Perm.↭-sym (shift a l rs) ⟩
  l ++ a ∷ rs  ∎


text:
open import Agda.Builtin.Nat

data Tree : Set where
  `    : Nat → Tree
  _`+_ : Tree → Tree → Tree

⟦_⟧ : Tree → Nat
⟦ ` n    ⟧ = n
⟦ t `+ u ⟧ = ⟦ t ⟧ + ⟦ u ⟧

data Target : Tree → Set where
  0+_ : ∀ e → Target (` 0 `+ e)
  _+0 : ∀ e → Target (e `+ ` 0)
  [_] : ∀ e → Target e

target : ∀ e → Target e
target (` 0 `+ e) = 0+ e
target (e `+ ` 0) = e +0
target e          = [ e ]

optimise   : Tree → Tree
structural : Tree → Tree

optimise t with {structural t} | target (structural t)
... | 0+ e  = e
... | e +0  = e
... | [ e ] = e

structural (` n)    = ` n
structural (e `+ f) = optimise e `+ optimise f

open import Agda.Builtin.Equality

suc-cong : ∀ {m n} → m ≡ n → suc m ≡ suc n
suc-cong refl = refl

+-cong : ∀ {m n p q} → m ≡ n → p ≡ q → m + p ≡ n + q
+-cong refl refl = refl

trans : {m n p : Nat} → m ≡ n → n ≡ p → m ≡ p
trans refl eq = eq

m≡m+0 : ∀ m → m ≡ m + 0
m≡m+0 0       = refl
m≡m+0 (suc m) = suc-cong (m≡m+0 m)

optimise-sound   : ∀ t → ⟦ optimise t ⟧ ≡ ⟦ t ⟧
structural-sound : ∀ t → ⟦ structural t ⟧ ≡ ⟦ t ⟧

optimise-sound t with {structural t} | target (structural t) | structural-sound t
... | 0+ e  | eq = eq
... | e +0  | eq = trans (m≡m+0 ⟦ e ⟧) eq
... | [ e ] | eq = eq

structural-sound (` n)    = refl
structural-sound (e `+ f) = +-cong (optimise-sound e) (optimise-sound f)

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-

Groupoid quotients:

-}

{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.GroupoidQuotients.Properties where

open import Cubical.HITs.GroupoidQuotients.Base

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels

open import Cubical.Functions.Surjection

open import Cubical.Data.Sigma

open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary.Base

open import Cubical.HITs.PropositionalTruncation as PropTrunc using (∥_∥₁; ∣_∣₁; squash₁)
open import Cubical.HITs.SetTruncation as SetTrunc using (∥_∥₂; ∣_∣₂; squash₂)

-- Type quotients

private
  variable
    ℓA ℓR ℓ : Level
    A : Type ℓA
    R : A → A → Type ℓR

elimSet : (Rt : BinaryRelation.isTrans R)
     → {B : A // Rt → Type ℓ}
     → ((x : A // Rt) → isSet (B x))
     → (f : (a : A) → B [ a ])
     → ({a b : A} (r : R a b) → PathP (λ i → B (eq// r i)) (f a) (f b))
     → (x : A // Rt)
     → B x
elimSet Rt Bset f feq [ a ] = f a
elimSet Rt Bset f feq (eq// r i) = feq r i
elimSet Rt Bset f feq (comp// {a} {b} {c} r s i j) =
  isSet→SquareP (λ i j → Bset (comp// r s i j))
    (λ j → feq r j) (λ j → feq (Rt a b c r s) j)
    (λ i → f a) (λ i → feq s i) i j
elimSet Rt Bset f feq (squash// x y p q r s i j k) =
  isOfHLevel→isOfHLevelDep 3 (λ x → isSet→isGroupoid (Bset x))
    _ _ _ _ (λ j k → g (r j k)) (λ j k → g (s j k)) (squash// x y p q r s) i j k
  where
    g = elimSet Rt Bset f feq

elimProp : (Rt : BinaryRelation.isTrans R)
         → {B : A // Rt → Type ℓ}
         → ((x : A // Rt) → isProp (B x))
         → ((a : A) → B [ a ])
         → (x : A // Rt)
         → B x
elimProp Rt Brop f x =
  elimSet Rt (λ x → isProp→isSet (Brop x)) f (λ r → isProp→PathP (λ i → Brop (eq// r i)) (f _) (f _)) x

elimProp2 : (Rt : BinaryRelation.isTrans R)
          → {C : A // Rt → A // Rt → Type ℓ}
         → ((x y : A // Rt) → isProp (C x y))
         → ((a b : A) → C [ a ] [ b ])
         → (x y : A // Rt)
         → C x y
elimProp2 Rt Cprop f = elimProp Rt (λ x → isPropΠ (λ y → Cprop x y))
                                   (λ x → elimProp Rt (λ y → Cprop [ x ] y) (f x))

isSurjective[] : (Rt : BinaryRelation.isTrans R)
               → isSurjection (λ a → [ a ])
isSurjective[] Rt = elimProp Rt (λ x → squash₁) (λ a → ∣ a , refl ∣₁)

elim : (Rt : BinaryRelation.isTrans R)
     → {B : A // Rt → Type ℓ}
     → ((x : A // Rt) → isGroupoid (B x))
     → (f : (a : A) → B [ a ])
     → (feq : {a b : A} (r : R a b) → PathP (λ i → B (eq// r i)) (f a) (f b))
     → ({a b c : A} (r : R a b) (s : R b c)
           → SquareP (λ i j → B (comp// r s i j))
           (feq r) (feq (Rt a b c r s)) (λ j → f a) (feq s))
     → (x : A // Rt)
     → B x
elim Rt Bgpd f feq fcomp [ a ] = f a
elim Rt Bgpd f feq fcomp (eq// r i) = feq r i
elim Rt Bgpd f feq fcomp (comp// r s i j) = fcomp r s i j
elim Rt Bgpd f feq fcomp (squash// x y p q r s i j k) =
  isOfHLevel→isOfHLevelDep 3 Bgpd
    _ _ _ _ (λ j k → g (r j k)) (λ j k → g (s j k)) (squash// x y p q r s) i j k
  where
    g = elim Rt Bgpd f feq fcomp

rec : (Rt : BinaryRelation.isTrans R)
    → {B : Type ℓ}
    → isGroupoid B
    → (f : A → B)
    → (feq : {a b : A} (r : R a b) → f a ≡ f b)
    → ({a b c : A} (r : R a b) (s : R b c)
          → Square (feq r) (feq (Rt a b c r s)) refl (feq s))
    → (x : A // Rt)
    → B
rec Rt Bgpd = elim Rt (λ _ → Bgpd)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- {-# OPTIONS -v tc.lhs.problem:10 #-}
-- Do not normalize goals!
module Issue734 where

id : Set → Set
id A = A

g : (A : Set) → id A
g A = {!!}
-- goal should be displayed as "id A", not as "A"

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Solutions to ExerciseSession3
{-# OPTIONS --cubical #-}
module SolutionsSession3 where

open import Part1
open import Part2
open import Part3
open import Part4 hiding (ℤ)
open import ExerciseSession1 hiding (B)

open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Nat
open import Cubical.Data.Int hiding (neg)

-- Exercise 1
assoc-++ : (xs ys zs : FMSet A) → xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
assoc-++ []       ys zs = refl
assoc-++ (x ∷ xs) ys zs j = x ∷ assoc-++ xs ys zs j
assoc-++ (comm x y xs i) ys zs j = comm x y (assoc-++ xs ys zs j) i
assoc-++ (trunc xs xs' p q i k) ys zs j =
  trunc (assoc-++ xs ys zs j) (assoc-++ xs' ys zs j)
        (λ l → assoc-++ (p l) ys zs j)
        (λ l → assoc-++ (q l) ys zs j) i k

-- Exercise 2
data ℤ : Type₀ where
  pos    : (n : ℕ) → ℤ
  neg    : (n : ℕ) → ℤ
  posneg : pos 0 ≡ neg 0

-- Exercise 3
Int→ℤ : Int → ℤ
Int→ℤ (pos n) = pos n
Int→ℤ (negsuc n) = neg (suc n)

ℤ→Int : ℤ → Int
ℤ→Int (pos n) = pos n
ℤ→Int (neg zero) = pos 0
ℤ→Int (neg (suc n)) = negsuc n
ℤ→Int (posneg _) = pos 0

ℤ→Int→ℤ : ∀ (n : ℤ) → Int→ℤ (ℤ→Int n) ≡ n
ℤ→Int→ℤ (pos n) _       = pos n
ℤ→Int→ℤ (neg zero) i    = posneg i
ℤ→Int→ℤ (neg (suc n)) _ = neg (suc n)
ℤ→Int→ℤ (posneg j) i    = posneg (j ∧ i)

Int→ℤ→Int : ∀ (n : Int) → ℤ→Int (Int→ℤ n) ≡ n
Int→ℤ→Int (pos n) _ = pos n
Int→ℤ→Int (negsuc n) _ = negsuc n

Int≡ℤ : Int ≡ ℤ
Int≡ℤ = isoToPath (iso Int→ℤ ℤ→Int ℤ→Int→ℤ Int→ℤ→Int)

isSetℤ : isSet ℤ
isSetℤ = subst isSet Int≡ℤ isSetInt

-- Exercise 4
isSurjection : (A → B) → Type _
isSurjection {A = A} {B = B} f = (b : B) → ∃ A (λ a → f a ≡ b)

isPropIsSurjection : (f : A → B) → isProp (isSurjection f)
isPropIsSurjection f = isPropΠ (λ _ → squash)

isSurjectionInc : isSurjection {A = A} ∣_∣
isSurjectionInc x = rec squash (λ y → ∣ (y , squash ∣ y ∣ x) ∣) x

-- Exercise 5
intLoop : Int → ΩS¹
intLoop (pos zero)       = refl
intLoop (pos (suc n))    = intLoop (pos n) ∙ loop
intLoop (negsuc zero)    = sym loop
intLoop (negsuc (suc n)) = intLoop (negsuc n) ∙ sym loop

windingIntLoop : (n : Int) → winding (intLoop n) ≡ n
windingIntLoop (pos zero)       = refl
windingIntLoop (pos (suc n))    = cong sucInt (windingIntLoop (pos n))
windingIntLoop (negsuc zero)    = refl
windingIntLoop (negsuc (suc n)) = cong predInt (windingIntLoop (negsuc n))

-- Exercise 6

data Susp (A : Type ℓ) : Type ℓ where
  north : Susp A
  south : Susp A
  merid : (a : A) → north ≡ south

SuspBool→S¹ : Susp Bool → S¹
SuspBool→S¹ north = base
SuspBool→S¹ south = base
SuspBool→S¹ (merid false i) = loop i
SuspBool→S¹ (merid true i)  = base

S¹→SuspBool : S¹ → Susp Bool
S¹→SuspBool base     = north
S¹→SuspBool (loop i) = (merid false ∙ sym (merid true)) i

SuspBool→S¹→SuspBool : (x : Susp Bool) → Path _ (S¹→SuspBool (SuspBool→S¹ x)) x
SuspBool→S¹→SuspBool north = refl
SuspBool→S¹→SuspBool south = merid true
SuspBool→S¹→SuspBool (merid false i) j = hcomp (λ k → (λ { (j = i1) → merid false i
                                                         ; (i = i0) → north
                                                         ; (i = i1) → merid true (j ∨ ~ k)}))
                                               (merid false i)
SuspBool→S¹→SuspBool (merid true i) j = merid true (i ∧ j)

S¹→SuspBool→S¹ : (x : S¹) → SuspBool→S¹ (S¹→SuspBool x) ≡ x
S¹→SuspBool→S¹ base       = refl
S¹→SuspBool→S¹ (loop i) j = hfill (λ k → λ { (i = i0) → base
                                           ; (i = i1) → base })
                                  (inS (loop i)) (~ j)

S¹≡SuspBool : S¹ ≡ Susp Bool
S¹≡SuspBool = isoToPath (iso S¹→SuspBool SuspBool→S¹ SuspBool→S¹→SuspBool S¹→SuspBool→S¹)


text:
module subst where

open import constants
open import cedille-types
open import ctxt-types
open import free-vars
open import rename
open import general-util
open import syntax-util
open import type-util

substh-ret-t : Set → Set
substh-ret-t T = ctxt → renamectxt → trie (Σi exprd ⟦_⟧) → T → T

{-# TERMINATING #-}
substh : ∀ {ed} → substh-ret-t ⟦ ed ⟧
substh-arg : substh-ret-t arg
substh-args : substh-ret-t args
substh-params' : ctxt → renamectxt → trie (Σi exprd ⟦_⟧) → params → params × ctxt × renamectxt × trie (Σi exprd ⟦_⟧)
substh-indices : substh-ret-t indices
substh-params : substh-ret-t params
substh-case : substh-ret-t case
substh-cases : substh-ret-t cases
substh-case-args : ctxt → renamectxt → trie (Σi exprd ⟦_⟧) → case-args → case-args × renamectxt × ctxt × trie (Σi exprd ⟦_⟧)
substh-datatype-info : substh-ret-t datatype-info

subst-rename-var-if : ∀ {ed} → ctxt → renamectxt → var → trie (Σi exprd ⟦_⟧) → ⟦ ed ⟧ → var
subst-rename-var-if Γ ρ ignored-var σ t = if is-free-in ignored-var t then fresh-h (λ s → ctxt-binds-var Γ s || trie-contains σ s || renamectxt-in-field ρ s) "x" else ignored-var
subst-rename-var-if Γ ρ x σ _ =
  {- rename bound variable x iff it is one of the vars being substituted for,
     or if x occurs free in one of the terms we are substituting for vars,
     or if it is the renamed version of any variable -}
  if trie-contains σ x {-|| trie-any (λ {(,_ {ed} t) → is-free-in x t}) σ-} || renamectxt-in-range ρ x || ctxt-binds-var Γ x then
    fresh-h (λ s → ctxt-binds-var Γ s || trie-contains σ s || renamectxt-in-field ρ s) x
  else
    x

substh {TERM} Γ ρ σ (App t t') = App (substh Γ ρ σ t) (substh Γ ρ σ t')
substh {TERM} Γ ρ σ (AppE t tT) = AppE (substh Γ ρ σ t) (substh Γ ρ σ -tT tT)
substh {TERM} Γ ρ σ (Lam me x oc t) =
  let x' = subst-rename-var-if Γ ρ x σ t in
    Lam me x' (substh Γ ρ σ -tk_ <$> oc)
      (substh (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') σ t)
substh {TERM} Γ ρ σ (LetTm me x T t t') =
  let x' = subst-rename-var-if Γ ρ x σ t' in
    LetTm me x' (substh Γ ρ σ <$> T) (substh Γ ρ σ t)
      (substh (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') σ t')
substh {TERM} Γ ρ σ (LetTp x k T t) =
  let x' = subst-rename-var-if Γ ρ x σ t in
    LetTp x' (substh Γ ρ σ k) (substh Γ ρ σ T)
      (substh (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') σ t)
substh {TERM} Γ ρ σ (Var x) =
 let x' = renamectxt-rep ρ x in
   case trie-lookup σ x' of λ where
     (just (,_ {TERM} t)) → t
     _ → Var x'
substh {TERM} Γ ρ σ (Hole pi) = Hole pi -- Retain position, so jumping to hole works
substh {TERM} Γ ρ σ (Beta t t') = Beta (substh Γ ρ σ t) (substh Γ ρ σ t')
substh {TERM} Γ ρ σ (IotaPair t₁ t₂ x T) =
  let x' = subst-rename-var-if Γ ρ x σ T in
  IotaPair (substh Γ ρ σ t₁) (substh Γ ρ σ t₂) x' (substh (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') σ T)
substh {TERM} Γ ρ σ (IotaProj t n) = IotaProj (substh Γ ρ σ t) n
substh {TERM} Γ ρ σ (Sigma t) = Sigma (substh Γ ρ σ t)
substh {TERM} Γ ρ σ (Phi t t₁ t₂) = Phi (substh Γ ρ σ t) (substh Γ ρ σ t₁) (substh Γ ρ σ t₂)
substh {TERM} Γ ρ σ (Rho tₑ x T t) =
  let x' = subst-rename-var-if Γ ρ x σ T in
  Rho (substh Γ ρ σ tₑ) x' (substh (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') σ T) (substh Γ ρ σ t)
substh {TERM} Γ ρ σ (Delta b? T t) =
  Delta (b? >>=c λ t₁ t₂ → just (substh Γ ρ σ t₁ , substh Γ ρ σ t₂))
        (substh Γ ρ σ T) (substh Γ ρ σ t)
substh {TERM} Γ ρ σ (Mu (inj₂ x) t T t~ ms) =
  let fv = λ x → trie-contains σ x || ctxt-binds-var Γ x || renamectxt-in-field ρ x
      x' = fresh-h (λ x → fv x || fv (mu-Type/ x) || fv (mu-isType/ x))
                   (if x =string ignored-var then "x" else x)
      ρ' = renamectxt-insert ρ x x'
      ρ' = renamectxt-insert ρ' (mu-Type/ x) (mu-Type/ x')
      ρ' = renamectxt-insert ρ' (mu-isType/ x) (mu-isType/ x')
      Γ' = ctxt-var-decl x' Γ
      Γ' = ctxt-var-decl (mu-Type/ x') Γ'
      Γ' = ctxt-var-decl (mu-isType/ x') Γ' in
    Mu (inj₂ x') (substh Γ ρ σ t) (substh (ctxt-var-decl (mu-Type/ x') Γ) (renamectxt-insert ρ (mu-Type/ x) (mu-Type/ x')) σ <$> T) (substh-datatype-info Γ ρ σ t~) (substh-cases Γ' ρ' σ ms)
substh {TERM} Γ ρ σ (Mu (inj₁ tᵢ) t' T t~ ms) =
  Mu (inj₁ (substh Γ ρ σ <$> tᵢ)) (substh Γ ρ σ t') (substh Γ ρ σ <$> T) (substh-datatype-info Γ ρ σ t~) (substh-cases Γ ρ σ ms)

substh {TYPE} Γ ρ σ (TpAbs me x tk t) =
  let x' = subst-rename-var-if Γ ρ x σ t in
    TpAbs me x' (substh Γ ρ σ -tk tk)
      (substh (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') σ t)
substh {TYPE} Γ ρ σ (TpLam x tk t) =
  let x' = subst-rename-var-if Γ ρ x σ t in
    TpLam x' (substh Γ ρ σ -tk tk)
      (substh (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') σ t)
substh {TYPE} Γ ρ σ (TpIota x T₁ T₂) =
  let x' = subst-rename-var-if Γ ρ x σ T₂ in
    TpIota x' (substh Γ ρ σ T₁)
      (substh (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') σ T₂)
substh {TYPE} Γ ρ σ (TpApp tp tT) = TpApp (substh Γ ρ σ tp) (substh Γ ρ σ -tT tT)
substh {TYPE} Γ ρ σ (TpEq t₁ t₂) = TpEq (substh Γ ρ σ t₁) (substh Γ ρ σ t₂)
substh {TYPE} Γ ρ σ (TpVar x) =
 let x' = renamectxt-rep ρ x in
   case trie-lookup σ x' of λ where
     (just (,_ {TYPE} T)) → T
     _ → TpVar x'
substh {TYPE} Γ ρ σ (TpHole pi) = TpHole pi -- Retain position, so jumping to hole works

substh {KIND} Γ ρ σ (KdAbs x tk k) =
  let x' = subst-rename-var-if Γ ρ x σ k in
    KdAbs x' (substh Γ ρ σ -tk tk)
      (substh (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') σ k)
substh {KIND} Γ ρ σ (KdHole pi) = KdHole pi -- Retain position, so jumping to hole works
substh {KIND} Γ ρ σ KdStar = KdStar

substh-datatype-info Γ ρ σ (mk-data-info X Xₒ asₚ asᵢ ps kᵢ k cs csₚₛ gds eds) =
  let Γ' = foldr (λ { (Param me x tk) Γ → ctxt-var-decl x Γ       }) Γ ps
      ρ' = foldr (λ { (Param me x tk) ρ → renamectxt-insert ρ x x }) ρ ps
      σ' = foldr (λ { (Param me x tk) σ → trie-remove σ x         }) σ ps in
  mk-data-info
    (renamectxt-rep ρ X)
    (renamectxt-rep ρ Xₒ)
    (substh Γ ρ σ -arg_ <$> asₚ)
    (substh Γ ρ σ -tT_ <$> asᵢ)
    ps
    (substh Γ' ρ' σ' kᵢ)
    (substh Γ' ρ' σ' k)
    (map-snd (substh Γ' ρ' σ') <$> cs)
    (map-snd (substh Γ ρ σ) <$> csₚₛ)
    gds
    eds

substh-arg Γ ρ σ = substh Γ ρ σ -arg_

substh-args Γ ρ σ = substh-arg Γ ρ σ <$>_

substh-params' Γ ρ σ ((Param me x tk) :: ps) =
  map-fst (Param me x (substh Γ ρ σ -tk tk) ::_)
    (substh-params' Γ (renamectxt-insert ρ x x) (trie-remove σ x) ps)
substh-params' Γ ρ σ [] = [] , Γ , ρ , σ

substh-params Γ ρ σ ps = fst (substh-params' Γ ρ σ ps)

substh-indices Γ ρ σ = params-to-indices ∘' substh-params Γ ρ σ ∘' indices-to-params

substh-case Γ ρ σ (Case x as t asₜₚ) =
  case (substh-case-args Γ ρ σ as) of λ where
    (as' , ρ' , Γ' , σ') →
      Case x as' (substh Γ' ρ' σ' t) (substh Γ' ρ' σ' -tT_ <$> asₜₚ)

substh-cases Γ ρ σ = map (substh-case Γ ρ σ)

substh-case-args Γ ρ σ as = foldr (λ where
  (CaseArg e x tk) f ρ Γ σ →
    let x' = subst-rename-var-if Γ ρ x σ (Var x) in
    map-fst (CaseArg e x' (substh Γ ρ σ -tk_ <$> tk) ::_)
            (f (renamectxt-insert ρ x x') (ctxt-var-decl x' Γ) (trie-remove σ x)))
  (λ ρ Γ σ → [] , ρ , Γ , σ) as ρ Γ σ

subst-ret-t : Set → Set
subst-ret-t T = {ed : exprd} → ctxt → ⟦ ed ⟧ → var → T → T

subst : ∀ {ed} → subst-ret-t ⟦ ed ⟧
subst Γ t x = substh Γ empty-renamectxt (trie-single x (, t))

subst-cases : subst-ret-t cases
subst-cases Γ t x = substh-cases Γ empty-renamectxt (trie-single x (, t))

subst-params : subst-ret-t params
subst-params Γ t x = substh-params Γ empty-renamectxt (trie-single x (, t))

subst-renamectxt : ∀ {ed : exprd} → ctxt → renamectxt → ⟦ ed ⟧ → ⟦ ed ⟧
subst-renamectxt Γ ρ = substh Γ ρ empty-trie

rename-var : ∀ {ed} → ctxt → var → var → ⟦ ed ⟧ → ⟦ ed ⟧
rename-var Γ x x' = subst-renamectxt Γ (renamectxt-single x x')

substs-ret-t : Set → Set
substs-ret-t T = ctxt → trie (Σi exprd ⟦_⟧) → T → T

substs : ∀ {ed} → substs-ret-t ⟦ ed ⟧
substs = flip substh empty-renamectxt

substs-args : substs-ret-t args
substs-args = flip substh-args empty-renamectxt

substs-params : substs-ret-t params
substs-params = flip substh-params empty-renamectxt

substs-cases : substs-ret-t cases
substs-cases = flip substh-cases empty-renamectxt

subst-params-args : params → args → trie (Σi exprd ⟦_⟧) × params × args
subst-params-args ps as = subst-params-args' ps as empty-trie where
  subst-params-args' : params → args → trie (Σi exprd ⟦_⟧) → trie (Σi exprd ⟦_⟧) × params × args
  subst-params-args' (Param me x tk :: ps) (Arg t :: as) σ =
    subst-params-args' ps as (trie-insert σ x (, t))
  subst-params-args' (Param me x tk :: ps) (ArgE (inj₁ t) :: as) σ =
    subst-params-args' ps as (trie-insert σ x (, t))
  subst-params-args' (Param me x tk :: ps) (ArgE (inj₂ T) :: as) σ =
    subst-params-args' ps as (trie-insert σ x (, T))
  subst-params-args' ps as σ = σ , ps , as

subst-params-args' : ctxt → params → args → ∀ {ed} → ⟦ ed ⟧ → ⟦ ed ⟧ × params × args
subst-params-args' Γ ps as t = map-fst (λ σ → substs Γ σ t) (subst-params-args ps as)

infixr 3 [_-_/_]_
[_-_/_]_ : ∀ {ed ed'} → ctxt → ⟦ ed ⟧ → var → ⟦ ed' ⟧ → ⟦ ed' ⟧
[ Γ - t / x ] t' = subst Γ t x t'

subst-unqual : ∀ {ed} → ctxt → 𝕃 (posinfo × var) → ⟦ ed ⟧ → ⟦ ed ⟧
subst-unqual Γ xs t =
  subst-renamectxt
    Γ
    (foldr (uncurry λ pi x xs → renamectxt-insert xs (pi % x) x) empty-renamectxt xs)
    t

-- Given the parameters (32@x : ...) (41@y : ...32@x...),
-- returns (x : ...) (y : ...x...) × (32@x → x, 41@y → y)
unqual-params : ctxt → params → params × renamectxt
unqual-params = h empty-renamectxt where
  h : renamectxt → ctxt → params → params × renamectxt
  h ρ Γ [] = [] , ρ
  h ρ Γ (Param me qx atk :: ps) =
    let x = unqual-local qx in
    map-fst (Param me x (subst-renamectxt Γ ρ -tk atk) ::_)
      (h (renamectxt-insert ρ qx x) (ctxt-var-decl x Γ) ps)

max_stars_repo_name: zmthy/cedille

max_issues_repo_name: zmthy/cedille

max_forks_repo_name: zmthy/cedille


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

open import Groups.Definition
open import Setoids.Setoids
open import LogicalFormulae
open import Sets.EquivalenceRelations
open import Groups.Homomorphisms.Definition
open import Groups.Homomorphisms.Lemmas
open import Groups.Isomorphisms.Definition
open import Groups.Subgroups.Definition
open import Groups.Lemmas

module Groups.FirstIsomorphismTheorem {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+G_ : A → A → A} {_+H_ : B → B → B} {G : Group S _+G_} {H : Group T _+H_} {f : A → B} (fHom : GroupHom G H f) where

open import Groups.Homomorphisms.Image fHom
open import Groups.Homomorphisms.Kernel fHom
open import Groups.Cosets G groupKernelIsSubgroup
open import Groups.QuotientGroup.Definition G fHom
open Setoid T
open Equivalence eq
open import Setoids.Subset T

groupFirstIsomorphismTheoremWellDefined : {x y : A} → groupKernelPred (Group.inverse G y +G x) → Setoid._∼_ (subsetSetoid imageGroupSubset) (f x , (x , reflexive)) (f y , (y , reflexive))
groupFirstIsomorphismTheoremWellDefined {x} {y} pr = transitive (symmetric (invTwice H _)) (transitive (symmetric u) (invTwice H _))
  where
    t : Setoid._∼_ T (Group.inverse H (f y) +H (f x)) (Group.0G H)
    t = transitive (transitive (Group.+WellDefined H (symmetric (homRespectsInverse fHom)) reflexive) (symmetric (GroupHom.groupHom fHom))) pr
    u : Setoid._∼_ T (Group.inverse H (Group.inverse H (f y))) (Group.inverse H (Group.inverse H (f x)))
    u = inverseWellDefined H (transferToRight' H t)

groupFirstIsomorphismTheorem : GroupsIsomorphic (cosetGroup groupKernelIsNormalSubgroup) (subgroupIsGroup H imageGroupSubgroup)
GroupsIsomorphic.isomorphism groupFirstIsomorphismTheorem x = f x , (x , reflexive)
GroupHom.groupHom (GroupIso.groupHom (GroupsIsomorphic.proof groupFirstIsomorphismTheorem)) {x} {y} = GroupHom.groupHom fHom
GroupHom.wellDefined (GroupIso.groupHom (GroupsIsomorphic.proof groupFirstIsomorphismTheorem)) {x} {y} = groupFirstIsomorphismTheoremWellDefined {x} {y}
SetoidInjection.wellDefined (SetoidBijection.inj (GroupIso.bij (GroupsIsomorphic.proof groupFirstIsomorphismTheorem))) = groupFirstIsomorphismTheoremWellDefined
SetoidInjection.injective (SetoidBijection.inj (GroupIso.bij (GroupsIsomorphic.proof groupFirstIsomorphismTheorem))) fx=fy = transitive (GroupHom.groupHom fHom) (transitive (Group.+WellDefined H reflexive fx=fy) (transitive (symmetric (GroupHom.groupHom fHom)) (transitive (GroupHom.wellDefined fHom (Group.invLeft G)) (imageOfIdentityIsIdentity fHom))))
SetoidSurjection.wellDefined (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof groupFirstIsomorphismTheorem))) = groupFirstIsomorphismTheoremWellDefined
SetoidSurjection.surjective (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof groupFirstIsomorphismTheorem))) {b , (a , fa=b)} = a , fa=b

groupFirstIsomorphismTheoremWellDefined' : {x y : A} → f (x +G (Group.inverse G y)) ∼ Group.0G H → Setoid._∼_ (subsetSetoid imageGroupSubset) (f x , (x , reflexive)) (f y , (y , reflexive))
groupFirstIsomorphismTheoremWellDefined' {x} {y} pr = transferToRight H (transitive (symmetric (transitive (GroupHom.groupHom fHom) (Group.+WellDefined H reflexive (homRespectsInverse fHom)))) pr)

groupFirstIsomorphismTheorem' : GroupsIsomorphic (quotientGroupByHom) (subgroupIsGroup H imageGroupSubgroup)
GroupsIsomorphic.isomorphism groupFirstIsomorphismTheorem' a = f a , (a , reflexive)
GroupHom.groupHom (GroupIso.groupHom (GroupsIsomorphic.proof groupFirstIsomorphismTheorem')) {x} {y} = GroupHom.groupHom fHom
GroupHom.wellDefined (GroupIso.groupHom (GroupsIsomorphic.proof groupFirstIsomorphismTheorem')) {x} {y} = groupFirstIsomorphismTheoremWellDefined'
SetoidInjection.wellDefined (SetoidBijection.inj (GroupIso.bij (GroupsIsomorphic.proof groupFirstIsomorphismTheorem'))) {x} {y} = groupFirstIsomorphismTheoremWellDefined' {x} {y}
SetoidInjection.injective (SetoidBijection.inj (GroupIso.bij (GroupsIsomorphic.proof groupFirstIsomorphismTheorem'))) {x} {y} fx=fy = transitive (GroupHom.groupHom fHom) (transitive (Group.+WellDefined H reflexive (homRespectsInverse fHom)) (transferToRight'' H fx=fy))
SetoidSurjection.wellDefined (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof groupFirstIsomorphismTheorem'))) {x} {y} = groupFirstIsomorphismTheoremWellDefined'
SetoidSurjection.surjective (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof groupFirstIsomorphismTheorem'))) {b , (a , fa=b)} = a , fa=b


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

-- The Category of Presheaves over a Category C, i.e.
-- the Functor Category [ C.op , Setoids ]
-- Again, the levels are made explicit to show the generality and constraints.
open import Level

open import Categories.Category
open import Categories.Category.Construction.Functors
open import Categories.Category.Instance.Setoids using (Setoids)

Presheaves : ∀ {o ℓ e o′ ℓ′ : Level} → Category o ℓ e →
  Category (o ⊔ ℓ ⊔ e ⊔ suc (o′ ⊔ ℓ′)) (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) (o ⊔ o′ ⊔ ℓ′)
Presheaves {o} {ℓ} {e} {o′} {ℓ′} C = Functors (Category.op C) (Setoids o′ ℓ′)

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


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

module FinEquivEquivPlusTimes where

open import Data.Product using (_×_; proj₁; proj₂)

open import Equiv using (refl∼; sym∼; sym≃; _⊎≃_; id≃; _≃_; _●_; _×≃_; qinv)

open import FinEquivPlusTimes using (F0≃⊥; module Plus; module Times)
open Plus using (⊎≃+; +≃⊎)
open Times using (×≃*; *≃×)

open import FinEquivTypeEquiv
  using (_fin≃_; module PlusE; module TimesE; module PlusTimesE)
open PlusE using (_+F_; unite+; uniti+; unite+r; uniti+r; assocr+; assocl+;
                 swap+; sswap+)
open TimesE using (_*F_; unite*; uniti*; unite*r; uniti*r; assocr*; assocl*;
                  swap*; sswap*)
open PlusTimesE using (distz; factorz; distzr; factorzr;
                       dist; factor; distl; factorl)
open import EquivEquiv
open import TypeEquiv
  using (unite₊equiv; unite₊′equiv; assocl₊equiv)

open import Data.Empty using (⊥)
open import Data.Unit using (⊤)
open import Data.Nat using (ℕ; _+_; _*_)
open import Data.Fin using (Fin)
open import Data.Sum using (_⊎_)
open import Data.Product using (_,_)
import Relation.Binary.PropositionalEquality as P using (refl)

import TypeEquivEquiv as T
  using (
    -- much lower down
    0×0≃0)

------------------------------------------------------------------------------
-- Equivalences for distributivity

distl-nat : {m n o m' n' o' : ℕ}
    {f : m fin≃ m'} {g : n fin≃ n'} {h : o fin≃ o'} →
    distl {m'} {n'} {o'} ● (f *F (g +F h)) ≋
      ((f *F g) +F (f *F h)) ● distl {m} {n} {o}
distl-nat = {!!}

factorl-nat : {m n o m' n' o' : ℕ}
    {f : m fin≃ m'} {g : n fin≃ n'} {h : o fin≃ o'} →
    factorl {m'} {n'} {o'} ● ((f *F g) +F (f *F h)) ≋
      (f *F (g +F h)) ● factorl {m} {n} {o}
factorl-nat = {!!}

dist-nat : {m n o m' n' o' : ℕ}
    {f : m fin≃ m'} {g : n fin≃ n'} {h : o fin≃ o'} →
    dist {m'} {n'} {o'} ● ((f +F g) *F h) ≋
      ((f *F h) +F (g *F h)) ● dist {m} {n} {o}
dist-nat = {!!}

factor-nat : {m n o m' n' o' : ℕ}
    {f : m fin≃ m'} {g : n fin≃ n'} {h : o fin≃ o'} →
    factor {m'} {n'} {o'} ● ((f *F h) +F (g *F h)) ≋
      ((f +F g) *F h) ● factor {m} {n} {o}
factor-nat = {!!}

distzr-nat : {m n : ℕ} {f : m fin≃ n} {g : 0 fin≃ 0} →
    distzr {n} ● (f *F g) ≋ g ● distzr {m}
distzr-nat = {!!}

factorzr-nat : {m n : ℕ} {f : m fin≃ n} {g : 0 fin≃ 0} →
    factorzr {n} ● g ≋ (f *F g) ● factorzr {m}
factorzr-nat = {!!}

distz-nat : {m n : ℕ} → {f : m fin≃ n} → {g : 0 fin≃ 0} →
    distz {n} ● (g *F f) ≋ g ● distz {m}
distz-nat = {!!}

factorz-nat : {m n : ℕ} → {f : m fin≃ n} → {g : 0 fin≃ 0} →
    factorz {n} ● g ≋ (g *F f) ● factorz {m}
factorz-nat = {!!}

A×[B⊎C]≃[A×C]⊎[A×B] : {m n o : ℕ} →
    distl {m} {o} {n} ● (id≃ {A = Fin m} *F swap+ {n} {o}) ≋
    swap+ {m * n} {m * o} ● distl {m} {n} {o}
A×[B⊎C]≃[A×C]⊎[A×B] = {!!}

[A⊎B]×C≃[C×A]⊎[C×B] : {m n o : ℕ} →
    (swap* {m} {o} +F swap* {n} {o}) ● dist {m} {n} {o} ≋
    distl {o} {m} {n} ● swap* {m + n} {o}
[A⊎B]×C≃[C×A]⊎[C×B] = {!!}

[A⊎B⊎C]×D≃[A×D⊎B×D]⊎C×D : {m n o p : ℕ} →
    (dist {m} {n} {p} +F id≃ {A = Fin (o * p)}) ●
      dist {m + n} {o} {p} ● (assocl+ {m} {n} {o} *F id≃ {A = Fin p}) ≋
    assocl+ {m * p} {n * p} {o * p} ●
      (id≃ {A = Fin (m * p)} +F dist {n} {o} {p}) ● dist {m} {n + o} {p}
[A⊎B⊎C]×D≃[A×D⊎B×D]⊎C×D = {!!}

A×B×[C⊎D]≃[A×B]×C⊎[A×B]×D : {m n o p : ℕ} →
    distl {m * n} {o} {p} ● assocl* {m} {n} {o + p} ≋
    (assocl* {m} {n} {o} +F assocl* {m} {n} {p}) ●
      distl {m} {n * o} {n * p} ● (id≃ {A = Fin m} *F distl {n} {o} {p})
A×B×[C⊎D]≃[A×B]×C⊎[A×B]×D = {!!}

[A⊎B]×[C⊎D]≃[[A×C⊎B×C]⊎A×D]⊎B×D : {m n o p : ℕ} →
    assocl+ {(m * o) + (n * o)} {m * p} {n * p} ●
      (dist {m} {n} {o} +F dist {m} {n} {p}) ●
      distl {m + n} {o} {p} ≋
    (assocl+ {m * o} {n * o} {m * p} +F id≃ {A = Fin (n * p)}) ●
      ((id≃ {A = Fin (m * o)} +F swap+ {m * p} {n * o}) +F id≃ {A = Fin (n * p)}) ●
      (assocr+ {m * o} {m * p} {n * o} +F id≃ {A = Fin (n * p)}) ●
      assocl+ {(m * o) + (m * p)} {n * o} {n * p} ●
      (distl {m} {o} {p} +F distl {n} {o} {p}) ● dist {m} {n} {o + p}
[A⊎B]×[C⊎D]≃[[A×C⊎B×C]⊎A×D]⊎B×D = {!!}

-- can't be done via equational reasoning!?!?
-- cannot even dig into T.0×0≃0 as f≋ is abstract
0×0≃0 : distz {0} ≋ distzr {0}
0×0≃0 = eq (λ {()}) (λ {()}) -- wow, talk about low-level reasoning!

0×[A⊎B]≃0 : {m n : ℕ} →
    distz {m + n} ≋ unite+ ● (distz {m} +F distz {n}) ● distl {0} {m} {n}
0×[A⊎B]≃0 = {!!}

0×1≃0 : unite*r ≋ distz {1}
0×1≃0 = {!!}

A×0≃0 : {m : ℕ} → distzr {m} ≋ distz {m} ● swap* {m} {0}
A×0≃0 = {!!}

0×A×B≃0 : {m n : ℕ} →
    distz {m * n} ≋
    distz {n} ● (distz {m} *F id≃ {A = Fin n}) ● assocl* {0} {m} {n}
0×A×B≃0 = {!!}

A×0×B≃0 : {m n : ℕ} →
    distzr {m} ● (id≃ {A = Fin m} *F distz {n})  ≋
    distz {n} ● (distzr {m} *F id≃ {A = Fin n}) ● assocl* {m} {0} {n}
A×0×B≃0 = {!!}

A×[0+B]≃A×B : {m n : ℕ} →
    (id≃ {A = Fin m} *F unite+ {n}) ≋
    unite+ ● (distzr {m} +F id≃) ● distl {m} {0} {n}
A×[0+B]≃A×B = {!!}

1×[A⊎B]≃A⊎B : {m n : ℕ} →
    unite* ≋ (unite* {m} +F unite* {n}) ● distl {1} {m} {n}
1×[A⊎B]≃A⊎B = {!!}

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
open import MJ.Types as Types
import MJ.Classtable.Core as Core

module MJ.Semantics.Values {c}(Ct : Core.Classtable c) where

open import Prelude

open import Level renaming (suc to lsuc; zero to lzero)
open import Data.List hiding (null)
open import Data.List.Membership.Propositional
open import Data.List.Prefix

open Core c
open Classtable Ct
open import MJ.Classtable.Membership Ct
open import MJ.LexicalScope c
open import Common.Weakening

{-
MJ inherits the values of STLC+Ref. In contrast to STCL+Ref, MJ also has
null-pointers; which we add as a constructor to our value type Val. The value
constructed by null is typed with an arbitrary reference type as it can be used
in place of any proper reference.
-}
data Val (W : World c) : Ty c → Set where
  num  : ℕ → Val W int
  unit : Val W void
  null : ∀ {C} → Val W (ref C)
  ref  : ∀ {C P} → (obj C) ∈ W → Σ ⊢ C <: P → Val W (ref P)

{-
We can construct default values out of thin air for every type
-}
default : ∀ {W} → (a : Ty c) → Val W a
default void = unit
default int = num 0
default (ref x) = null

{-
Value weakening
-}
weaken-val : ∀ {a}{W W' : World c} → W ⊒ W' → Val W' a → Val W a
weaken-val ext (num n) = num n
weaken-val ext unit = unit
weaken-val ext null = null
weaken-val ext (ref x sub) = ref (∈-⊒ x ext) sub

instance
  val-weakenable : ∀ {a} → Weakenable (λ W → Val W a)
  val-weakenable = record { wk = weaken-val }


text:
module _ where

data D .(A : Set) : Set

-- The dot should not be repeated here
data D .A where
  mkD : D A


text:
{-# OPTIONS --warning=error #-}

module UselessPrivateImport where

private
  open import Common.Prelude


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

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

open import LibraBFT.ImplShared.Consensus.Types
open import Util.Encode
open import Util.PKCS                           as PKCS hiding (sign; verify)
open import Util.Prelude

module LibraBFT.Impl.OBM.Crypto where

------------------------------------------------------------------------------
-- keys

postulate -- TODO-1 : makePK
  makePK : SK → PK

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

postulate -- TODO-1: implement obmHashVersion
  obmHashVersion : Version → HashValue

------------------------------------------------------------------------------
-- sign and verify

record CryptoHash (A : Set) : Set where
  field
    sign        : SK → A → Signature
    verify      : {-Text-} PK → Signature → A → Either ErrLog Unit
    ⦃ encodeA ⦄ : Encoder A

open CryptoHash ⦃ ... ⦄ public

instance
  CryptoHashBlockData : CryptoHash BlockData
  CryptoHashBlockData = record
    { sign   = λ sk bd     → PKCS.sign-raw  (encode bd)     sk
    ; verify = λ pk sig bd → if PKCS.verify (encode bd) sig pk
                             then Right unit
                             else Left fakeErr }

instance
  CryptoHashLedgerInfo : CryptoHash LedgerInfo
  CryptoHashLedgerInfo = record
    { sign   = λ sk li     → PKCS.sign-raw  (encode li)     sk
    ; verify = λ pk sig li → if PKCS.verify (encode li) sig pk
                             then Right unit
                             else Left fakeErr }

instance
  CryptoHashTimeout : CryptoHash Timeout
  CryptoHashTimeout = record
    { sign   = λ sk to     → PKCS.sign-raw  (encode to)     sk
    ; verify = λ pk sig to → if PKCS.verify (encode to) sig pk
                             then Right unit
                             else Left fakeErr }


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.AbGroup.Properties where

open import Cubical.Foundations.Prelude

open import Cubical.Algebra.AbGroup.Base

private variable
  ℓ : Level

module AbGroupTheory (A'@(A , Ar) : AbGroup ℓ) where

  open AbGroupStr Ar

  comm-4 : (a b c d : A) → ((a + b) + (c + d) ≡ (a + c) + (b + d))
  comm-4 a b c d = ((a + b) + (c + d)  ≡⟨ +Assoc (a + b) c d ⟩
                   (((a + b) + c) + d) ≡⟨ cong (λ X → X + d) (sym (+Assoc a b c)) ⟩
                   ((a + (b + c)) + d) ≡⟨ cong (λ X → (a + X) + d) (+Comm b c) ⟩
                   ((a + (c + b)) + d) ≡⟨ cong (λ X → X + d) (+Assoc a c b) ⟩
                   (((a + c) + b) + d) ≡⟨ sym (+Assoc (a + c) b d) ⟩
                   ((a + c) + (b + d)) ∎)


text:
module BBHeap.Complete.Base {A : Set}(_≤_ : A → A → Set) where

open import BBHeap _≤_
open import BBHeap.Complete.Alternative _≤_ renaming (lemma-bbheap-complete to lemma-bbheap-complete')
open import BTree.Complete.Alternative.Correctness {A}
open import BTree.Complete.Base {A}
open import Bound.Lower A
open import Function using (_∘_)

lemma-bbheap-complete : {b : Bound}(h : BBHeap b) → Complete (forget h)
lemma-bbheap-complete = lemma-complete'-complete ∘ lemma-bbheap-complete'

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
------------------------------------------------------------------------------
-- Bisimulation on unbounded lists
------------------------------------------------------------------------------

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

-- In FOTC, we won't use the bisimulation functional on unbounded
-- lists. This module is only for illustrative purposes.

module FOTC.Relation.Binary.Bisimilarity.Bisimulation where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Relation.Binary.Bisimilarity.Type
open import FOTC.Relation.Binary.Bisimilarity.PropertiesI

----------------------------------------------------------------------------
-- The bisimilarity relation _≈_ on unbounded lists is the greatest
-- post-fixed point of Bisimulation (by post-fp and gpfp).

-- The bisimulation functional on unbounded lists (adapted from Dybjer
-- and Sander 1989, p. 310 and Jacobs and Rutten 1997, p. 30).
BisimulationF : (D → D → Set) → D → D → Set
BisimulationF B xs ys =
  ∃[ x' ] ∃[ xs' ] ∃[ ys' ] xs ≡ x' ∷ xs' ∧ ys ≡ x' ∷ ys' ∧ B xs' ys'

-- The bisimilarity relation _≈_ on unbounded lists is a post-fixed
-- point of Bisimulation, i.e.
--
-- _≈_ ≤ Bisimulation _≈_.
post-fp : ∀ {xs ys} → xs ≈ ys → BisimulationF _≈_ xs ys
post-fp = ≈-out

-- The bisimilarity relation _≈_ on unbounded lists is the greatest
-- post-fixed point of Bisimulation, i.e.
 --
-- ∀ B. B ≤ Bisimulation B ⇒ B ≤ _≈_.
greatest-post-fp :
  (B : D → D → Set) →
  -- B is a post-fixed point of Bisimulation.
  (∀ {xs} {ys} → B xs ys → BisimulationF B xs ys) →
  -- _≈_ is greater than B.
  ∀ {xs} {ys} → B xs ys → xs ≈ ys
greatest-post-fp = ≈-coind

-- Because a greatest post-fixed point is a fixed-point, the
-- bisimilarity relation _≈_ on unbounded lists is also a pre-fixed
-- point of Bisimulation, i.e.
--
-- Bisimulation _≈_ ≤ _≈_.
pre-fp : ∀ {xs} {ys} → BisimulationF _≈_ xs ys → xs ≈ ys
pre-fp = ≈-in

----------------------------------------------------------------------------
-- References
--
-- Dybjer, Peter and Sander, Herbert P. (1989). A Functional
-- Programming Approach to the Specification and Verification of
-- Concurrent Systems. Formal Aspects of Computing 1, pp. 303–319.
--
-- Jacobs, Bart and Rutten, Jan (1997). A Tutorial on (Co)Algebras and
-- (Co)Induction. EATCS Bulletin 62, pp. 222–259.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import Issue3188.Issue3188a

B : Set
B = Set


text:
module Oscar.Class.Functor where

open import Oscar.Class.Monoid
open import Oscar.Data.Equality
open import Oscar.Data.Product
open import Oscar.Level
open import Oscar.Relation
open import Oscar.Function

record Functor {a} {A : Set a} {b} (_↠_ : A → A → Set b) ⦃ _ : Monoid _↠_ ⦄ {c} (C : A → Set c) : Set (a ⊔ b ⊔ c) where
  field
    _◃_ : ∀ {m n} → m ↠ n → m ⟨ C ⟩→ n
    ◃-identity : ∀ {m} → (x : C m) → ε ◃ x ≡ x
    ◃-associativity : ∀ {l m n} (f : l ↠ m) (g : m ↠ n) → (g ◇ f) ◃_ ≡̇ g ◃_ ∘ f ◃_
    ◃-extensionality : ∀ {m n} {f g : m ↠ n} → f ≡ g → f ◃_ ≡ g ◃_

open Functor ⦃ … ⦄ public

open import Data.List
open import Oscar.Function

instance MonoidFunction : ∀ {a} → Monoid {A = Set a} (λ m n → m → n)
Monoid.ε MonoidFunction = λ x → x
Monoid._◇_ MonoidFunction g f = g ∘ f
Monoid.◇-left-identity MonoidFunction _ = refl
Monoid.◇-right-identity MonoidFunction _ = refl
Monoid.◇-associativity MonoidFunction _ _ _ = refl

instance FunctorList : ∀ {a} → Functor _ ⦃ MonoidFunction {a} ⦄ List
Functor._◃_ FunctorList {m} {n} f [] = []
Functor._◃_ FunctorList {m} {n} f (x ∷ xs) = f x ∷ f ◃ xs
Functor.◃-identity FunctorList = {!!}
Functor.◃-associativity FunctorList = {!!}
Functor.◃-extensionality FunctorList = {!!}


text:
-- There was a bug when scope checking with clauses.
module WithScopeError where

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

f : Nat -> Nat
f n with y
  where y = suc n
f n | x = y x


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

module Deltaplus where

{- Chapter 9.2: Semi-Simplicial Types

   This file contains the definition of the index category
   for semi-simplicial with judgmental categorical laws: Δ₊
   In other words, we check Proposition 9.2.1.

   We want to keep it independent of the other files,
   so we do not import anything. -}

{- For simplicity, we only use the lowest universe
   (totally sufficient) -}
Type = Set

-- the empty type
data Empty : Type where

-- the unit type
data ⊤ : Type where
  * : ⊤

-- the natural numbers
data ℕ : Type where
  O : ℕ
  S : (n : ℕ) → ℕ

{- Finite types: these are the

   ===  OBJECTS of Δ₊ ===

-}
data Fin : ℕ → Type where
  fz : {n : ℕ} → Fin (S n)
  fs : {n : ℕ} → Fin n → Fin (S n)

-- >-relation on finite types
_>fin_ : {n : ℕ} → (i j : Fin n) → Set
fz >fin i = Empty
fs j >fin fz = ⊤
fs j >fin fs i = j >fin i

{- the proposition [we do not need to prove propositionality here, but
   we could prove it easily] that a function is increasing;
   this is the tricky part: it needs to be done in a way which ensures
   that composition will behave nicely (strictly associative etc) later -}
is-increasing : {m n : ℕ} → (Fin m → Fin n) → Type
is-increasing {m} {n} f = {j i : Fin m} → (j >fin i) → ((f j) >fin (f i))

infixr 1 _,_

record Σ (A : Type) (B : A → Type) : Type where
  constructor _,_
  field
    fst : A
    snd : B fst

{- Strictly increasing maps: these are the

   === MORPHISMS of Δ₊ ===

-}
_⇒+_ : ℕ → ℕ → Set
m ⇒+ n = Σ (Fin m → Fin n) is-increasing

_∘+_ : {l m n : ℕ} → (m ⇒+ n) → (l ⇒+ m) → (l ⇒+ n)
(g , p₂) ∘+ (f , p₁) = (λ i → g(f(i))) , (λ p → p₂ (p₁ p))

-- === IDENTITY MORPHISMS of Δ₊ ===

idΔ₊ : ∀ {n} → n ⇒+ n
idΔ₊ = (λ x → x) , (λ p → p)

{- Now, let us check that the categorical laws hold judgmentally.
   To do this, we use the usual notion of equality. -}

infix 3 _==_

data _==_ {A : Type} (a : A) : A → Type where
  idp : a == a

-- === IDENTITY LAWS ===

id-comp : ∀ {m n} → (f : m ⇒+ n) → (idΔ₊ ∘+ f) == f
id-comp f = idp

comp-id : ∀ {m n} → (f : m ⇒+ n) → (f ∘+ idΔ₊) == f
comp-id f = idp

-- === ASSOCIATIVITY LAW ===

comp-assoc : ∀ {i j m n} → (f : i ⇒+ j) → (g : j ⇒+ m) → (h : m ⇒+ n)
             → h ∘+ (g ∘+ f) == (h ∘+ g) ∘+ f
comp-assoc f g h = idp

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
-----------------------------------------------------------------------
-- This file defines Dial₂(Sets) and its SMC structure.              --
-----------------------------------------------------------------------
module Dial2Sets where

open import prelude

-- The objects:
Obj : Set₁
Obj = Σ[ U ∈ Set ] (Σ[ X ∈ Set ] (U → X → Set))

-- The morphisms:
Hom : Obj → Obj → Set
Hom (U , X , α) (V , Y , β) =
  Σ[ f ∈ (U → V) ]
    (Σ[ F ∈ (Y → X) ] (∀{u : U}{y : Y} → α u (F y) → β (f u) y))

-- Composition:
comp : {A B C : Obj} → Hom A B → Hom B C → Hom A C
comp {(U , X , α)} {(V , Y , β)} {(W , Z , γ)} (f , F , p₁) (g , G , p₂) =
  (g ∘ f , F ∘ G , (λ {u z} p-α → p₂ (p₁ p-α)))

infixl 5 _○_

_○_ = comp

-- The contravariant hom-functor:
Homₐ :  {A' A B B' : Obj} → Hom A' A → Hom B B' → Hom A B → Hom A' B'
Homₐ f h g = comp f (comp g h)

-- The identity function:
id : {A : Obj} → Hom A A
id {(U , V , α)} = (id-set , id-set , id-set)

-- In this formalization we will only worry about proving that the
-- data of morphisms are equivalent, and not worry about the morphism
-- conditions.  This will make proofs shorter and faster.
--
-- If we have parallel morphisms (f,F) and (g,G) in which we know that
-- f = g and F = G, then the condition for (f,F) will imply the
-- condition of (g,G) and vice versa.  Thus, we can safly ignore it.
infix 4 _≡h_

_≡h_ : {A B : Obj} → (f g : Hom A B) → Set
_≡h_ {(U , X , α)}{(V , Y , β)} (f , F , p₁) (g , G , p₂) = f ≡ g × F ≡ G

≡h-refl : {A B : Obj}{f : Hom A B} → f ≡h f
≡h-refl {U , X , α}{V , Y , β}{f , F , _} = refl , refl

≡h-trans : ∀{A B}{f g h : Hom A B} → f ≡h g → g ≡h h → f ≡h h
≡h-trans {U , X , α}{V , Y , β}{f , F , _}{g , G , _}{h , H , _} (p₁ , p₂) (p₃ , p₄) rewrite p₁ | p₂ | p₃ | p₄ = refl , refl

≡h-sym : ∀{A B}{f g : Hom A B} → f ≡h g → g ≡h f
≡h-sym {U , X , α}{V , Y , β}{f , F , _}{g , G , _} (p₁ , p₂) rewrite p₁ | p₂ = refl , refl

≡h-subst-○ : ∀{A B C}{f₁ f₂ : Hom A B}{g₁ g₂ : Hom B C}{j : Hom A C}
  → f₁ ≡h f₂
  → g₁ ≡h g₂
  → f₂ ○ g₂ ≡h j
  → f₁ ○ g₁ ≡h j
≡h-subst-○ {U , X , α}
         {V , Y , β}
         {W , Z , γ}
         {f₁ , F₁ , _}
         {f₂ , F₂ , _}
         {g₁ , G₁ , _}
         {g₂ , G₂ , _}
         {j , J , _}
         (p₅ , p₆) (p₇ , p₈) (p₉ , p₁₀) rewrite p₅ | p₆ | p₇ | p₈ | p₉ | p₁₀ = refl , refl

○-assoc : ∀{A B C D}{f : Hom A B}{g : Hom B C}{h : Hom C D}
  → f ○ (g ○ h) ≡h (f ○ g) ○ h
○-assoc {U , X , α}{V , Y , β}{W , Z , γ}{S , T , ι}
        {f , F , _}{g , G , _}{h , H , _} = refl , refl

○-idl : ∀{A B}{f : Hom A B} → id ○ f ≡h f
○-idl {U , X , _}{V , Y , _}{f , F , _} = refl , refl

○-idr : ∀{A B}{f : Hom A B} → f ○ id ≡h f
○-idr {U , X , _}{V , Y , _}{f , F , _} = refl , refl

-----------------------------------------------------------------------
-- Dial₂(Sets) is a SMC                                              --
-----------------------------------------------------------------------

-- The tensor functor: ⊗
_⊗ᵣ_ : ∀{U X V Y : Set} → (U → X → Set) → (V → Y → Set) → ((U × V) → ((V → X) × (U → Y)) → Set)
_⊗ᵣ_ α β (u , v) (f , g) = (α u (f v)) × (β v (g u))

_⊗ₒ_ : (A B : Obj) → Obj
(U , X , α) ⊗ₒ (V , Y , β) = ((U × V) , ((V → X) × (U → Y)) , α ⊗ᵣ β)

F⊗ : ∀{S Z W T V X U Y : Set}{f : U → W}{F : Z → X}{g : V → S}{G : T → Y} → (S → Z) × (W → T) → (V → X) × (U → Y)
F⊗ {f = f}{F}{g}{G} (h₁ , h₂) = (λ v → F(h₁ (g v))) , (λ u → G(h₂ (f u)))

_⊗ₐ_ : {A B C D : Obj} → Hom A C → Hom B D → Hom (A ⊗ₒ B) (C ⊗ₒ D)
_⊗ₐ_ {(U , X , α)}{(V , Y , β)}{(W , Z , γ)}{(S , T , δ)} (f , F , p₁) (g , G , p₂) = ⟨ f , g ⟩ , F⊗ {f = f}{F}{g}{G} , p
 where
  p : {u : U × V} {y : (S → Z) × (W → T)} → (α ⊗ᵣ β) u ((F⊗ {f = f}{F}{g}{G}) y) → (γ ⊗ᵣ δ) (⟨ f , g ⟩ u) y
  p {(u , v)} {(h₁ , h₂)} (p-α , p-β) = p₁ p-α , p₂ p-β

-- The unit for tensor:
ι : ⊤ {lzero} → ⊤ {lzero} → Set
ι triv triv = ⊤

I : Obj
I = (⊤ , ⊤ , ι)

J : Obj
J = (⊤ , ⊤ , (λ x y → ⊥))

-- The left-unitor:
λ⊗-p : ∀{U X α}{u : ⊤ × U} {x : X} → (ι ⊗ᵣ α) u ((λ _ → triv) , (λ _ → x)) → α (snd u) x
λ⊗-p {U}{X}{α}{(triv , u)}{x} (triv , p-α) = p-α

λ⊗ : ∀{A : Obj} → Hom (I ⊗ₒ A) A
λ⊗ {(U , X , α)} = snd , (λ x → (λ _ → triv) , (λ _ → x)) , λ⊗-p

λ⁻¹⊗ : ∀{A : Obj} → Hom A (I ⊗ₒ A)
λ⁻¹⊗ {(U , X , α)} = (λ u → triv , u) , ((λ x → snd x triv) , λ⁻¹⊗-p)
 where
  λ⁻¹⊗-p : ∀{U X α} → {u : U} {y : (U → ⊤) × (⊤ → X)} → α u (snd y triv) → (ι ⊗ᵣ α) (triv , u) y
  λ⁻¹⊗-p {U}{X}{α}{u}{(h₁ , h₂)} p-α with h₁ u
  ... | triv = triv , p-α

-- The right-unitor:
ρ⊗ : ∀{A : Obj} → Hom (A ⊗ₒ I) A
ρ⊗ {(U , X , α)} = fst , (λ x → (λ x₁ → x) , (λ x₁ → triv)) , ρ⊗-p
 where
  ρ⊗-p : ∀{U X α}{u : U × ⊤}{x : X} → (α ⊗ᵣ ι) u ((λ _ → x) , (λ _ → triv)) → α (fst u) x
  ρ⊗-p {U}{X}{α}{(u , triv)}{x} (p-α , triv) = p-α

ρ⊗-inv : ∀{A : Obj} → Hom A (A ⊗ₒ I)
ρ⊗-inv {(U , X , α)} = (λ x → x , triv) , (λ x → fst x triv) , ρ⊗-p-inv
 where
  ρ⊗-p-inv : ∀{U X α}{u : U} {y : Σ (⊤ → X) (λ x → U → ⊤)} → α u (fst y triv) → (α ⊗ᵣ ι) (u , triv) y
  ρ⊗-p-inv {U}{X}{α}{u}{(f , g)} p-α rewrite single-range {g = g}{u} = p-α , triv

-- Symmetry:
β⊗ : ∀{A B : Obj} → Hom (A ⊗ₒ B) (B ⊗ₒ A)
β⊗ {(U , X , α)}{(V , Y , β)} = twist-× , twist-× , β⊗-p
 where
   β⊗-p : ∀{U V Y X α β} → {u : U × V} {y : (U → Y) × (V → X)} →
       (α ⊗ᵣ β) u (twist-× y) → (β ⊗ᵣ α) (twist-× u) y
   β⊗-p {U}{V}{Y}{X}{α}{β}{(u , v)}{(h₁ , h₂)} p-α = twist-× p-α

-- The associator:
α⊗-inv : ∀{A B C : Obj} → Hom (A ⊗ₒ (B ⊗ₒ C)) ((A ⊗ₒ B) ⊗ₒ C)
α⊗-inv {(U , X , α)}{(V , Y , β)}{(W , Z , γ)} = rl-assoc-× , Fα-inv , α-inv-cond
 where
   Fα-inv : (W → (V → X) × (U → Y)) × (U × V → Z) → (V × W → X) × (U → (W → Y) × (V → Z))
   Fα-inv = (λ p → (λ p' → fst ((fst p) (snd p')) (fst p')) , (λ u → (λ w → snd (fst p w) u) , (λ v → (snd p) (u , v))))
   α-inv-cond : ∀{u : U × V × W} {y : (W → (V → X) × (U → Y)) × (U × V → Z)} → (α ⊗ᵣ (β ⊗ᵣ γ)) u (Fα-inv y) → ((α ⊗ᵣ β) ⊗ᵣ γ) (rl-assoc-× u) y
   α-inv-cond {(u , v , w)} {(h₁ , h₂)} (p₁ , p₂ , p₃) with h₁ w
   ... | (a , b) = (p₁ , p₂) , p₃

Fα : ∀{V W X Y U V Z : Set} → Σ (Σ V (λ x → W) → X) (λ x → U → Σ (W → Y) (λ x₁ → V → Z))
       → Σ (W → Σ (V → X) (λ x → U → Y)) (λ x → Σ U (λ x₁ → V) → Z)
Fα (f ,  g) = (λ x → (λ x₁ → f ((x₁ , x))) , (λ x₁ → fst (g x₁) x)) , (λ x → snd (g (fst x)) (snd x))

α⊗ : ∀{A B C : Obj} → Hom ((A ⊗ₒ B) ⊗ₒ C) (A ⊗ₒ (B ⊗ₒ C))
α⊗ {(U , X , α)}{(V , Y , β)}{(W , Z , γ)} = (lr-assoc-× , Fα {V} , α-cond)
 where
  α-cond : {u : Σ (Σ U (λ x → V)) (λ x → W)}{y : Σ (Σ V (λ x → W) → X) (λ x → U → Σ (W → Y) (λ x₁ → V → Z))} →
      ((α ⊗ᵣ β) ⊗ᵣ γ) u (Fα {V} y) → (α ⊗ᵣ (β ⊗ᵣ γ)) (lr-assoc-× u) y
  α-cond {(u , v) , w}{(f , g)} ((p₁ , p₂) , p₃) with g u
  ... | (h₁ , h₂) = p₁ , p₂ , p₃

α⊗-id₁ : ∀{A B C} → (α⊗ {A}{B}{C}) ○ α⊗-inv ≡h id
α⊗-id₁ {U , X , α}{V , Y , β}{W , Z , γ} = ext-set aux , ext-set aux'
 where
   aux : {a : Σ (Σ U (λ x → V)) (λ x → W)} → rl-assoc-× (lr-assoc-× a) ≡ a
   aux {(u , v) , w} = refl

   aux' : {a : Σ (W → Σ (V → X) (λ x → U → Y)) (λ x → Σ U (λ x₁ → V) → Z)}
     → ((λ x → (λ x₁ → fst (fst a x) x₁) , (λ x₁ → snd (fst a x) x₁)) , (λ x → snd a (fst x , snd x))) ≡ a
   aux' {j₁ , j₂} = eq-× (ext-set aux'') (ext-set aux''')
    where
      aux'' : {a : W} → (fst (j₁ a) , snd (j₁ a)) ≡ j₁ a
      aux'' {w} with j₁ w
      ... | h₁ , h₂ = refl

      aux''' : {a : Σ U (λ x₁ → V)} → j₂ (fst a , snd a) ≡ j₂ a
      aux''' {u , v} = refl

α⊗-id₂ : ∀{A B C} → (α⊗-inv {A}{B}{C}) ○ α⊗ ≡h id
α⊗-id₂ {U , X , α}{V , Y , β}{W , Z , γ} = ext-set aux , ext-set aux'
 where
   aux : {a : Σ U (λ x → Σ V (λ x₁ → W))} → lr-assoc-× (rl-assoc-× a) ≡ a
   aux {u , (v , w)} = refl
   aux' : {a
       : Σ (Σ V (λ x → W) → X) (λ x → U → Σ (W → Y) (λ x₁ → V → Z))} →
      ((λ p' → fst (fst (Fα {V} {W} {X} {Y} {U} {V} {Z} a) (snd p')) (fst p')) ,
       (λ u → (λ w → snd (fst (Fα {V} {W} {X} {Y} {U} {V} {Z} a) w) u) , (λ v → snd (Fα {V} {W} {X} {Y} {U} {V} {Z} a) (u , v))))
      ≡ a
   aux' {j₁ , j₂} = eq-× (ext-set aux'') (ext-set aux''')
     where
       aux'' : {a : Σ V (λ x → W)} → j₁ (fst a , snd a) ≡ j₁ a
       aux'' {v , w} = refl
       aux''' : {a : U} → ((λ w → fst (j₂ a) w) , (λ v → snd (j₂ a) v)) ≡ j₂ a
       aux''' {u} with j₂ u
       ... | h₁ , h₂ = refl

-- Internal hom:
⊸-cond : ∀{U V X Y : Set} → (U → X → Set) → (V → Y → Set) → (U → V) × (Y → X) → U × Y → Set
⊸-cond α β (f , g) (u , y) = α u (g y) → β (f u) y

_⊸ₒ_ : Obj → Obj → Obj
(U , X , α) ⊸ₒ (V , Y , β) = ((U → V) × (Y → X)) , (U × Y) , ⊸-cond α β

_⊸ₐ_ : {A B C D : Obj} → Hom C A → Hom B D → Hom (A ⊸ₒ B) (C ⊸ₒ D)
_⊸ₐ_ {(U , X , α)}{(V , Y , β)}{(W , Z , γ)}{(S , T , δ)} (f , F , p₁) (g , G , p₂) =
  h , H , p₃
  where
   h : Σ (U → V) (λ x → Y → X) → Σ (W → S) (λ x → T → Z)
   h (h₁ , h₂) = (λ w → g (h₁ (f w))) , (λ t → F (h₂ (G t)))
   H : Σ W (λ x → T) → Σ U (λ x → Y)
   H (w , t) = f w , G t
   p₃ : {u : Σ (U → V) (λ x → Y → X)} {y : Σ W (λ x → T)} → ⊸-cond α β u (H y) → ⊸-cond γ δ (h u) y
   p₃ {h₁ , h₂}{w , t} c c' = p₂ (c (p₁ c'))

cur : {A B C : Obj}
  → Hom (A ⊗ₒ B) C
  → Hom A (B ⊸ₒ C)
cur {U , X , α}{V , Y , β}{W , Z , γ} (f , F , p₁)
  = (λ u → (λ v → f (u , v)) , (λ z → snd (F z) u)) , (λ p →  fst (F (snd p)) (fst p)) , cur-cond
 where
   cur-cond : ∀{u : U}{y : Σ V (λ x → Z)}
     → α u (fst (F (snd y)) (fst y))
     → ⊸-cond β γ ((λ v → f (u , v)) , (λ z → snd (F z) u)) y
   cur-cond {u}{v , z} p₂ p₃ with p₁ {u , v}{z}
   ... | p₁' with F z
   ... | (j₁ , j₂) = p₁' (p₂ , p₃)

cur-≡h : ∀{A B C}{f₁ f₂ : Hom (A ⊗ₒ B) C}
  → f₁ ≡h f₂
  → cur f₁ ≡h cur f₂
cur-≡h {U , X , α}{V , Y , β}{W , Z , γ}
       {f₁ , F₁ , p₁}{f₂ , F₂ , p₂} (p₃ , p₄)
       rewrite p₃ | p₄ = refl , refl

cur-cong : ∀{A B C}{f₁ f₂ : Hom (A ⊗ₒ B) C} → f₁ ≡h f₂ → cur f₁ ≡h cur f₂
cur-cong {(U , X , α)} {(V , Y , β)} {(W , Z , γ)}{f₁ , F₁ , _}{f₂ , F₂ , _} (p₁ , p₂) rewrite p₁ | p₂ = refl , refl

uncur : {A B C : Obj}
  → Hom A (B ⊸ₒ C)
  → Hom (A ⊗ₒ B) C
uncur {U , X , α}{V , Y , β}{W , Z , γ} (f , F , p₁)
  = (λ p → fst (f (fst p)) (snd p)) , (λ z → (λ v → F (v , z)) , (λ u → snd (f u) z)) , uncur-cond
  where
    uncur-cond : ∀{u : Σ U (λ x → V)} {y : Z}
      → (α ⊗ᵣ β) u ((λ v → F (v , y)) , (λ u₁ → snd (f u₁) y))
      → γ (fst (f (fst u)) (snd u)) y
    uncur-cond {u , v}{z} (p₂ , p₃) with p₁ {u}{v , z} p₂
    ... | p₁' with f u
    ... | (j₁ , j₂) = p₁' p₃

cur-uncur-bij₁ : ∀{A B C}{f : Hom (A ⊗ₒ B) C}
  → uncur (cur f) ≡h f
cur-uncur-bij₁ {U , X , α}{V , Y , β}{W , Z , γ}{f , F , p₁} = ext-set aux₁ , ext-set aux₂
 where
   aux₁ : {a : Σ U (λ x → V)} → f (fst a , snd a) ≡ f a
   aux₁ {u , v} = refl

   aux₂ : {a : Z} → ((λ v → fst (F a) v) , (λ u → snd (F a) u)) ≡ F a
   aux₂ {z} with F z
   ... | j₁ , j₂ = refl

cur-uncur-bij₂ : ∀{A B C}{g : Hom A (B ⊸ₒ C)}
  → cur (uncur g) ≡h g
cur-uncur-bij₂ {U , X , α}{V , Y , β}{W , Z , γ}{g , G , p₁} = ext-set aux₁ , ext-set aux₂
 where
   aux₁ : {a : U} → ((λ v → fst (g a) v) , (λ z → snd (g a) z)) ≡ g a
   aux₁ {u} with g u
   ... | (j₁ , j₂) = refl

   aux₂ : {a : Σ V (λ x → Z)} → G (fst a , snd a) ≡ G a
   aux₂ {v , z} = refl

-- The of-course exponential:
!ₒ-cond : ∀{U X : Set}
  → (U → X → Set)
  → U
  → (U → X *)
  → Set
!ₒ-cond α u f = all-pred (α u) (f u)

!ₒ : Obj → Obj
!ₒ (U , X , α) = U , (U → X *) , !ₒ-cond α

!-cta : {V Y U X : Set}
  → (Y → X)
  → (U → V)
  → (V → Y *)
  → (U → X *)
!-cta F f g = λ u → list-funct F (g (f u))

!ₐ-cond : ∀{U V Y X : Set}{F : Y → X}{f : U → V}
  → (α : U → X → Set)
  → (β : V → Y → Set)
  → (p : {u : U} {y : Y} → α u (F y) → β (f u) y)
    {u : U}{l : Y *}
  → all-pred (α u) (list-funct F l)
  → all-pred (β (f u)) l
!ₐ-cond _ _ _ {l = []} _ = triv
!ₐ-cond α β p {u}{x :: xs} (p' , p'') = p p' , !ₐ-cond α β p p''

!ₐ : {A B : Obj} → Hom A B → Hom (!ₒ A) (!ₒ B)
!ₐ {U , X , α}{V , Y , β} (f , F , p) = f , !-cta F f , !ₐ-cond α β p

-- Of-course is a comonad:
ε : ∀{A} → Hom (!ₒ A) A
ε {U , X , α} = id-set , (λ x y → [ x ]) , fst

δ-cta : {U X : Set} → (U → 𝕃 (U → 𝕃 X)) → U → 𝕃 X
δ-cta g u = foldr (λ f rest → (f u) ++ rest) [] (g u)

δ : ∀{A} → Hom (!ₒ A) (!ₒ (!ₒ A))
δ {U , X , α} = id-set , δ-cta , δ-cond
  where
   δ-cond : {u : U} {l : 𝕃 (U → 𝕃 X)}
     → all-pred (α u) (foldr (λ f → _++_ (f u)) [] l)
     → all-pred (λ f
     → all-pred (α u) (f u)) l
   δ-cond {l = []} _ = triv
   δ-cond {u}{l = x :: l'} p with
     all-pred-append {X}{α u}
                     {x u}
                     {foldr (λ f → _++_ (f u)) [] l'}
                     ∧-unit ∧-assoc
   ... | p' rewrite p' = fst p , δ-cond {u} {l'} (snd p)

-- These diagrams can be found on page 22 of the report.
{-
comonand-diag₁ : ∀{A}
  → (δ {A}) ○ (!ₐ (δ {A})) ≡h (δ {A}) ○ (δ { !ₒ A})
comonand-diag₁ {U , X , α} =
  refl , ext-set (λ {a} → ext-set (λ {a₁} → aux {a₁}{a a₁}))
 where
   aux : ∀{a₁ : U}{l : 𝕃 (U → 𝕃 (U → 𝕃 X))} →
      foldr (λ f → _++_ (f a₁)) []
      (map (λ g u → foldr (λ f → _++_ (f u)) [] (g u)) l)
      ≡
      foldr (λ f → _++_ (f a₁)) [] (foldr (λ f → _++_ (f a₁)) [] l)
   aux {a}{[]} = refl
   aux {a}{x :: l} rewrite
     sym (foldr-append {l₁ = x a}{foldr (λ f → _++_ (f a)) [] l}{a})
     = cong2 {a = foldr (λ f → _++_ (f a)) [] (x a)}
             _++_
             refl
             (aux {a}{l})

comonand-diag₂ : ∀{A}
  → (δ {A}) ○ (ε { !ₒ A}) ≡h (δ {A}) ○ (!ₐ (ε {A}))
comonand-diag₂ {U , X , α} =
  refl , ext-set (λ {f} → ext-set (λ {a} → aux {a}{f a}))
 where
  aux : ∀{a : U}{l : X *}
    → l ++ [] ≡ foldr (λ f₁ → _++_ (f₁ a)) [] (map (λ x y → x :: []) l)
  aux {a}{[]} = refl
  aux {a}{x :: l} with aux {a}{l}
  ... | IH rewrite ++[] l =
    cong2 {a = x} {x} {l}
          {foldr (λ f₁ → _++_ (f₁ a)) [] (map (λ x₁ y → x₁ :: []) l)} _::_ refl
          IH
-}
module Cartesian where
  π₁ : {U X V Y : Set}
    → {α : U → X → Set}
    → {β : V → Y → Set}
    → Hom ((!ₒ (U , X , α)) ⊗ₒ (!ₒ (V , Y , β))) (!ₒ (U , X , α))
  π₁ {U}{X}{V}{Y}{α}{β} = fst , (λ f → (λ v u → f u) , (λ u v → [])) , π₁-cond
    where
      π₁-cond : ∀{u : Σ U (λ x → V)} {y : U → 𝕃 X} →
        ((λ u₁ f → all-pred (α u₁) (f u₁)) ⊗ᵣ
        (λ u₁ f → all-pred (β u₁) (f u₁)))
        u ((λ v u₁ → y u₁) , (λ u₁ v → [])) →
        all-pred (α (fst u)) (y (fst u))
      π₁-cond {u , v}{f} (p₁ , p₂) = p₁

  π₂ : {U X V Y : Set}
      → {α : U → X → Set}
      → {β : V → Y → Set}
      → Hom ((!ₒ (U , X , α)) ⊗ₒ (!ₒ (V , Y , β))) (!ₒ (V , Y , β))
  π₂ {U}{X}{V}{Y}{α}{β} = snd , (λ f → (λ v u → []) , (λ u v → f v)) , π₂-cond
      where
        π₂-cond : ∀{u : Σ U (λ x → V)} {y : V → 𝕃 Y} →
          ((λ u₁ f → all-pred (α u₁) (f u₁)) ⊗ᵣ
            (λ u₁ f → all-pred (β u₁) (f u₁)))
              u ((λ v u₁ → []) , (λ u₁ v → y v)) →
            all-pred (β (snd u)) (y (snd u))
        π₂-cond {u , v}{f} (p₁ , p₂) = p₂

  cart-ar-crt : {U X V Y W Z : Set}
    → {α : U → X → Set}
    → {β : V → Y → Set}
    → {γ : W → Z → Set}
    → Hom (!ₒ (W , Z , γ)) (!ₒ (U , X , α))
    → Hom (!ₒ (W , Z , γ)) (!ₒ (V , Y , β))
    → Σ (V → U → 𝕃 X) (λ x → U → V → 𝕃 Y) → W → 𝕃 Z
  cart-ar-crt  (f , F , p₁) (g , G , p₂) (j₁ , j₂) w = F (j₁ (g w)) w ++ G (j₂ (f w)) w

  cart-ar : {U X V Y W Z : Set}
    → {α : U → X → Set}
    → {β : V → Y → Set}
    → {γ : W → Z → Set}
    → Hom (!ₒ (W , Z , γ)) (!ₒ (U , X , α))
    → Hom (!ₒ (W , Z , γ)) (!ₒ (V , Y , β))
    → Hom (!ₒ (W , Z , γ)) ((!ₒ (U , X , α)) ⊗ₒ (!ₒ (V , Y , β)))
  cart-ar {U}{X}{V}{Y}{W}{Z}{α}{β}{γ} (f , F , p₁) (g , G , p₂)
    = (λ w → f w , g w) , cart-ar-crt {α = α}{β} (f , F , p₁) (g , G , p₂) , cart-ar-cond
      where
        cart-ar-cond : ∀{u : W} {y : Σ (V → U → 𝕃 X) (λ x → U → V → 𝕃 Y)} →
          all-pred (γ u) (cart-ar-crt {α = α}{β} (f , F , p₁) (g , G , p₂) y u) →
          ((λ u₁ f₁ → all-pred (α u₁) (f₁ u₁)) ⊗ᵣ
          (λ u₁ f₁ → all-pred (β u₁) (f₁ u₁)))
          (f u , g u) y
        cart-ar-cond {w}{j₁ , j₂} p
          rewrite
            all-pred-append {f = γ w}{F (j₁ (g w)) w}{G (j₂ (f w)) w} ∧-unit ∧-assoc with p
        ... | (a , b) = p₁ a , p₂ b

  cart-diag₁ : {U X V Y W Z : Set}
    → {α : U → X → Set}
    → {β : V → Y → Set}
    → {γ : W → Z → Set}
    → {f : Hom (W , Z , γ) (U , X , α)}
    → {g : Hom (W , Z , γ) (V , Y , β)}
    → _≡h_ { !ₒ (W , Z , γ)}{ !ₒ (U , X , α)}
      (!ₐ {W , Z , γ}{U , X , α} f)
      (comp { !ₒ (W , Z , γ)}
            {((!ₒ (U , X , α)) ⊗ₒ (!ₒ (V , Y , β)))}
            { !ₒ (U , X , α)}
            (cart-ar {α = α}{β}{γ} (!ₐ {W , Z , γ}{U , X , α} f) (!ₐ {W , Z , γ}{V , Y , β} g))
            π₁)
  cart-diag₁ {f = f , F , p₁}{g , G , p₂}
    = refl , ext-set (λ {j} → ext-set (λ {w} → sym (++[] (map F (j (f w))))))

  cart-diag₂ : {U X V Y W Z : Set}
    → {α : U → X → Set}
    → {β : V → Y → Set}
    → {γ : W → Z → Set}
    → {f : Hom (W , Z , γ) (U , X , α)}
    → {g : Hom (W , Z , γ) (V , Y , β)}
    → _≡h_ { !ₒ (W , Z , γ)}{ !ₒ (V , Y , β)}
      (!ₐ {W , Z , γ}{V , Y , β} g)
      (comp { !ₒ (W , Z , γ)}
            {((!ₒ (U , X , α)) ⊗ₒ (!ₒ (V , Y , β)))}
            { !ₒ (V , Y , β)}
            (cart-ar {α = α}{β}{γ} (!ₐ {W , Z , γ}{U , X , α} f) (!ₐ {W , Z , γ}{V , Y , β} g))
            π₂)
  cart-diag₂ {f = f , F , p₁}{g , G , p₂}
    = refl , ext-set (λ {j} → ext-set (λ {w} → refl))

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
-- Common imports and other auxiliary operations used in the library
module SOAS.Common where

open import Categories.Category.Instance.Sets public
open import Axiom.Extensionality.Propositional
  using (Extensionality; ExtensionalityImplicit)
open import Relation.Binary.PropositionalEquality public
  hiding (Extensionality)
  renaming (subst to ≡subst; [_] to ≡[_])

open import Categories.Category public
open import Categories.Category.Helper public
open import Categories.Functor public
  renaming (id to idF)

open import Categories.NaturalTransformation public
  using (ntHelper)
  renaming (NaturalTransformation to NT; id to idN; _∘ᵥ_ to _∘N_)
open import Categories.NaturalTransformation.Equivalence using (_≃_) public
open import Categories.Morphism using (Iso) public

open import Level as L hiding (lift) renaming (suc to lsuc) public
open import Function using (flip; case_of_; _∋_) public renaming (_$_ to _$ᶠ_)
open import Data.Product public using (_×_; proj₁; proj₂; _,_; Σ; module Σ; Σ-syntax; swap)
open import Data.Sum public using (_⊎_ ; inj₁; inj₂)
open import Data.Unit public using (tt)

-- Unit type
data *T : Set where
  * : *T

-- Shorthand for first universe level
1ℓ : Level
1ℓ = lsuc 0ℓ

-- Basic function extensionality postulates
postulate
  -- Extensionality with one explicit or implicit argument
  ext  : Extensionality 0ℓ 0ℓ
  iext : ExtensionalityImplicit 0ℓ 0ℓ

-- Functions with two explicit arguments
ext² : {A : Set} {B : A → Set}{C : (x : A) → B x → Set}
       {f g : (x : A) → (y : B x) → C x y} →
       (∀ x y → f x y ≡ g x y) →
       (λ x y → f x y) ≡ (λ x y → g x y)
ext² p = ext (λ x → ext (λ y → p x y))

-- Functions with one implicit and one explicit argument
dext : {A : Set} {B : A → Set}{C : (x : A) → B x → Set}
       {f g : {x : A} → (y : B x) → C x y} →
       (∀ {x} y → f {x} y ≡ g {x} y) →
       (λ {x} y → f {x} y) ≡ (λ {x} y → g {x} y)
dext p = iext (ext p)

-- Functions with two pairs of implicit-explicit arguments
dext² : {A : Set}{B : A → Set}{C : A → A → Set}
       {D : (x : A) → B x → (y : A) → C x y → Set}
       {f g : {x : A} → (b : B x) → {y : A} → (c : C x y) → D x b y c} →
       (∀ {x} b {y} c → f {x} b {y} c ≡ g {x} b {y} c) →
       (λ {x} b {y} c → f {x} b {y} c) ≡
       (λ {x} b {y} c → g {x} b {y} c)
dext² p = dext (λ {x} y → dext (p {x} y))

-- Functions with one implicit and one explicit argument where the
-- pointwise equality proof does not use the explicit argument
dext′ : {A : Set} {B : A → Set}{C : (x : A) → B x → Set}
       {f g : {x : A} → (y : B x) → C x y} →
       (∀ {x} {y} → f {x} y ≡ g {x} y) →
       (λ {x} y → f {x} y) ≡ (λ {x} y → g {x} y)
dext′ p = dext (λ {x} y → p {x}{y})

-- Use the naming convention for categories
𝕊ets : Category 1ℓ 0ℓ 0ℓ
𝕊ets = Sets 0ℓ
module 𝕊et = Category 𝕊ets

-- Make composition and the identity globally accessible
open Category (Sets 0ℓ) public using (_∘_; id)

-- Set isomorphism shorthands
open import Categories.Morphism 𝕊ets public using ()
        renaming ( _≅_ to _≅ₛ_ ; module ≅ to ≅ₛ ; ≅-setoid to ≅ₛ-setoid)

-- Congruence with the arguments reversed -- easier to focus on the equalities
-- if the congruence environment is very large
congr : ∀{ℓ}{A B : Set ℓ}{x y : A} → x ≡ y → (f : A → B) → f x ≡ f y
congr refl f = refl

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
{-
Joseph Eremondi
Utrecht University Capita Selecta
UU# 4229924
July 22, 2015
-}

module SemiLin where

open import Data.Vec
open import Data.Nat
import Data.Fin as Fin

open import Data.List
import Data.List.All
open import Data.Bool
open import Data.Char

open import Data.Maybe

open import Data.Product
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Binary.Core

open import Category.Monad

open import Data.Nat.Properties.Simple

open import Data.Maybe
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import Utils

open import Function

import RETypes

open import Data.Sum

import Data.Nat.Properties.Simple

--The Parikh vector for a word is the count of occurrences of
--each letter of our alphabet in that word.
--We just represent this as a vector of Natural numbers
Parikh : ℕ -> Set
Parikh n = Vec ℕ n

--Scalar multiplication
_·ₛ_ : {n : ℕ} -> ℕ -> Parikh n -> Parikh n
c ·ₛ [] = []
c ·ₛ (x ∷ vt) = (c * x) ∷ (c ·ₛ vt)

--Vector addition
_+v_ : {n : ℕ} -> Parikh n -> Parikh n -> Parikh n
[] +v [] = []
(x ∷ ut) +v (y ∷ vt) = x + y ∷ ut +v vt

--The zero vector
v0 : {n : ℕ} -> Parikh n
v0 {zero} = []
v0 {suc n} = 0 ∷ v0

--0 times anything is v0
scalar0ident : {n : ℕ} -> (v : Parikh n ) -> 0 ·ₛ v ≡ v0
scalar0ident [] = refl
scalar0ident (x ∷ v) = cong (_∷_ zero) (scalar0ident v)

--Prove that 0 is a neutral element on the left
v0identLeft : {n : ℕ} -> {v : Parikh n} -> v0 +v v ≡ v
v0identLeft {v = []} = refl
v0identLeft {v = x ∷ v} =
  let
    subIdent = v0identLeft {v = v}
  in cong (λ t → x ∷ t) subIdent

--Prove that vector addition is commutative
v+-commut : {n : ℕ} -> (u : Parikh n) -> (v : Parikh n) -> (u +v v ≡ v +v u)
v+-commut [] [] = refl
v+-commut (x ∷ u) (y ∷ v) rewrite +-comm x y  | v+-commut u v = refl

--Prove the right-identity for vector addition with 0
--Just conbines commutativity and the left identity
v0identRight : {n : ℕ} -> {v : Parikh n} -> v +v v0 ≡ v
v0identRight {v = v} =
  begin
    v +v v0
  ≡⟨ v+-commut v v0 ⟩
    v0 +v v
  ≡⟨ v0identLeft ⟩
    v ∎

--Prove that vector addition is associative
--I couldn't figure out how to get this one working with rewrite
vAssoc : {n : ℕ} -> {x : Parikh n} {y : Parikh n} {z : Parikh n}
  -> (x +v y) +v z ≡ x +v (y +v z)
vAssoc {zero} {[]} {[]} {[]} = refl
vAssoc {suc n} {xh ∷ xt} {yh ∷ yt} {zh ∷ zt} =
  let
    x = xh ∷ xt
    y = yh ∷ yt
    z = zh ∷ zt
  in --_≡⟨_⟩_
      begin
        (x +v y) +v z
      ≡⟨ refl ⟩
        (xh + yh + zh) ∷ (xt +v yt) +v zt
      ≡⟨ cong (λ h → h ∷ (xt +v yt) +v zt) (+-assoc xh yh zh) ⟩
        xh + (yh + zh) ∷ (xt +v yt) +v zt
      ≡⟨ cong (λ t → xh + (yh + zh) ∷ t) vAssoc ⟩
        (xh + (yh + zh) ∷ xt +v (yt +v zt))
      ≡⟨ refl ⟩
        x +v (y +v z)
      ∎

-- Wouter: here's one definition using rewrite...
vAssoc2 : {n : ℕ} -> {x : Parikh n} {y : Parikh n} {z : Parikh n}
  -> (x +v y) +v z ≡ x +v (y +v z)
vAssoc2 {x = []} {[]} {[]} = refl
vAssoc2 {x = x ∷ xs} {y ∷ ys} {z ∷ zs} rewrite +-assoc x y z | vAssoc {x = xs} {y = ys} {z = zs}
  = refl

--Prove that scalar multiplication distributes over vector addition
scalarAssoc : {n : ℕ} -> (x y : ℕ ) -> (v : Parikh n) -> (x + y) ·ₛ v ≡  (x ·ₛ v) +v (y ·ₛ v)
scalarAssoc x y [] = refl
scalarAssoc x y (vfirst ∷ v) rewrite scalarAssoc x y v | distribʳ-*-+ vfirst x y = refl

--Handy lemma, prove that 0 + anything is 0
ident0 : (x : ℕ) -> x + 0 ≡ x
ident0 zero = refl
ident0 (suc x) = cong suc (ident0 x)

--Show that 1 is an identity for scalar multiplication
scalarIdent : {n : ℕ} -> (v : Parikh n) -> (1 ·ₛ v ≡ v )
scalarIdent [] = refl
scalarIdent (x ∷ v) rewrite scalarIdent v | ident0 x = refl

--A linear set is defined by an offset vector b
--And a set of m vectors v1 ... vm.
--A vector u is in a linear set if there exists constants c1 ... cm
--such that u = b + c1·v1 + ... + cm·vm

-- Wouter -- do you really want to existentially quantify m?
-- You could also define LinSet n m = Parikh n × Vec (Parikh n) m
--  I don' think it makes a whole lot of difference, but later on in applyLinCom
--  you use this anyway.
--  For what it's worth, you may want to note that ∃ n . Vec a n is isomorphic to List a
LinSet : ℕ -> Set
LinSet n = (Parikh n) × (∃ λ (m : ℕ) → Vec (Parikh n) m )

--Given an offset vector, a set of m Parikh vectors, and a set of m constants
--Return b + c1·v1 + ... + cm·vm
-- Wouter: you might want to consider defining this directly by recursion over the
--  cs and vset. The induction you use in this definition will determine how easy/hard
--  it might be to reason about this function later.
--  See the proof of sumPreserved in SemiLinRE, for instance.
applyLinComb : {n : ℕ} -> Parikh n -> (m : ℕ ) -> (Vec (Parikh n) m ) -> Vec ℕ m ->  Parikh n
applyLinComb base .0 [] cs = base
applyLinComb base (suc m) (firstVec ∷ vset) (firstConst ∷ cs) = (firstConst ·ₛ firstVec) +v (applyLinComb base m vset cs)

--Show that, if all the coefficients in a linear combination are 0, that the resulting vector is the base (offset) vector
v0apply : {n m : ℕ} -> (base : Parikh n) -> (vecs : Vec (Parikh n) m ) -> applyLinComb base m  vecs (v0 {m}) ≡ base
v0apply base [] = refl
v0apply {n} {suc m} base (x ∷ vecs) rewrite scalar0ident x | v0apply base vecs = v0identLeft

--A type acting as a witness that a vector is in a linear set
--Is just a set of coefficients, and a proof that those coefficients
--form v as a linear combination of vectors in our linear set's list
LinComb : {n : ℕ} -> Parikh n -> LinSet n -> Set
LinComb {n} initV (base , m , vset)  =
  ∃ (λ (cs : Vec ℕ m) -> applyLinComb base m vset cs ≡ initV )

--Sum of each vector in a linear set i.e. L1 + L2 = {x + y | x in L1, y in L2 }
--We just add the bases, and concatenate the list of vectors which can be multiplied by constants
_+l_ : {n : ℕ} -> LinSet n -> LinSet n -> LinSet n
(base1 , m1 , vecs1 ) +l (base2 , m2 , vecs2 ) = (base1 +v base2 , m1 + m2 , vecs1 Data.Vec.++ vecs2 )

--A semi-linear is a finite union of linear sets
--We represent this using a list of linear sets
SemiLinSet : ℕ -> Set
SemiLinSet n = List (LinSet n)

--Sum each linear set in the two semi-linear sets
--We basically just do a pairwise +l for each linear set in each of the semi-linear sets
_+s_ : {n : ℕ} -> SemiLinSet n -> SemiLinSet n -> SemiLinSet n
s1 +s s2 = Data.List.concat (Data.List.map (λ l1 -> Data.List.map (λ l2 -> l1 +l l2 )  s2 ) s1 )

--Data type for a witness that an element is in a semiLinear set
--Basically just a proof that there's some element (linear set) of the list containing the vector
data InSemiLin : {n : ℕ} -> (v : Parikh n) -> (sl : SemiLinSet n) -> Set where
  InHead : {n : ℕ}
    -> (v : Parikh n)
    -> (sh : LinSet n)
    -> (st : SemiLinSet n)
    -> LinComb v sh
    -> InSemiLin v (sh ∷ st)
  InTail : {n : ℕ}
    -> (v : Parikh n)
    -> (sh : LinSet n)
    -> (st : SemiLinSet n)
    -> InSemiLin v st
    -> InSemiLin v (sh ∷ st)

--Creates a  vector
--Which has 1 in the specified component, and 0 elsewhere
basis : { n : ℕ} -> ( i : Fin.Fin n ) -> Parikh n
basis Fin.zero  = Data.Vec.[ suc zero ] Data.Vec.++ v0
basis (Fin.suc f) = 0 ∷ basis f

--A proof that if a vector is in a SemiLinear set, then the vector is also in the
--union of that SemiLinear set with another single linear set
slExtend : {n : ℕ} -> (v : Parikh n) -> (sl : SemiLinSet n) -> InSemiLin v sl -> (ls : LinSet n) -> InSemiLin v (ls ∷ sl )
slExtend v sl inTail ls = InTail v ls sl inTail

--the above proof, but extended to an arbitrary number of linear sets
slConcatLeft : {n : ℕ} -> (v : Parikh n) -> (sl : SemiLinSet n) -> InSemiLin v sl -> (sl2 : SemiLinSet n) -> InSemiLin v (sl2 Data.List.++  sl )
slConcatLeft v sl inTail [] = inTail
slConcatLeft v sl inTail (x ∷ sl2) = InTail v x (sl2 Data.List.++ sl) (slConcatLeft v sl inTail sl2)

--The above proof, but the vectors are concatenated on the right
slConcatRight : {n : ℕ} -> (v : Parikh n) -> (sl : SemiLinSet n) -> InSemiLin v sl -> (sl2 : SemiLinSet n) -> InSemiLin v (sl Data.List.++  sl2 )
slConcatRight v .(sh ∷ st) (InHead .v sh st x) sl2 = (InHead v sh (st Data.List.++ sl2) x)
slConcatRight v .(sh ∷ st) (InTail .v sh st inTail) sl2 = slExtend v (st Data.List.++ sl2) (slConcatRight v st inTail sl2) sh

--Show that, if a vector is in a linear-set, then it is in a semi-linear set containing that linear set
slCons :  {n : ℕ} -> (v : Parikh n) -> (sl : SemiLinSet n) -> (ls : LinSet n) -> (InSemiLin v (ls ∷ [] ) ) -> InSemiLin v (ls ∷ sl )
slCons v sl sh (InHead .v .sh .[] x) = InHead v sh sl x
slCons v sl sh (InTail .v .sh .[] ())

--A linear set containing only v0
l0 : {n : ℕ} -> LinSet n
l0 = (v0 , zero , [] )

--A semi-linear set containing only v0
s0 : {n : ℕ} -> SemiLinSet n
s0 = (v0 , zero , [] ) ∷ []

--Show that, if a vector is in s0, then it must be v0
s0match : {n : ℕ} -> (v : Parikh n) -> InSemiLin v s0 -> v ≡ v0
s0match .v0 (InHead .v0 .(v0 , 0 , []) .[] (comb , refl)) = refl
s0match v (InTail .v .(v0 , 0 , []) .[] ())

--Show that if a vector is in a semi-lin set, then it's not the empty list
inSemiNonEmtpy : {n : ℕ} -> (v : Parikh n) -> (s : SemiLinSet n) -> InSemiLin v s -> ∃ λ sh -> ∃ λ st -> s ≡ sh ∷ st
inSemiNonEmtpy v .(sh ∷ st) (InHead .v sh st x) = sh , st , refl
inSemiNonEmtpy v .(sh ∷ st) (InTail .v sh st inSemi) = sh , st , refl

-------------Functions for Star ------------------
-- Star is by far the most complicated case, so a large number of definitions and lemmas
--Are dedicated to it

--Given a linear set L, find another linear set
--such that L = L +l (L*)
--We do this by allowing the base to appear an arbitrary number of times
linStar : {n : ℕ} -> LinSet n -> LinSet n
linStar (base , m , vecs ) = (base , suc m , base ∷ vecs )

--Given a non-empty semi-linear set, find the sum of the star
--of all linear sets it contains
starSum : {n : ℕ} -> LinSet n -> SemiLinSet n -> LinSet n
starSum ls [] = linStar ls
starSum first (sh ∷ s) = (linStar sh) +l starSum first s

--The semi-linear set for the Star of a regular expression
--The semi-linear set always contains 0, since the empty string matches r*
--We then union s0 with the sum of the star of each linear set
--in the Parikh image of r
starSemiLin : {n : ℕ} -> SemiLinSet n -> SemiLinSet n
starSemiLin [] = s0
starSemiLin (first ∷ s) = s0 Data.List.++ (  starSum first s ∷ [])

--Show that v0 is always in a star semi-linear set
zeroInStar : {n : ℕ} -> (s ss : SemiLinSet n) -> ss ≡ (starSemiLin s)  -> InSemiLin v0 ss
zeroInStar [] .((v0 , 0 , []) ∷ []) refl = InHead v0 (v0 , zero , []) [] ([] , refl)
zeroInStar (x ∷ s) .((v0 , 0 , []) ∷ starSum x s ∷ []) refl = InHead v0 (v0 , zero , []) (starSum x s ∷ []) ([] , refl)

--Show that if we sum two linear sets, then the number of vectors that can be combined
--is the sum of the number in each input set
linSetLen : {n : ℕ} -> (l1 l2 l3 : LinSet n) -> l1 +l l2 ≡ l3 -> (proj₁ (proj₂ l3)) ≡ (proj₁ (proj₂ l1)) + (proj₁ (proj₂ l2))
linSetLen (proj₁ , m1 , proj₂) (proj₃ , m2 , proj₄) .(proj₁ +v proj₃ , m1 + m2 , proj₂ Data.Vec.++ proj₄) refl = refl

--Useful lemma, suc x = x + 1
plusOneDef : ( x : ℕ) -> (suc x ≡ x + 1)
plusOneDef zero = refl
plusOneDef (suc x) = cong suc (plusOneDef x)

--Show that we can "remove" part of the base vector
--When making a linear combination
baseSplit : {n : ℕ} (ub vb : Parikh n) (vm : ℕ) (vvecs : Vec (Parikh n) vm) (vconsts : Vec ℕ vm) ->
  applyLinComb (ub +v vb) vm vvecs vconsts
  ≡ ub +v applyLinComb vb vm vvecs vconsts
baseSplit ub vb .0 [] [] = refl
baseSplit ub vb (suc m) (x ∷ vvecs) (c ∷ vconsts)  =
  begin
  applyLinComb (ub +v vb) (suc m) (x ∷ vvecs) (c ∷ vconsts)
  ≡⟨ refl ⟩ --cong {!!} (baseSplit ub vb _ vvecs vconsts)
  (c ·ₛ x) +v applyLinComb (ub +v vb) m vvecs vconsts
  ≡⟨ cong (λ x₁ → (c ·ₛ x) +v x₁) (baseSplit ub vb m vvecs vconsts) ⟩
  (c ·ₛ x) +v (ub +v applyLinComb vb m vvecs vconsts)
  ≡⟨ sym vAssoc ⟩
  ((c ·ₛ x) +v ub) +v applyLinComb vb m vvecs vconsts
  ≡⟨ cong (λ x₁ → x₁ +v applyLinComb vb m vvecs vconsts) (v+-commut (c ·ₛ x) ub) ⟩
  (ub +v (c ·ₛ x)) +v applyLinComb vb m vvecs vconsts
  ≡⟨ vAssoc ⟩
  (ub +v ((c ·ₛ x) +v applyLinComb vb m vvecs vconsts) ∎)

--If we have two linear combinations of vectors,
--That we can make it into a single combination of vectors
--By adding the bases, and concatenating the vector lists, and
-- concatenating the coefficient lists
combSplit :
  {n : ℕ} (ub vb : Parikh n) (um vm : ℕ) (uvecs : Vec (Parikh n) um) (vvecs : Vec (Parikh n) vm) (uconsts : Vec ℕ um) (vconsts : Vec ℕ vm) ->
  (applyLinComb (ub +v vb) (um + vm) (uvecs Data.Vec.++ vvecs) (uconsts Data.Vec.++ vconsts)
  ≡ (applyLinComb ub um uvecs uconsts) +v (applyLinComb vb vm vvecs vconsts) )
combSplit ub vb .0 vm [] vvecs [] vconsts = baseSplit ub vb vm vvecs vconsts
combSplit ub vb (suc um) vm (x ∷ uvecs) vvecs (uc ∷ uconsts) vconsts =
  begin
  applyLinComb (ub +v vb) (suc (um + vm))
    (x ∷ uvecs Data.Vec.++ vvecs) ((uc ∷ uconsts) Data.Vec.++ vconsts)
  ≡⟨ refl ⟩
  (uc ·ₛ x) +v applyLinComb (ub +v vb) (um + vm) (uvecs Data.Vec.++ vvecs)
                 (uconsts Data.Vec.++ vconsts)
  ≡⟨ cong (λ x₁ → (uc ·ₛ x) +v x₁) (combSplit ub vb um vm uvecs vvecs uconsts vconsts) ⟩
  (uc ·ₛ x) +v
    (applyLinComb ub um uvecs uconsts +v
     applyLinComb vb vm vvecs vconsts)
  ≡⟨ sym vAssoc ⟩
  ((uc ·ₛ x) +v applyLinComb ub um uvecs uconsts) +v
    applyLinComb vb vm vvecs vconsts
  ≡⟨ refl ⟩
  (((uc ·ₛ x) +v applyLinComb ub um uvecs uconsts) +v
     applyLinComb vb vm vvecs vconsts ∎)

--Extend the idea of distributivity to linear combinations
--Basically, the c1*v +v c2*v = (c1 +v c2 )*v, where * is element-wise product
applyCombSum :
  {n m : ℕ} ->
  (vecs : Vec (Parikh n) m ) ->
  (uconsts vconsts : Parikh m ) ->
  applyLinComb v0 m vecs (uconsts +v vconsts) ≡ applyLinComb v0 m vecs uconsts +v applyLinComb v0 m vecs vconsts
applyCombSum [] uconsts vconsts = sym v0identRight
applyCombSum {n} {suc m} (firstVec ∷ vecs) (uc ∷ uconsts) (vc ∷ vconsts) rewrite applyCombSum vecs uconsts vconsts | scalarAssoc uc vc firstVec =
  begin
  ((uc ·ₛ firstVec) +v (vc ·ₛ firstVec)) +v
    (applyLinComb v0 m vecs uconsts +v
     applyLinComb v0 m vecs vconsts)
  ≡⟨ vAssoc ⟩
  (uc ·ₛ firstVec) +v
    ((vc ·ₛ firstVec) +v
     (applyLinComb v0 m vecs uconsts +v
      applyLinComb v0 m vecs vconsts))
  ≡⟨ cong (λ x → (uc ·ₛ firstVec) +v x) (v+-commut (vc ·ₛ firstVec) (applyLinComb v0 m vecs uconsts +v applyLinComb v0 m vecs vconsts)) ⟩
  (uc ·ₛ firstVec) +v
    ((applyLinComb v0 m vecs uconsts +v applyLinComb v0 m vecs vconsts)
     +v (vc ·ₛ firstVec))
  ≡⟨ sym vAssoc ⟩
  ((uc ·ₛ firstVec) +v
     (applyLinComb v0 m vecs uconsts +v applyLinComb v0 m vecs vconsts))
    +v (vc ·ₛ firstVec)
  ≡⟨ cong (λ x → x +v (vc ·ₛ firstVec)) (sym vAssoc) ⟩
  (((uc ·ₛ firstVec) +v applyLinComb v0 m vecs uconsts) +v
     applyLinComb v0 m vecs vconsts)
    +v (vc ·ₛ firstVec)
  ≡⟨ vAssoc ⟩
  ((uc ·ₛ firstVec) +v applyLinComb v0 m vecs uconsts) +v
    (applyLinComb v0 m vecs vconsts +v (vc ·ₛ firstVec))
  ≡⟨ cong (λ x → ((uc ·ₛ firstVec) +v applyLinComb v0 m vecs uconsts) +v x) (v+-commut (applyLinComb v0 m vecs vconsts) (vc ·ₛ firstVec)) ⟩
  ((uc ·ₛ firstVec) +v applyLinComb v0 m vecs uconsts) +v
    ((vc ·ₛ firstVec) +v applyLinComb v0 m vecs vconsts) ∎

--If a linear set has base 0, and u and v are both in that set, then u+v is as well
sumEqualVecs : {n : ℕ} -> (ls : LinSet n) -> (proj₁ ls ≡ v0) -> (u v : Parikh n) -> LinComb u ls -> LinComb v ls -> LinComb (u +v v) ls
sumEqualVecs (.v0 , m , vecs) refl .(applyLinComb v0 m vecs uconsts) .(applyLinComb v0 m vecs vconsts) (uconsts , refl) (vconsts , refl)  =
  (uconsts +v vconsts) , applyCombSum vecs uconsts vconsts --applyCombSum {!!} {!!} vecs uconsts vconsts

--Show that the base vector of a linear set is always in that set, just set coefficients to 0
linContainsBase : {n : ℕ} -> (base : Parikh n) -> (m : ℕ ) -> (vecs : Vec (Parikh n) m ) -> applyLinComb base m vecs v0 ≡ base
linContainsBase base .0 [] = refl
linContainsBase base (suc m) (x ∷ vecs) rewrite linContainsBase base m vecs  =
  begin
  (zero ·ₛ x) +v base
  ≡⟨ cong (λ y → y +v base) (scalar0ident x) ⟩
  v0 +v base
  ≡⟨ v0identLeft ⟩
  (base ∎)

--Show that applying a linear combination with the base is just
--The base, plus the linear combination with v0 base
--Just a useful lemma for other proofs, basically uses associativity
linCombRemoveBase
 :  {n : ℕ}
 -> (m : ℕ )
 -> (base : Parikh n )
 -> (vecs : Vec (Parikh n) m )
 -> (c : Parikh m)
 -> applyLinComb base m vecs c ≡ base +v applyLinComb v0 m vecs c
linCombRemoveBase {n} m base vecs c =
  begin
  applyLinComb base m vecs c
  ≡⟨ cong (λ x → applyLinComb x m vecs c) (sym v0identRight) ⟩
  applyLinComb (base +v v0) m vecs c
  ≡⟨ baseSplit base v0 m vecs c ⟩
  base +v applyLinComb v0 m vecs c ∎

--Show that only v0 is in a set with no vectors and v0 base
emptyCombZero : {n : ℕ} -> (v : Parikh n ) -> LinComb v (v0 , 0 , []) -> v ≡ v0
emptyCombZero .v0 ([] , refl) = refl

--Show that when we add two linear combinations of the same vectors together,
--We get a linear combination of those vectors, with an extra base left-over
linCombDecompBase
 :  {n : ℕ}
 -> (m : ℕ )
 -> (base : Parikh n )
 -> (vecs : Vec (Parikh n) m )
 -> (c1 : Parikh m )
 -> (c2 : Parikh m)
 -> (applyLinComb base m vecs c1 ) +v (applyLinComb base m vecs c2 ) ≡ base +v applyLinComb base m vecs (c1 +v c2)
linCombDecompBase .0 base [] c1 c2 = refl
linCombDecompBase (suc m) base (vec1 ∷ vecs) (c ∷ c1) (cc ∷ c2) rewrite linCombDecompBase m base vecs c1 c2 | linCombRemoveBase m base vecs c1 | linCombRemoveBase m base vecs c2   =
  begin
  ((c ·ₛ vec1) +v (base +v applyLinComb v0 m vecs c1)) +v
    ((cc ·ₛ vec1) +v (base +v applyLinComb v0 m vecs c2))
  ≡⟨ cong (λ x → x +v ((cc ·ₛ vec1) +v (base +v applyLinComb v0 m vecs c2))) (sym vAssoc ) ⟩
  (((c ·ₛ vec1) +v base) +v applyLinComb v0 m vecs c1) +v
    ((cc ·ₛ vec1) +v (base +v applyLinComb v0 m vecs c2))
  ≡⟨ cong (λ x → (x +v applyLinComb v0 m vecs c1) +v ((cc ·ₛ vec1) +v (base +v applyLinComb v0 m vecs c2))) (v+-commut (c ·ₛ vec1) base) ⟩
  ((base +v (c ·ₛ vec1)) +v applyLinComb v0 m vecs c1) +v
    ((cc ·ₛ vec1) +v (base +v applyLinComb v0 m vecs c2))
  ≡⟨ cong (λ x → x +v ((cc ·ₛ vec1) +v (base +v applyLinComb v0 m vecs c2))) vAssoc ⟩
  (base +v ((c ·ₛ vec1) +v applyLinComb v0 m vecs c1)) +v
    ((cc ·ₛ vec1) +v (base +v applyLinComb v0 m vecs c2))
  ≡⟨ vAssoc ⟩
  base +v
    (((c ·ₛ vec1) +v applyLinComb v0 m vecs c1) +v
     ((cc ·ₛ vec1) +v (base +v applyLinComb v0 m vecs c2)))
  ≡⟨ cong (λ x → base +v (((c ·ₛ vec1) +v applyLinComb v0 m vecs c1) +v x)) (sym vAssoc) ⟩
  base +v
    (((c ·ₛ vec1) +v applyLinComb v0 m vecs c1) +v
     (((cc ·ₛ vec1) +v base) +v applyLinComb v0 m vecs c2))
  ≡⟨ cong (λ x → base +v (((c ·ₛ vec1) +v applyLinComb v0 m vecs c1) +v (x +v applyLinComb v0 m vecs c2))) (v+-commut (cc ·ₛ vec1) base) ⟩
  base +v
    (((c ·ₛ vec1) +v applyLinComb v0 m vecs c1) +v
     ((base +v (cc ·ₛ vec1)) +v applyLinComb v0 m vecs c2))
  ≡⟨ cong (λ x → base +v x) vAssoc ⟩
  base +v
    ((c ·ₛ vec1) +v
     (applyLinComb v0 m vecs c1 +v
      ((base +v (cc ·ₛ vec1)) +v applyLinComb v0 m vecs c2)))
  ≡⟨ cong (λ x → base +v ((c ·ₛ vec1) +v x)) (sym vAssoc) ⟩
  base +v
    ((c ·ₛ vec1) +v
     ((applyLinComb v0 m vecs c1 +v (base +v (cc ·ₛ vec1))) +v
      applyLinComb v0 m vecs c2))
  ≡⟨ cong (λ x → base +v ((c ·ₛ vec1) +v (x +v applyLinComb v0 m vecs c2))) (v+-commut (applyLinComb v0 m vecs c1) (base +v (cc ·ₛ vec1))) ⟩
  base +v
    ((c ·ₛ vec1) +v
     (((base +v (cc ·ₛ vec1)) +v applyLinComb v0 m vecs c1) +v
      applyLinComb v0 m vecs c2))
  ≡⟨ cong (λ x → base +v ((c ·ₛ vec1) +v x)) vAssoc ⟩
  base +v
    ((c ·ₛ vec1) +v
     ((base +v (cc ·ₛ vec1)) +v
      (applyLinComb v0 m vecs c1 +v applyLinComb v0 m vecs c2)))
  ≡⟨ cong (λ x → base +v ((c ·ₛ vec1) +v ((base +v (cc ·ₛ vec1)) +v x))) (sym (applyCombSum vecs c1 c2)) ⟩
  base +v
    ((c ·ₛ vec1) +v
     ((base +v (cc ·ₛ vec1)) +v applyLinComb v0 m vecs (c1 +v c2)))
  ≡⟨ cong (λ x → base +v x) (sym vAssoc) ⟩
  base +v
    (((c ·ₛ vec1) +v (base +v (cc ·ₛ vec1))) +v
     applyLinComb v0 m vecs (c1 +v c2))
  ≡⟨ cong (λ x → base +v (x +v applyLinComb v0 m vecs (c1 +v c2))) (sym vAssoc) ⟩
  base +v
    ((((c ·ₛ vec1) +v base) +v (cc ·ₛ vec1)) +v
     applyLinComb v0 m vecs (c1 +v c2))
  ≡⟨ cong (λ x → base +v ((x +v (cc ·ₛ vec1)) +v applyLinComb v0 m vecs (c1 +v c2))) (v+-commut (c ·ₛ vec1) base) ⟩
  base +v
    (((base +v (c ·ₛ vec1)) +v (cc ·ₛ vec1)) +v
     applyLinComb v0 m vecs (c1 +v c2))
  ≡⟨ cong (λ x → base +v (x +v applyLinComb v0 m vecs (c1 +v c2))) vAssoc ⟩
  base +v
    ((base +v ((c ·ₛ vec1) +v (cc ·ₛ vec1))) +v
     applyLinComb v0 m vecs (c1 +v c2))
  ≡⟨ cong (λ x → base +v ((base +v x) +v applyLinComb v0 m vecs (c1 +v c2))) (sym (scalarAssoc c cc vec1)) ⟩
  base +v
    ((base +v ((c + cc) ·ₛ vec1)) +v applyLinComb v0 m vecs (c1 +v c2))
  ≡⟨ cong (λ x → base +v (x +v applyLinComb v0 m vecs (c1 +v c2))) (v+-commut base ((c + cc) ·ₛ vec1)) ⟩
  base +v
    ((((c + cc) ·ₛ vec1) +v base) +v applyLinComb v0 m vecs (c1 +v c2))
  ≡⟨ cong (λ x → base +v x) vAssoc ⟩
  base +v
    (((c + cc) ·ₛ vec1) +v (base +v applyLinComb v0 m vecs (c1 +v c2)))
  ≡⟨ cong (λ x → base +v (((c + cc) ·ₛ vec1) +v x)) (sym (baseSplit base v0 m vecs (c1 +v c2))) ⟩
  base +v
    (((c + cc) ·ₛ vec1) +v applyLinComb (base +v v0) m vecs (c1 +v c2))
  ≡⟨ cong (λ x → base +v (((c + cc) ·ₛ vec1) +v applyLinComb x m vecs (c1 +v c2))) v0identRight ⟩
  base +v (((c + cc) ·ₛ vec1) +v applyLinComb base m vecs (c1 +v c2))
  ≡⟨ cong (λ x → base +v x) refl ⟩
  (base +v (((c + cc) ·ₛ vec1) +v applyLinComb base m vecs (c1 +v c2)) ∎)

--Show that, if v1 is in L, and v2 is in L*, then v1 +v v2 is in L*
--Can be used to show that the sum of any vectors from L will be in L*
linStarExtend
  : {n : ℕ} -> (v1 v2 : Parikh n ) ->
  (l1 ls : LinSet n ) -> ls ≡ linStar l1  -> LinComb v1 l1 -> LinComb v2 ls -> LinComb (v1 +v v2) ls
linStarExtend .(applyLinComb base m vecs c1) .((c2h ·ₛ base) +v applyLinComb base m vecs c2) (base , m , vecs) .(base , suc m , base ∷ vecs) refl (c1 , refl) (c2h ∷ c2 , refl)  =
  ((1 ∷ c1) +v (c2h ∷ c2)) ,
  (begin
  (suc c2h ·ₛ base) +v applyLinComb base m vecs (c1 +v c2)
  ≡⟨ cong (λ x → (x ·ₛ base) +v applyLinComb base m vecs (c1 +v c2)) refl  ⟩
  ((1 + c2h) ·ₛ base) +v applyLinComb base m vecs (c1 +v c2)
  ≡⟨ cong (λ x → (x ·ₛ base) +v applyLinComb base m vecs (c1 +v c2)) (+-comm (suc zero) c2h) ⟩
  ((c2h + 1) ·ₛ base) +v applyLinComb base m vecs (c1 +v c2)
  ≡⟨ cong (λ x → x +v applyLinComb base m vecs (c1 +v c2)) (scalarAssoc c2h 1 base) ⟩
  ((c2h ·ₛ base) +v (1 ·ₛ base)) +v
    applyLinComb base m vecs (c1 +v c2)
  ≡⟨ cong (λ x → ((c2h ·ₛ base) +v x) +v applyLinComb base m vecs (c1 +v c2)) (scalarIdent base) ⟩
  ((c2h ·ₛ base) +v base) +v applyLinComb base m vecs (c1 +v c2)
  ≡⟨ vAssoc ⟩
  (c2h ·ₛ base) +v (base +v applyLinComb base m vecs (c1 +v c2))
  ≡⟨ cong (λ x → (c2h ·ₛ base) +v x) (sym (linCombDecompBase m base vecs c1 c2)) ⟩
  (c2h ·ₛ base) +v
    (applyLinComb base m vecs c1 +v applyLinComb base m vecs c2)
  ≡⟨ cong (λ x → (c2h ·ₛ base) +v x) (v+-commut (applyLinComb base m vecs c1) (applyLinComb base m vecs c2)) ⟩
  (c2h ·ₛ base) +v
    (applyLinComb base m vecs c2 +v applyLinComb base m vecs c1)
  ≡⟨ sym vAssoc ⟩
  ((c2h ·ₛ base) +v applyLinComb base m vecs c2) +v
    applyLinComb base m vecs c1
  ≡⟨ cong (λ x → x +v applyLinComb base m vecs c1 ) refl ⟩
  (applyLinComb base (suc m) (base ∷ vecs) (c2h ∷ c2)) +v
    applyLinComb base m vecs c1
  ≡⟨ v+-commut ((c2h ·ₛ base) +v applyLinComb base m vecs c2) (applyLinComb base m vecs c1) ⟩ applyLinComb base m vecs c1 +v
              ((c2h ·ₛ base) +v applyLinComb base m vecs c2) ∎
  )

--Show that every non-empty vector in L* for a linear-set L
--Can be split into a vector from L and another in L*
--Basically proves that L* contains only sums of vectors in L
linStarDecomp
 :  {n : ℕ}
 -> (v : Parikh n)
 -> (l ls : LinSet n)
 -> v ≢ v0
 -> proj₁ (l) ≢ v0
 -> ls ≡ linStar l
 -> LinComb v ls
 -> LinComb v l ⊎ (∃ λ v1 -> ∃ λ v2 -> v1 +v v2 ≡ v × LinComb v1 l × LinComb v2 ls × v1 ≢ v0 )
linStarDecomp .((0 ·ₛ base) +v applyLinComb base m vecs c) (base , m , vecs) .(base , suc m , base ∷ vecs) vnz bnz refl (zero ∷ c , refl) rewrite scalar0ident base  = inj₁ (c , (sym v0identLeft))
linStarDecomp .((suc cbase ·ₛ base) +v applyLinComb base m vecs c) (base , m , vecs) .(base , suc m , base ∷ vecs) vnz bnz refl (suc cbase ∷ c , refl) = inj₂ ( base , (applyLinComb base (suc m) (base ∷ vecs) (cbase ∷ c)) ,
  (sym (begin -- ? ≡⟨ ? ⟩ ?
    (suc cbase ·ₛ base) +v applyLinComb base m vecs c
    ≡⟨ cong (λ x → x +v applyLinComb base m vecs c) refl ⟩
    ((1 + cbase) ·ₛ base) +v applyLinComb base m vecs c
    ≡⟨ cong (λ x → x +v applyLinComb base m vecs c) (scalarAssoc 1 cbase base) ⟩
    ((suc zero ·ₛ base) +v (cbase ·ₛ base)) +v
      applyLinComb base m vecs c
    ≡⟨ cong (λ x → (x +v (cbase ·ₛ base)) +v applyLinComb base m vecs c) (scalarIdent base) ⟩
    (base +v (cbase ·ₛ base)) +v applyLinComb base m vecs c
    ≡⟨  vAssoc ⟩
    base +v ((cbase ·ₛ base) +v applyLinComb base m vecs c)
    ≡⟨ refl ⟩
    (base +v ((cbase ·ₛ base) +v applyLinComb base m vecs c) ∎))) ,
  (v0 , linContainsBase base m vecs) , ((cbase ∷ c) , refl) , bnz )

max_stars_repo_name: JoeyEremondi/agda-parikh

max_issues_repo_name: JoeyEremondi/agda-parikh

max_forks_repo_name: JoeyEremondi/agda-parikh


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

open import HoTT
open import homotopy.elims.SuspSmash
open import homotopy.elims.CofPushoutSection

-- Σ(X∧Y) ≃ X * Y

module homotopy.SuspSmash {i j} (X : Ptd i) (Y : Ptd j) where

private

  {- path lemmas -}
  private
    reduce-x : ∀ {i} {A : Type i} {x y z : A} (p : x == y) (q : z == y)
      → p ∙ ! q ∙ q ∙ ! p ∙ p == p
    reduce-x idp idp = idp

    reduce-y : ∀ {i} {A : Type i} {x y z : A} (p : x == y) (q : x == z)
      → p ∙ ! p ∙ q ∙ ! q ∙ p == p
    reduce-y idp idp = idp

  module Into = SuspRec {A = Smash X Y}
    {C = de⊙ X * de⊙ Y}
    (left (pt X))
    (right (pt Y))
    (Smash-rec
      (λ x y →
        jglue (pt X) (pt Y) ∙ ! (jglue x (pt Y))
        ∙ jglue x y
        ∙ ! (jglue (pt X) y) ∙ jglue (pt X) (pt Y))
      (jglue (pt X) (pt Y))
      (jglue (pt X) (pt Y))
      (λ x → reduce-x (jglue (pt X) (pt Y)) (jglue x (pt Y)))
      (λ y → reduce-y (jglue (pt X) (pt Y)) (jglue (pt X) y)))

  into = Into.f

  module Out = JoinRec
    {C = Susp (Smash X Y)}
    (λ _ → north)
    (λ _ → south)
    (λ x y → merid (smin x y))

  out = Out.f

  abstract
    into-out : (j : de⊙ X * de⊙ Y) → into (out j) == j
    into-out = Join-elim
      (λ x → glue (pt X , pt Y) ∙ ! (glue (x , pt Y)))
      (λ y → ! (glue (pt X , pt Y)) ∙ glue (pt X , y))
      (λ x y → ↓-∘=idf-from-square into out $
        (ap (ap into) (Out.glue-β x y)
         ∙ Into.merid-β (smin x y))
        ∙v⊡ lemma (glue (pt X , pt Y)) (glue (x , pt Y))
                  (glue (pt X , y)) (glue (x , y)))
      where
      lemma : ∀ {i} {A : Type i} {x y z w : A}
        (p : x == y) (q : z == y) (r : x == w) (s : z == w)
        → Square (p ∙ ! q) (p ∙ ! q ∙ s ∙ ! r ∙ p) s (! p ∙ r)
      lemma idp idp idp s =
        vert-degen-square (∙-unit-r s)

    out-into : (σ : Susp (Smash X Y)) → out (into σ) == σ
    out-into = SuspSmash-elim
      idp
      idp
      (λ x y → ↓-∘=idf-in' out into $
        ap (ap out) (Into.merid-β (smin x y))
        ∙ lemma₁ out (Out.glue-β (pt X) (pt Y))
                     (Out.glue-β x (pt Y))
                     (Out.glue-β x y)
                     (Out.glue-β (pt X) y)
                     (Out.glue-β (pt X) (pt Y))
        ∙ lemma₂ {p = merid (smin (pt X) (pt Y))}
                 {q = merid (smin x (pt Y))}
                 {r = merid (smin x y)}
                 {s = merid (smin (pt X) y)}
                 {t = merid (smin (pt X) (pt Y))}
            (ap merid (smgluel (pt X) ∙ ! (smgluel x)))
            (ap merid (smgluer y ∙ ! (smgluer (pt Y)))))
      where
      lemma₁ : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
        {x y z u v w : A}
        {p : x == y} {q : z == y} {r : z == u} {s : v == u} {t : v == w}
        {p' : f x == f y} {q' : f z == f y} {r' : f z == f u}
        {s' : f v == f u} {t' : f v == f w}
        (α : ap f p == p') (β : ap f q == q') (γ : ap f r == r')
        (δ : ap f s == s') (ε : ap f t == t')
        → ap f (p ∙ ! q ∙ r ∙ ! s ∙ t) == p' ∙ ! q' ∙ r' ∙ ! s' ∙ t'
      lemma₁ f {p = idp} {q = idp} {r = idp} {s = idp} {t = idp}
            idp idp idp idp idp
        = idp

      lemma₂ : ∀ {i} {A : Type i} {x y z u : A}
        {p q : x == y} {r : x == z} {s t : u == z}
        (α : p == q) (β : s == t)
        → p ∙ ! q  ∙ r ∙ ! s ∙ t == r
      lemma₂ {p = idp} {r = idp} {s = idp} idp idp = idp

module SuspSmash where

  eq : Susp (Smash X Y) ≃ (de⊙ X * de⊙ Y)
  eq = equiv into out into-out out-into

  ⊙eq : ⊙Susp (⊙Smash X Y) ⊙≃ (X ⊙* Y)
  ⊙eq = ≃-to-⊙≃ eq idp

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

module Algebra.Linear.Structures.Bundles.FiniteDimensional where

open import Algebra
open import Algebra.FunctionProperties
open import Relation.Binary using (Rel)
open import Level using (Level; suc; _⊔_)

open import Algebra.Structures.Bundles.Field
open import Algebra.Linear.Structures.Bundles

open import Algebra.Linear.Structures.VectorSpace
open import Algebra.Linear.Structures.FiniteDimensional

open import Data.Nat using (ℕ)

record FiniteDimensional {k ℓᵏ} (K : Field k ℓᵏ) (c ℓ : Level) (n : ℕ) : Set (suc (c ⊔ k ⊔ ℓ ⊔ ℓᵏ)) where
  field
    Carrier             : Set c
    _≈_                 : Rel Carrier ℓ
    _+_                 : Carrier -> Carrier -> Carrier
    _∙_                 : Field.Carrier K -> Carrier -> Carrier
    -_                  : Carrier -> Carrier
    0#                  : Carrier
    isFiniteDimensional : IsFiniteDimensional K _≈_ _+_ _∙_ -_ 0# n

  open IsFiniteDimensional isFiniteDimensional public

  vectorSpace : VectorSpace K c ℓ
  vectorSpace = record { isVectorSpace = isVectorSpace }

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


text:
module Data.Word64.Exts where

open import Agda.Builtin.Nat
open import Agda.Builtin.Word
open import Data.Nat
open import Data.Word

addWord : Word64 → Word64 → Word64
addWord a b = primWord64FromNat (primWord64ToNat a + primWord64ToNat b)

subWord : Word64 → Word64 → Word64
subWord a b = primWord64FromNat (primWord64ToNat a - primWord64ToNat b)

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille