text:
module SimpleTermUnification where

open import OscarPrelude

data Term (n : Nat) : Set where
  var : Fin n → Term n
  leaf : Term n
  _fork_ : Term n → Term n → Term n

|> : ∀ {m n} → (r : Fin m → Fin n) → Fin m → Term n
|> r = var ∘ r

_<|_ : ∀ {m n} → (f : Fin m → Term n) → Term m → Term n
f <| var x = f x
f <| leaf = leaf
f <| (t₁ fork t₂) = (f <| t₁) fork (f <| t₂)

<|-assoc : ∀ {m n o} (f : Fin n → Term o) (g : Fin m → Term n) (x : Term m) → f <| (g <| x) ≡ (λ y → f <| g y) <| x
<|-assoc f g (var x) = refl
<|-assoc f g leaf = refl
<|-assoc f g (x₁ fork x₂) rewrite <|-assoc f g x₁ | <|-assoc f g x₂ = refl

_≗_ : ∀ {m n} → (f g : Fin m → Term n) → Set
f ≗ g = ∀ x → f x ≡ g x

infixr 9 _⋄_
_⋄_ : ∀ {l m n} → (f : Fin m → Term n) → (g : Fin l → Term m) → Fin l → Term n
(f ⋄ g) = (f <|_) ∘ g

⋄-assoc : ∀ {l m n o} (f : Fin n → Term o) (g : Fin m → Term n) (h : Fin l → Term m) → (f ⋄ (g ⋄ h)) ≗ ((f ⋄ g) ⋄ h)
⋄-assoc f g h x = <|-assoc f g (h x)

⋄-assoc' : ∀ {l m n o} (f : Fin n → Term o) (g : Fin m → Term n) (h : Fin l → Term m) → (f ⋄ (g ⋄ h)) ≡ ((f ⋄ g) ⋄ h)
⋄-assoc' f g h = {!⋄-assoc f g h!}

thin : ∀ {n} → (x : Fin (suc n)) → (y : Fin n) → Fin (suc n)
thin {n} zero y = suc y
thin {zero} (suc x) ()
thin {suc n} (suc x) zero = zero
thin {suc n} (suc x) (suc y) = suc (thin x y)

thick : ∀ {n} → (x y : Fin (suc n)) → Maybe (Fin n)
thick {n} zero zero = nothing
thick {n} zero (suc y) = just y
thick {zero} (suc ()) zero
thick {suc n} (suc x) zero = just zero
thick {zero} (suc ()) (suc y)
thick {suc n} (suc x) (suc y) = suc <$> thick x y

check : ∀ {n} → (x : Fin (suc n)) (t : Term (suc n)) → Maybe (Term n)
check x (var y) = var <$> thick x y
check x leaf = just leaf
check x (t₁ fork t₂) = _fork_ <$> check x t₁ <*> check x t₂

_for_ : ∀ {n} → (t' : Term n) (x : Fin (suc n)) → Fin (suc n) → Term n
(t' for x) y with thick x y
… | just y' = var y'
… | nothing = t'

data AList (n : Nat) : Nat → Set where
  anil : AList n n
  _asnoc_/_ : ∀ {m} → (σ : AList n m) → (t' : Term m) → (x : Fin (suc m)) → AList n (suc m)

sub : ∀ {n m} → (σ : AList n m) → Fin m → Term n
sub anil = var
sub (σ asnoc t' / x) = sub σ ⋄ (t' for x)

flexFlex : ∀ {m} → (x y : Fin m) → ∃ (flip AList m)
flexFlex {zero} () _
flexFlex {suc m} x y with thick x y
… | just y' = m , (anil asnoc var y' / x)
… | nothing = suc m , anil

flexRigid : ∀ {m} → (x : Fin m) (t : Term m) → Maybe (∃ (flip AList m))
flexRigid {zero} () _
flexRigid {suc m} x t with check x t
… | just t' = just $ m , anil asnoc t' / x
… | nothing = nothing

amgu : ∀ {m} → (s t : Term m) (acc : ∃ (flip AList m)) → Maybe (∃ (flip AList m))
amgu {m} leaf leaf acc = just acc
amgu {m} leaf (_ fork _) _ = nothing
amgu {m} (_ fork _) leaf _ = nothing
amgu {m} (s₁ fork s₂) (t₁ fork t₂) acc = amgu s₁ t₁ acc >>= amgu s₂ t₂
amgu {m} (var x) (var y) (.m , anil) = just $ flexFlex x y
amgu {m} (var x) t (.m , anil) = flexRigid x t
amgu {m} t (var x) (.m , anil) = flexRigid x t
amgu {suc m} s t (n , (σ asnoc r / z)) = amgu ((r for z) <| s) ((r for z) <| t) (n , σ) >>= λ {(n' , σ') → just $ n' , σ' asnoc r / z}

mgu : ∀ {m} → (s t : Term m) → Maybe (∃ (flip AList m))
mgu {m} s t = amgu s t (m , anil)

f : Fin 4 → Term 5
f n = var (thin (suc n) n) fork var (thin (suc n) n)

g : Fin 4 → Term 5
g n = var (suc n)

fs : Term 5
fs = f 0 fork (f 1 fork (f 2 fork f 3))

gs : Term 5
gs = g 0 fork (g 1 fork (g 2 fork g 3))

foo : Set
foo = {!mgu fs gs!}

Property : Nat → Set₁
Property m = ∀ {n} → (Fin m → Term n) → Set

Unifies : ∀ {m} → (s t : Term m) → Property m
Unifies s t f = f <| s ≡ f <| t

_∧_ : ∀ {m} → (P Q : Property m) → Property m
(P ∧ Q) f = P f × Q f

_⇔_ : ∀ {m} → (P Q : Property m) → Property m
(P ⇔ Q) f = (P f → Q f) × (Q f → P f)

Nothing : ∀ {m} (P : Property m) → Set
Nothing {m} P = ∀ {n} → (f : Fin m → Term n) → ¬ P f

infixl 3 _[-⋄_]_
_[-⋄_]_ : ∀ {m n} (P : Property m) (f : Fin m → Term n) → Property n
(P [-⋄ f ] g) = P (g ⋄ f)

_≤ₛ_ : ∀ {m n n'} (f : Fin m → Term n) (g : Fin m → Term n') → Set
f ≤ₛ g = ∃ λ f' → f ≗ (f' ⋄ g)

Max : ∀ {m} (P : Property m) → Property m
Max {m} P f = P f × ∀ {n} → (f' : Fin m → Term n) → P f' → f' ≤ₛ f

DClosed : ∀ {m} (P : Property m) → Set
DClosed {m} P = ∀ {n n'} (f : Fin m → Term n) (g : Fin m → Term n') → f ≤ₛ g → P g → P f

Lemma1 : ∀ {l} {P Q : Property l} {m n o}
           {p : Fin m → Term n}
           {q : Fin n → Term o}
           {a : Fin l → Term m}
         → DClosed P
         → Max (P [-⋄ a ]_) p
         → Max (Q [-⋄ (p ⋄ a)]_) q
         → Max ((P ∧ Q) [-⋄ a ]_) (q ⋄ p)
Lemma1 {P = P} {Q} {p = p} {q} {a} DCP maxP maxQ =
  let Qqpa : Q (q ⋄ p ⋄ a)
      Qqpa = fst maxQ
      Qqpa' : Q ((q ⋄ p) ⋄ a)
      Qqpa' = {!⋄-assoc q p a!}
      Pqpa : P (q ⋄ p ⋄ a)
      Pqpa = DCP (λ z → q <| (p <| a z)) (λ z → p <| a z) (q , (λ x → refl)) (fst maxP)
      lem3 : ∀ {n} → {f : Fin _ → Term n} → P (f ⋄ a) → Q (f ⋄ a) → f ≤ₛ (q ⋄ p)
      lem3 = {!!}
  in ({!!} , {!maxQ!}) , {!!}
  where
  Ppa : P (p ⋄ a)
  Ppa = fst maxP

  pMax : ∀ {n} {p' : Fin _ → Term n} → P (p' ⋄ a) → p' ≤ₛ p
  pMax {n} {p'} Pp'a = snd maxP p' Pp'a

data Step (n : Nat) : Set where
  left : Term n → Step n
  right : Term n → Step n

_+ₛ_ : ∀ {n} → (ps : List (Step n)) → (t : Term n) → Term n
[] +ₛ t = t
(left r ∷ ps) +ₛ t = (ps +ₛ t) fork r
(right l ∷ ps) +ₛ t = l fork (ps +ₛ t)

theorem-6 : ∀ m → (s t : Term m) → (r : Maybe (∃ (flip AList m))) → mgu s t ≡ r → Either (∃ λ n → ∃ λ σ → Max (Unifies s t) (sub σ) × r ≡ just (n , σ)) (Nothing (Unifies s t) × r ≡ nothing)
theorem-6 = {!!}


text:
module Types where

open import Data.Bool
open import Data.Fin using (Fin)
import      Data.Fin as F
open import Data.Nat renaming (_≟_ to _≟N_)
open import Data.Vec hiding (head; tail)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

infixl 80 _∙_

data Type : Set where
  𝔹  : Type
  𝔹⁺ : ℕ → Type
  ℂ  : Type → Type
  _⇒_ : Type → Type → Type
  _×_ : Type → Type → Type

data Syntax : Set where
  bitI   : Syntax
  bitO   : Syntax
  []     : Syntax
  _∷_    : Syntax → Syntax → Syntax
  _nand_ : Syntax → Syntax → Syntax
  reg    : Syntax → Syntax → Syntax
  pair   : Syntax → Syntax → Syntax
  latest : Syntax → Syntax
  head   : Syntax → Syntax
  tail   : Syntax → Syntax
  var    : ℕ → Syntax
  _∙_    : Syntax → Syntax → Syntax
  lam    : Type → Syntax → Syntax

Ctx : ℕ → Set
Ctx = Vec Type

data Term {n} (Γ : Ctx n) : Type → Set where
  bitI   : Term Γ 𝔹
  bitO   : Term Γ 𝔹
  []     : Term Γ (𝔹⁺ 0)
  _∷_    : ∀ {n} → Term Γ 𝔹 → Term Γ (𝔹⁺ n) → Term Γ (𝔹⁺ (suc n))
  _nand_ : Term Γ 𝔹 → Term Γ 𝔹 → Term Γ 𝔹
  reg    : ∀ {τ σ} → Term Γ τ → Term Γ (τ ⇒ (τ × σ)) → Term Γ (ℂ σ)
  pair   : ∀ {σ τ} → Term Γ σ → Term Γ τ → Term Γ (σ × τ)
  latest : ∀ {τ} → Term Γ (ℂ τ) → Term Γ τ
  head   : ∀ {n} → Term Γ (𝔹⁺ (suc n)) → Term Γ 𝔹
  tail   : ∀ {n} → Term Γ (𝔹⁺ (suc n)) → Term Γ (𝔹⁺ n)
  var    : ∀ {τ} (i : Fin n) → (lookup i Γ ≡ τ) → Term Γ τ
  _∙_    : ∀ {σ τ} → Term Γ (σ ⇒ τ) → Term Γ σ → Term Γ τ
  lam    : ∀ {σ τ} → Term (σ ∷ Γ) τ → Term Γ (σ ⇒ τ)

Closed : Type → Set
Closed τ = ∀ {n} {ctx : Ctx n} → Term ctx τ

≡𝔹⁺ : ∀ {n m} → 𝔹⁺ n ≡ 𝔹⁺ m → n ≡ m
≡𝔹⁺ refl = refl

≡ℂ : ∀ {τ σ} → ℂ τ ≡ ℂ σ → τ ≡ σ
≡ℂ refl = refl

≡⇒₁ : ∀ {σ σ′ τ τ′} → σ ⇒ τ ≡ σ′ ⇒ τ′ → σ ≡ σ′
≡⇒₁ refl = refl

≡⇒₂ : ∀ {σ σ′ τ τ′} → σ ⇒ τ ≡ σ′ ⇒ τ′ → τ ≡ τ′
≡⇒₂ refl = refl

≡×₁ : ∀ {σ σ′ τ τ′} → σ × τ ≡ σ′ × τ′ → σ ≡ σ′
≡×₁ refl = refl

≡×₂ : ∀ {σ σ′ τ τ′} → σ × τ ≡ σ′ × τ′ → τ ≡ τ′
≡×₂ refl = refl

_≟T_ : (σ τ : Type) → Dec (σ ≡ τ)
𝔹 ≟T 𝔹 = yes refl
𝔹 ≟T 𝔹⁺ _ = no (λ ())
𝔹 ≟T ℂ _ = no (λ ())
𝔹 ≟T (_ ⇒ _) = no (λ ())
𝔹 ≟T (_ × _) = no (λ ())
𝔹⁺ _ ≟T 𝔹 = no (λ ())
𝔹⁺ n ≟T 𝔹⁺ m with n ≟N m
𝔹⁺ n ≟T 𝔹⁺ .n | yes refl = yes refl
𝔹⁺ n ≟T 𝔹⁺ m  | no ¬p = no (λ x → ¬p (≡𝔹⁺ x))
𝔹⁺ _ ≟T ℂ _ = no (λ ())
𝔹⁺ _ ≟T (y ⇒ y₁) = no (λ ())
𝔹⁺ _ ≟T (y × y₁) = no (λ ())
ℂ _ ≟T 𝔹 = no (λ ())
ℂ _ ≟T 𝔹⁺ n = no (λ ())
ℂ τ ≟T ℂ σ with τ ≟T σ
ℂ τ ≟T ℂ .τ | yes refl = yes refl
ℂ τ ≟T ℂ σ | no ¬p = no (λ x → ¬p (≡ℂ x))
ℂ _ ≟T (_ ⇒ _) = no (λ ())
ℂ _ ≟T (_ × _) = no (λ ())
(_ ⇒ _) ≟T 𝔹 = no (λ ())
(σ ⇒ τ) ≟T 𝔹⁺ x₂ = no (λ ())
(_ ⇒ _) ≟T ℂ _ = no (λ ())
(σ ⇒ τ) ≟T (σ₁ ⇒ τ₁) with σ ≟T σ₁ | τ ≟T τ₁
(σ ⇒ τ) ≟T (σ₁ ⇒ τ₁) | yes p | yes p₁ = yes (cong₂ _⇒_ p p₁)
(σ ⇒ τ) ≟T (σ₁ ⇒ τ₁) |     _ | no  ¬p = no (λ x → ¬p (≡⇒₂ x))
(σ ⇒ τ) ≟T (σ₁ ⇒ τ₁) | no ¬p |      _ = no (λ x → ¬p (≡⇒₁ x))
(_ ⇒ _) ≟T (_ × _) = no (λ ())
(_ × _) ≟T 𝔹 = no (λ ())
(_ × _) ≟T 𝔹⁺ _ = no (λ ())
(_ × _) ≟T ℂ _ = no (λ ())
(_ × _) ≟T (_ ⇒ _) = no (λ ())
(σ × τ) ≟T (σ₁ × τ₁) with σ ≟T σ₁ | τ ≟T τ₁
(σ × τ) ≟T (σ₁ × τ₁) | yes p | yes p₁ = yes (cong₂ _×_ p p₁)
(σ × τ) ≟T (σ₁ × τ₁) | _ | no ¬p = no (λ x → ¬p (≡×₂ x))
(σ × τ) ≟T (σ₁ × τ₁) | no ¬p | _ = no (λ x → ¬p (≡×₁ x))

erase : ∀ {n} {Γ : Ctx n} {τ} → Term Γ τ → Syntax
erase bitI        = bitI
erase bitO        = bitO
erase []          = []
erase (x ∷ xs)    = erase x ∷ erase xs
erase (x nand y)  = erase x nand erase y
erase (reg x t)   = reg (erase x) (erase t)
erase (pair x y)  = pair (erase x) (erase y)
erase (latest x)  = latest (erase x)
erase (head x)    = head (erase x)
erase (tail x)    = tail (erase x)
erase (var v _)   = var (F.toℕ v)
erase (t ∙ u)     = erase t ∙ erase u
erase (lam {σ} t) = lam σ (erase t)

ext: agda

max_stars_repo_name: bens/hwlc

max_issues_repo_name: bens/hwlc

max_forks_repo_name: bens/hwlc


text:
{-# OPTIONS --without-K --rewriting #-}
open import HoTT.Base
open import HoTT.Identity
open import HoTT.Identity.Sigma
open import HoTT.Identity.Pi
open import HoTT.Identity.Universe
open import HoTT.Identity.Product
open import HoTT.HLevel
open import HoTT.HLevel.Truncate
open import HoTT.Equivalence
open import HoTT.Equivalence.Lift

module HoTT.Logic where

private variable i j k : Level

LiftProp : Prop𝒰 i → Prop𝒰 (i ⊔ j)
LiftProp {i} {j} P = type (Lift {j} (P ty))

⊤ : Prop𝒰 i
⊤ = type 𝟏

⊥ : Prop𝒰 i
⊥ = type 𝟎

_∧_ : Prop𝒰 i → Prop𝒰 j → Prop𝒰 (i ⊔ j)
P ∧ Q = type (P ty × Q ty) ⦃ ×-hlevel ⦄

_⇒_ : Prop𝒰 i → Prop𝒰 j → Prop𝒰 (i ⊔ j)
P ⇒ Q = type (P ty → Q ty)
infix 10 _⇒_

_⇔_ : Prop𝒰 i → Prop𝒰 i → Prop𝒰 (lsuc i)
P ⇔ Q = type (P ty == Q ty) ⦃ equiv-hlevel (=𝒰-equiv ⁻¹ₑ) ⦄
  where
  instance
    _ = Σ-hlevel
    _ = raise ⦃ hlevel𝒰.h P ⦄
    _ = raise ⦃ hlevel𝒰.h Q ⦄

_∨_ : Prop𝒰 i → Prop𝒰 j → Prop𝒰 (i ⊔ j)
P ∨ Q = type ∥ P ty + Q ty ∥

∃ : (A : 𝒰 i) → (A → Prop𝒰 j) → Prop𝒰 (i ⊔ j)
∃ A P = type ∥ Σ A (_ty ∘ P) ∥
syntax ∃ A (λ x → Φ) = ∃[ x ∶ A ] Φ

∀' : (A : 𝒰 i) → (P : A → Prop𝒰 j) → Prop𝒰 (i ⊔ j)
∀' A P = type (Π A (_ty ∘ P))
  where instance _ = λ {x} → hlevel𝒰.h (P x)
syntax ∀' A (λ x → Φ) = ∀[ x ∶ A ] Φ

LEM : 𝒰 (lsuc i)
LEM {i} = (A : Prop𝒰 i) → A ty + ¬ A ty

LEM∞ : 𝒰 (lsuc i)
LEM∞ {i} = (A : 𝒰 i) → A + ¬ A

LDN : 𝒰 (lsuc i)
LDN {i} = (A : Prop𝒰 i) → ¬ ¬ A ty → A ty

AC : 𝒰 (lsuc i ⊔ lsuc j ⊔ lsuc k)
AC {i} {j} {k} =
  {X : 𝒰 i} {A : X → 𝒰 j} {P : (x : X) → A x → 𝒰 k} →
  ⦃ hlevel 2 X ⦄ → ⦃ {x : X} → hlevel 2 (A x) ⦄ →
  ⦃ {x : X} {a : A x} → hlevel 1 (P x a) ⦄ →
  Π[ x ∶ X ] ∥ Σ[ a ∶ A x ] P x a ∥ →
  ∥ Σ[ g ∶ Π[ x ∶ X ] A x ] Π[ x ∶ X ] P x (g x) ∥

Lemma3/9/1 : (P : 𝒰 i) → ⦃ hlevel 1 P ⦄ → P ≃ ∥ P ∥
Lemma3/9/1 P = let open Iso in iso→eqv λ where
  .f → ∣_∣ ; .g → ∥-rec id ; .η _ → refl ; .ε _ → center

-- Principle of unique choice
Corollary3/9/2 : {A : 𝒰 i} {P : A → 𝒰 i} → ⦃ {x : A} → hlevel 1 (P x) ⦄ →
                 ((x : A) → ∥ P x ∥) → (x : A) → P x
Corollary3/9/2 {P = P} f = ∥-rec id ∘ f

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text: module Agda.TypeChecking.Lock where

max_stars_repo_name: jappeace/agda

max_issues_repo_name: jappeace/agda

max_forks_repo_name: jappeace/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.Pointed.FunExt where

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

open import Cubical.Foundations.Pointed.Base
open import Cubical.Foundations.Pointed.Properties
open import Cubical.Foundations.Pointed.Homotopy

private
  variable
    ℓ ℓ' : Level

module _ {A : Pointed ℓ} {B : typ A → Type ℓ'} {ptB : B (pt A)} where

  -- pointed function extensionality
  funExt∙P : {f g : Π∙ A B ptB} → f ∙∼P g → f ≡ g
  funExt∙P (h , h∙) i .fst x = h x i
  funExt∙P (h , h∙) i .snd = h∙ i

  -- inverse of pointed function extensionality
  funExt∙P⁻ : {f g : Π∙ A B ptB} → f ≡ g → f ∙∼P g
  funExt∙P⁻ p .fst a i = p i .fst a
  funExt∙P⁻ p .snd i = p i .snd

  -- function extensionality is an isomorphism, PathP version
  funExt∙PIso : (f g : Π∙ A B ptB) → Iso (f ∙∼P g) (f ≡ g)
  Iso.fun (funExt∙PIso f g)  = funExt∙P {f = f} {g = g}
  Iso.inv (funExt∙PIso f g) = funExt∙P⁻ {f = f} {g = g}
  Iso.rightInv (funExt∙PIso f g) p i j = p j
  Iso.leftInv (funExt∙PIso f g) h _ = h

  -- transformed to equivalence
  funExt∙P≃ : (f g : Π∙ A B ptB) → (f ∙∼P g) ≃ (f ≡ g)
  funExt∙P≃ f g = isoToEquiv (funExt∙PIso f g)

  -- funExt∙≃ using the other kind of pointed homotopy
  funExt∙≃ : (f g : Π∙ A B ptB) → (f ∙∼ g) ≃ (f ≡ g)
  funExt∙≃ f g = compEquiv (∙∼≃∙∼P f g) (funExt∙P≃ f g)

  -- standard pointed function extensionality and its inverse
  funExt∙ : {f g : Π∙ A B ptB} → f ∙∼ g → f ≡ g
  funExt∙ {f = f} {g = g} = equivFun (funExt∙≃ f g)

  funExt∙⁻ : {f g : Π∙ A B ptB} → f ≡ g → f ∙∼ g
  funExt∙⁻ {f = f} {g = g} = equivFun (invEquiv (funExt∙≃ f g))

max_stars_repo_name: L-TChen/cubical

max_issues_repo_name: L-TChen/cubical

max_forks_repo_name: L-TChen/cubical


text:
{-# OPTIONS --cubical --no-exact-split --safe #-}
module Cubical.Structures.MultiSet where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.SIP renaming (SNS-PathP to SNS)
open import Cubical.Functions.FunExtEquiv

open import Cubical.Structures.Pointed
open import Cubical.Structures.Queue

open import Cubical.Data.Unit
open import Cubical.Data.Sum
open import Cubical.Data.Nat
open import Cubical.Data.Sigma

module _(A : Type ℓ)
        (Aset : isSet A) where

 open Queues-on A Aset

 member-structure : Type ℓ → Type ℓ
 member-structure X = A → X → ℕ

 Member : Type (ℓ-suc ℓ)
 Member = TypeWithStr ℓ member-structure

 member-iso : StrIso member-structure ℓ
 member-iso (X , f) (Y , g) e = ∀ a x → f a x ≡ g a (e .fst x)

 Member-is-SNS : SNS {ℓ} member-structure member-iso
 Member-is-SNS = SNS-≡→SNS-PathP member-iso ((λ _ _ → funExt₂Equiv))

 -- a multi set structure inspired bei Okasaki
 multi-set-structure : Type ℓ → Type ℓ
 multi-set-structure X = X × (A → X → X) × (A → X → ℕ)

 Multi-Set : Type (ℓ-suc ℓ)
 Multi-Set = TypeWithStr ℓ multi-set-structure

 multi-set-iso : StrIso multi-set-structure ℓ
 multi-set-iso (X , emp₁ , insert₁ , memb₁) (Y , emp₂ , insert₂ , memb₂) e =
            (e .fst emp₁ ≡ emp₂)
          × (∀ a q → e .fst (insert₁ a q) ≡ insert₂ a (e .fst q))
          × (∀ a x → memb₁ a x ≡ memb₂ a (e .fst x))

 Multi-Set-is-SNS : SNS {ℓ₁ = ℓ} multi-set-structure multi-set-iso
 Multi-Set-is-SNS =
   join-SNS pointed-iso pointed-is-SNS
            {S₂ = λ X → (left-action-structure X) × (member-structure X)}
            (λ B C e →  (∀ a q → e .fst (B .snd .fst a q) ≡ C .snd .fst a (e .fst q))
                      × (∀ a x → (B .snd .snd a x) ≡ (C .snd .snd a (e .fst x))))
            (join-SNS left-action-iso Left-Action-is-SNS member-iso Member-is-SNS)


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

module Swaps where

-- Intermediate representation of permutations to prove soundness and
-- completeness

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

open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; subst; subst₂; cong; cong₂; setoid;
        inspect; [_]; proof-irrelevance; module ≡-Reasoning)
open import Relation.Binary.PropositionalEquality.TrustMe
  using (trustMe)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Data.Nat.Properties
  using (m≢1+m+n; i+j≡0⇒i≡0; i+j≡0⇒j≡0; n≤m+n)
open import Data.Nat.Properties.Simple
  using (+-right-identity; +-suc; +-assoc; +-comm;
        *-assoc; *-comm; *-right-zero; distribʳ-*-+)
open import Data.Nat.DivMod using (_mod_)
open import Relation.Binary using (Rel; Decidable; Setoid)
open import Relation.Binary.Core using (Transitive)

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

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

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

open import Cauchy
open import Perm
open import Proofs
open import CauchyProofs
open import CauchyProofsT
open import CauchyProofsS
open import Groupoid
open import PiLevel0

------------------------------------------------------------------------------
-- Representation of a permutation as a product of "transpositions."
-- This product is not commutative; we apply it from left to
-- right. Because we eventually want to normalize permutations to some
-- canonical representation, we insist that the first component of a
-- transposition is always ≤ than the second

infix 90 _X_

data Transposition (n : ℕ) : Set where
  _X_ : (i j : Fin n) → {p : toℕ i ≤ toℕ j} → Transposition n

i≰j→j≤i : (i j : ℕ) → (i ≰ j) → (j ≤ i)
i≰j→j≤i i 0 p = z≤n
i≰j→j≤i 0 (suc j) p with p z≤n
i≰j→j≤i 0 (suc j) p | ()
i≰j→j≤i (suc i) (suc j) p with i ≤? j
i≰j→j≤i (suc i) (suc j) p | yes p' with p (s≤s p')
i≰j→j≤i (suc i) (suc j) p | yes p' | ()
i≰j→j≤i (suc i) (suc j) p | no p' = s≤s (i≰j→j≤i i j p')

mkTransposition : {n : ℕ} → (i j : Fin n) → Transposition n
mkTransposition {n} i j with toℕ i ≤? toℕ j
... | yes p = _X_ i j {p}
... | no p  = _X_ j i {i≰j→j≤i (toℕ i) (toℕ j) p}

Transposition* : ℕ → Set
Transposition* n = List (Transposition n)

-- Representation of a permutation as a product of cycles where each
-- cycle is a non-empty sequence of indices

Cycle : ℕ → Set
Cycle n = List⁺ (Fin n)

Cycle* : ℕ → Set
Cycle* n = List (Cycle n)

-- Convert cycles to products of transpositions

cycle→transposition* : ∀ {n} → Cycle n → Transposition* n
cycle→transposition* c = mapL (mkTransposition (head c)) (reverse (ntail c))

cycle*→transposition* : ∀ {n} → Cycle* n → Transposition* n
cycle*→transposition* cs = concatMap cycle→transposition* cs

-- Convert from Cauchy representation to product of cycles

-- Helper that checks if there is a cycle that starts at i
-- Returns the cycle containing i and the rest of the permutation
-- without that cycle

findCycle : ∀ {n} → Fin n → Cycle* n →  Maybe (Cycle n × Cycle* n)
findCycle i [] = nothing
findCycle i (c ∷ cs) with toℕ i ≟ toℕ (head c)
findCycle i (c ∷ cs) | yes _ = just (c , cs)
findCycle i (c ∷ cs) | no _ =
  maybe′ (λ { (c' , cs') → just (c' , c ∷ cs') }) nothing (findCycle i cs)

-- Another helper that repeatedly tries to merge smaller cycles

{-# NO_TERMINATION_CHECK #-}
mergeCycles : ∀ {n} → Cycle* n → Cycle* n
mergeCycles [] = []
mergeCycles (c ∷ cs) with findCycle (last c) cs
mergeCycles (c ∷ cs) | nothing = c ∷ mergeCycles cs
mergeCycles (c ∷ cs) | just (c' , cs') = mergeCycles ((c ⁺++ ntail c') ∷ cs')

-- To convert a Cauchy representation to a product of cycles, just create
-- a cycle of size 2 for each entry and then merge the cycles

cauchy→cycle* : ∀ {n} → Cauchy n → Cycle* n
cauchy→cycle* {n} perm =
  mergeCycles
    (toList (zipWith (λ i j → i ∷⁺ Data.List.NonEmpty.[ j ]) (allFin n) perm))

-- Cauchy to product of transpostions

cauchy→transposition* : ∀ {n} → Cauchy n → Transposition* n
cauchy→transposition* = cycle*→transposition* ∘ cauchy→cycle*

------------------------------------------------------------------------------
-- Main functions

-- A permutation between t₁ and t₂ has three components in the Cauchy
-- representation: the map π of each element to a new position and a
-- proof that the sizes of the domain and range are the same and that
-- the map is injective.

TPermutation : U → U → Set
TPermutation t₁ t₂ = size t₁ ≡ size t₂ × Permutation (size t₁)

-- A view of (t : U) as normalized types.
-- Let size t be n then the normalized version of t is the type
-- (1 + (1 + (1 + (1 + ... 0)))) i.e. Fin n.

fromSize : ℕ → U
fromSize 0       = ZERO
fromSize (suc n) = PLUS ONE (fromSize n)

canonicalU : U → U
canonicalU = fromSize ∘ size

size+ : (n₁ n₂ : ℕ) → PLUS (fromSize n₁) (fromSize n₂) ⟷ fromSize (n₁ + n₂)
size+ 0        n₂ = unite₊
size+ (suc n₁) n₂ = assocr₊ ◎ (id⟷ ⊕ size+ n₁ n₂)

size* : (n₁ n₂ : ℕ) → TIMES (fromSize n₁) (fromSize n₂) ⟷ fromSize (n₁ * n₂)
size* 0        n₂ = absorbr
size* (suc n₁) n₂ = dist ◎ (unite⋆ ⊕ size* n₁ n₂) ◎ size+ n₂ (n₁ * n₂)

normalizeC : (t : U) → t ⟷ canonicalU t
normalizeC ZERO = id⟷
normalizeC ONE  = uniti₊ ◎ swap₊
normalizeC (PLUS t₀ t₁) =
  (normalizeC t₀ ⊕ normalizeC t₁) ◎ size+ (size t₀) (size t₁)
normalizeC (TIMES t₀ t₁) =
  (normalizeC t₀ ⊗ normalizeC t₁) ◎ size* (size t₀) (size t₁)

-- Given a normalized type Fin n and two indices 'a' and 'b' generate the code
-- to swap the two indices. Ex:
-- swapFin {3} "0" "1" should produce the permutation:
-- assocl₊ ◎ (swap₊ ⊕ id⟷) ◎ assocr₊ :
-- PLUS ONE (PLUS ONE (PLUS ONE ZERO)) ⟷ PLUS ONE (PLUS ONE (PLUS ONE ZERO))

swapFin : {n : ℕ} → (a b : Fin n) → (leq : toℕ a ≤ toℕ b) → fromSize n ⟷ fromSize n
swapFin zero zero z≤n = id⟷
swapFin zero (suc zero) z≤n = assocl₊ ◎ (swap₊ ⊕ id⟷) ◎ assocr₊
swapFin zero (suc (suc b)) z≤n =
  (assocl₊ ◎ (swap₊ ⊕ id⟷) ◎ assocr₊) ◎
  (id⟷ ⊕ swapFin zero (suc b) z≤n) ◎
  (assocl₊ ◎ (swap₊ ⊕ id⟷) ◎ assocr₊)
swapFin (suc a) zero ()
swapFin (suc a) (suc b) (s≤s leq) = id⟷ ⊕ swapFin a b leq

-- permutation to combinator

transposition*2c : (m n : ℕ) (m≡n : m ≡ n) → Transposition* m →
                   (fromSize m ⟷ fromSize n)
transposition*2c m n m≡n [] rewrite m≡n = id⟷
transposition*2c m n m≡n (_X_ i j {leq} ∷ π) rewrite m≡n =
  swapFin i j leq ◎ transposition*2c n n refl π

perm2c : {t₁ t₂ : U} → TPermutation t₁ t₂ → (t₁ ⟷ t₂)
perm2c {t₁} {t₂} (s₁≡s₂ , (π , inj)) =
  normalizeC t₁ ◎
  transposition*2c (size t₁) (size t₂) s₁≡s₂ (cauchy→transposition* π) ◎
  (! (normalizeC t₂))

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Example showing how the free monad construction on containers can be
-- used
------------------------------------------------------------------------

module README.Container.FreeMonad where

open import Category.Monad
open import Data.Empty
open import Data.Unit
open import Data.Bool
open import Data.Nat
open import Data.Sum using (inj₁; inj₂)
open import Data.Product renaming (_×_ to _⟨×⟩_)
open import Data.Container
open import Data.Container.Combinator
open import Data.Container.FreeMonad
open import Data.W
open import Relation.Binary.PropositionalEquality

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

-- The signature of state and its (generic) operations.

State : Set → Container _
State S = ⊤ ⟶ S ⊎ S ⟶ ⊤
  where
  _⟶_ : Set → Set → Container _
  I ⟶ O = I ▷ λ _ → O

get : ∀ {S} → State S ⋆ S
get = do (inj₁ _ , return)
  where
  open RawMonad rawMonad

put : ∀ {S} → S → State S ⋆ ⊤
put s = do (inj₂ s , return)
  where
  open RawMonad rawMonad

-- Using the above we can, for example, write a stateful program that
-- delivers a boolean.
prog : State ℕ ⋆ Bool
prog =
  get         >>= λ n →
  put (suc n) >>
  return true
  where
  open RawMonad rawMonad

runState : ∀ {S X} → State S ⋆ X → (S → X ⟨×⟩ S)
runState (sup (inj₁ x) _)        = λ s → x , s
runState (sup (inj₂ (inj₁ _)) k) = λ s → runState (k s) s
runState (sup (inj₂ (inj₂ s)) k) = λ _ → runState (k _) s

test : runState prog 0 ≡ true , 1
test = refl

-- It should be noted that @State S ⋆ X@ is not the state monad. If we
-- could quotient @State S ⋆ X@ by the seven axioms of state (see
-- Plotkin and Power's "Notions of Computation Determine Monads", 2002)
-- then we would get the state monad.


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

module Container.List where

open import Prelude
open import Data.Fin
open import Container

List : Type a → Type a
List = ⟦ ℕ , Fin ⟧

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
{-# OPTIONS --allow-unsolved-metas #-}

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

test : (x y : Nat) → x ≡ y → x ≡ 1 → y ≡ 1 → Nat
test (suc zero) (suc zero) refl refl refl = {!!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Prelude

module Implicits.Syntax where

open import Implicits.Syntax.Type public
open import Implicits.Syntax.Term public
open import Implicits.Syntax.Context public


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

module Cubical.Categories.Monoidal.Enriched where

open import Cubical.Categories.Monoidal.Base
open import Cubical.Foundations.Prelude

module _ {ℓV ℓV' : Level} (V : MonoidalCategory ℓV ℓV') (ℓE : Level) where

  open MonoidalCategory V
    renaming (ob to obV; Hom[_,_] to V[_,_]; id to idV; _⋆_ to _⋆V_)

  record EnrichedCategory : Type (ℓ-max (ℓ-max ℓV ℓV') (ℓ-suc ℓE)) where
    field
      ob : Type ℓE
      Hom[_,_] : ob → ob → obV
      id : ∀ {x} → V[ unit , Hom[ x , x ] ]
      seq : ∀ x y z → V[ Hom[ x , y ] ⊗ Hom[ y , z ] , Hom[ x , z ] ]

      -- Axioms
      ⋆IdL : ∀ x y →   η⟨ _ ⟩  ≡  (id {x} ⊗ₕ idV)  ⋆V  (seq x x y)
      ⋆IdR : ∀ x y →   ρ⟨ _ ⟩  ≡  (idV ⊗ₕ id {y})  ⋆V  (seq x y y)
      ⋆Assoc : ∀ x y z w →
          α⟨ _ , _ , _ ⟩  ⋆V  ((seq x y z) ⊗ₕ idV)  ⋆V  (seq x z w)
                          ≡  (idV ⊗ₕ (seq y z w))  ⋆V  (seq x y w)

-- TODO: define underlying category using Hom[ x , y ] := V[ unit , Hom[ x , y ] ]

max_stars_repo_name: FernandoLarrain/cubical


text:
{-

--{-# OPTIONS --allow-unsolved-metas #-}
--{-# OPTIONS -v 100 #-}

{- Yellow highlighting should be accompanied by an error message -}

{- By default, command-line agda reports "unsolved metas" and gives a source-code location, but no information about the nature of the unsolved metas. (Emacs agda gives only yellow-highlighting.). With  Without increasing verbosity (via "-v 100")  -}
postulate
  yellow-highlighting-but-no-error-message : Set _

{- --allow-unsolved-metas -}
{-
Running from the command-line, agda reports that there are unsolved metas but doesn't say anything about what they are. Is there a way to increase verbosity about the unsolved metas?
-}

postulate
  error-message-but-no-link-to-source-code-location : _ _
-}
postulate
  Σ : (A : Set) (B : A → Set) → Set
  X : Set

confusing-message--not-empty-type-of-sizes : Σ _ λ x → X
confusing-message--not-empty-type-of-sizes = {!!}


text:
------------------------------------------------------------------------------
-- Testing the non-internal ATP equality
------------------------------------------------------------------------------

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

module NonInternalEquality where

postulate D : Set

data _≡_ (x : D) : D → Set where
  refl : x ≡ x
{-# ATP axiom refl #-}

postulate foo : ∀ x → x ≡ x
{-# ATP prove foo #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


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

-- A Monad in a Bicategory.
-- For the more elementary version of Monads, see 'Categories.Monad'.
module Categories.Bicategory.Monad where

open import Level
open import Data.Product using (_,_)

open import Categories.Bicategory
import Categories.Bicategory.Extras as Bicat
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)

record Monad {o ℓ e t} (𝒞 : Bicategory o ℓ e t) : Set (o ⊔ ℓ ⊔ e ⊔ t) where
  open Bicat 𝒞

  field
    C : Obj
    T : C ⇒₁ C
    η : id₁ ⇒₂ T
    μ : (T ⊚₀ T) ⇒₂ T

    assoc     : μ ∘ᵥ (T ▷ μ) ∘ᵥ associator.from ≈ (μ ∘ᵥ (μ ◁ T))
    sym-assoc : μ ∘ᵥ (μ ◁ T) ∘ᵥ associator.to ≈ (μ ∘ᵥ (T ▷ μ))
    identityˡ : μ ∘ᵥ (T ▷ η) ∘ᵥ unitorʳ.to ≈ id₂
    identityʳ : μ ∘ᵥ (η ◁ T) ∘ᵥ unitorˡ.to ≈ id₂

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

open import lib.Basics
-- open import lib.NType2
-- open import lib.PathGroupoid

open import lib.types.Bool
open import lib.types.IteratedSuspension
open import lib.types.Lift
open import lib.types.LoopSpace
open import lib.types.Nat
open import lib.types.Paths
open import lib.types.Pi
open import lib.types.Pointed
open import lib.types.Sigma
open import lib.types.Suspension
open import lib.types.TLevel
open import lib.types.Unit

module nicolai.pseudotruncations.Preliminary-definitions where

-- definition of weak constancy
wconst : ∀ {i j} {A : Type i} {B : Type j} → (A → B) → Type (lmax i j)
wconst {A = A} f = (a₁ a₂ : A) → f a₁ == f a₂

{- Pointed maps (without the 'point') -}
_→̇_ : ∀ {i j} (Â : Ptd i) (B̂ : Ptd j) → Type _
Â →̇ B̂ = fst (Â ⊙→ B̂)

{- It is useful to have a lemma which allows to construct equalities
   between pointed types. Of course, we know that such an equality
   is a pair of equalities; however, transporting a function can
   make things more tedious than necessary! -}
make-=-∙ : ∀ {i j} {Â : Ptd i} {B̂ : Ptd j} (f̂ ĝ : Â →̇ B̂)
           (p : fst f̂ == fst ĝ)
           → ! (app= p (snd Â)) ∙ snd f̂ == snd ĝ
           → f̂ == ĝ
make-=-∙ (f , p) (.f , q) idp t = pair= idp t

{- A lemma that allows to prove that the value of a map between
   pointed maps, at some given point, is some given point.
   This would otherwise be an involved nesting of transports/
   PathOvers. -}
→̇-maps-to : ∀ {i} {Â B̂ Ĉ D̂ : Ptd i} (F̂ : (Â →̇ B̂) → (Ĉ →̇ D̂))
              (f̂ : Â →̇ B̂) (ĝ : Ĉ →̇ D̂)
              (p : fst (F̂ f̂) == (fst ĝ))
              (q : (app= p (snd Ĉ)) ∙ (snd ĝ) == snd (F̂ f̂))
              → F̂ f̂ == ĝ
→̇-maps-to F̂ f̂ (.(fst (F̂ f̂)) , .(snd (F̂ f̂))) idp idp = idp

{- Also trivial: make pointed equivalences from an ordinary equality -}
coe-equiv∙ : ∀ {i} {Â B̂ : Ptd i} → (Â == B̂) → Â ⊙≃ B̂
coe-equiv∙ idp = (idf _ , idp) , idf-is-equiv _

module _ {i} where

  {- Of course, spheres are defined in the library.
     Unfortunately, they do not play well together with iterated suspension.
     If f is an endofunction, one can define [f^Sn] either as [f^n ∘ f] or as
     [f ∘ f^n]. It turns out that it is much more convenient if one chooses
     different possibilites for Ω and for Σ (suspension), as the adjunction
     can then be handled much more directly.
     In summary: It's best to redefine spheres. -}

  ⊙Susp-iter' : (n : ℕ) (Â : Ptd i) → Ptd i
  ⊙Susp-iter' O Â = Â
  ⊙Susp-iter' (S n) Â = ⊙Susp-iter' n (⊙Susp Â)

  {- compare: definition of iterated Ω
    ⊙Ω-iter : (n : ℕ) (Â : Ptd i) → Ptd i
    ⊙Ω-iter O Â = Â
    ⊙Ω-iter (S n) Â = ⊙Ω (⊙Ω-iter n Â)
  -}

  ⊙Sphere' : (n : ℕ) → Ptd i
  ⊙Sphere' n = ⊙Susp-iter' n (⊙Lift ⊙Bool)

  Sphere' : (n : ℕ) → Type i
  Sphere' = fst ∘ ⊙Sphere'

  nor' : (n : ℕ) → Sphere' n
  nor' = snd ∘ ⊙Sphere'

  {- Unfortunately, we will sometimes still need the "other" behaviour of the sphere.
     Thus, we show at least the following: -}

  ⊙Susp-iter : (n : ℕ) (Â : Ptd i) → Ptd i
  ⊙Susp-iter O Â = Â
  ⊙Susp-iter (S n) Â = ⊙Susp (⊙Susp-iter n Â)

  ⊙Sphere* : (n : ℕ) → Ptd i
  ⊙Sphere* n = ⊙Susp-iter n (⊙Lift ⊙Bool)

  Sphere* : (n : ℕ) → Type i
  Sphere* = fst ∘ ⊙Sphere*

  {- Of course, this proof could be done for all endofunctions. -}
  susp-iter= : (n : ℕ) (Â : Ptd i) → ⊙Susp-iter' n Â == ⊙Susp-iter n Â
  susp-iter= O Â = idp
  susp-iter= (S O) Â = idp
  susp-iter= (S (S n)) Â =
    ⊙Susp-iter' (S (S n)) Â
      =⟨ susp-iter= (S n) (⊙Susp Â) ⟩
    ⊙Susp (⊙Susp-iter n (⊙Susp Â))
      =⟨ ap ⊙Susp (! (susp-iter= n (⊙Susp Â))) ⟩
    ⊙Susp (⊙Susp-iter' (S n) Â)
      =⟨ ap ⊙Susp (susp-iter= (S n) Â) ⟩
    ⊙Susp-iter (S (S n)) Â
      ∎

  {- Thus, we have for the spheres: -}
  ⊙Spheres= : (n : ℕ) → ⊙Sphere' n == ⊙Sphere* n
  ⊙Spheres= n = susp-iter= n (⊙Lift ⊙Bool)

  Spheres= : (n : ℕ) → Sphere' n == Sphere* n
  Spheres= n = ap fst (⊙Spheres= n)

  {- Also, we have this: -}
  susp'-switch : (n : ℕ) → ⊙Sphere' (S n) == ⊙Susp (⊙Sphere' n)
  susp'-switch n = (⊙Spheres= (S n)) ∙ (ap ⊙Susp (! (⊙Spheres= n)))

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
-- Andreas, Bentfest 2016-04-28 Marsstrand
-- Issue 1944: also resolve overloaded projections in checking position

module _ (A : Set) (a : A) where

record R B : Set where
  field f : B
open R

record S B : Set where
  field f : B
open S

test : ∀{A : Set} → A → A
test = f
-- Expected error:
-- Cannot resolve overloaded projection f because first visible
-- argument is not of record type
-- when checking that the expression f has type .A → .A

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


text:
open import Relation.Binary using (Rel)
open import Algebra.Bundles using (CommutativeRing)

open import Algebra.Module.Normed

module Algebra.Module.Limit.Compose
  {r ℓr} {CR : CommutativeRing r ℓr}
  (open CommutativeRing CR using () renaming (Carrier to X))
  {rel} {_≤_ : Rel X rel}
  {ma ℓma} (MA : NormedModule CR _≤_ ma ℓma)
  {mb ℓmb} (MB : NormedModule CR _≤_ mb ℓmb)
  {mc ℓmc} (MC : NormedModule CR _≤_ mc ℓmc)
  where

open import Data.Product using (_,_)
open import Function using (_∘_)

open CommutativeRing CR
open import Assume using (assume)

import Algebra.Module.Limit as Limit

open Limit MA MB using () renaming
  ( _DifferentiableAt_ to _DifferentiableAt₁₂_
  ; Differentiable to Differentiable₁₂
  )

open Limit MB MC using () renaming
  (_DifferentiableAt_ to _DifferentiableAt₂₃_
  ; Differentiable to Differentiable₂₃
  )

open Limit MA MC using () renaming
  (_DifferentiableAt_ to _DifferentiableAt₁₃_
  ; Differentiable to Differentiable₁₃
  )

private
  module MA = NormedModule MA
  module MB = NormedModule MB
  module MC = NormedModule MC

∘-differentiable-at : ∀ {g f x} → g DifferentiableAt₂₃ (f x) → f DifferentiableAt₁₂ x → (g ∘ f) DifferentiableAt₁₃ x
∘-differentiable-at {g} {f} {x} (Dg , _) (Df , _) = (Dg ∘ Df) , assume

∘-differentiable : ∀ {g f} → Differentiable₂₃ g → Differentiable₁₂ f → Differentiable₁₃ (g ∘ f)
∘-differentiable {g} {f} diff-g diff-f = λ x → ∘-differentiable-at {g} {f} {x} (diff-g (f x)) (diff-f x)

max_stars_repo_name: cspollard/reals

max_issues_repo_name: cspollard/reals

max_forks_repo_name: cspollard/reals


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

module Data.Binary.Addition.Properties where

open import Prelude
open import Data.Binary.Definition
open import Data.Binary.Addition
open import Data.Binary.Conversion
import Data.Nat as ℕ
import Data.Nat.Properties as ℕ
open import Path.Reasoning
open import Data.Binary.Isomorphism

+-cong : ∀ xs ys → ⟦ xs + ys ⇓⟧ ≡ ⟦ xs ⇓⟧ ℕ.+ ⟦ ys ⇓⟧
add₁-cong : ∀ xs ys → ⟦ add₁ xs ys ⇓⟧ ≡ 1 ℕ.+ ⟦ xs ⇓⟧ ℕ.+ ⟦ ys ⇓⟧
add₂-cong : ∀ xs ys → ⟦ add₂ xs ys ⇓⟧ ≡ 2 ℕ.+ ⟦ xs ⇓⟧ ℕ.+ ⟦ ys ⇓⟧

lemma₁ : ∀ xs ys → ⟦ add₁ xs ys ⇓⟧ ℕ.* 2 ≡ ⟦ xs ⇓⟧ ℕ.* 2 ℕ.+ (2 ℕ.+ ⟦ ys ⇓⟧ ℕ.* 2)
lemma₁ xs ys =
  ⟦ add₁ xs ys ⇓⟧ ℕ.* 2 ≡⟨ cong (ℕ._* 2) (add₁-cong xs ys) ⟩
  2 ℕ.+ (⟦ xs ⇓⟧ ℕ.+ ⟦ ys ⇓⟧) ℕ.* 2 ≡⟨ cong (2 ℕ.+_ ) (ℕ.+-*-distrib ⟦ xs ⇓⟧ ⟦ ys ⇓⟧ 2) ⟩
  2 ℕ.+ ⟦ xs ⇓⟧ ℕ.* 2 ℕ.+ ⟦ ys ⇓⟧ ℕ.* 2 ≡⟨ cong (ℕ._+ (⟦ ys ⇓⟧ ℕ.* 2)) (ℕ.+-comm 2 (⟦ xs ⇓⟧ ℕ.* 2)) ⟩
  ⟦ xs ⇓⟧ ℕ.* 2 ℕ.+ 2 ℕ.+ ⟦ ys ⇓⟧ ℕ.* 2 ≡⟨ ℕ.+-assoc (⟦ xs ⇓⟧ ℕ.* 2) 2 (⟦ ys ⇓⟧ ℕ.* 2) ⟩
  ⟦ xs ⇓⟧ ℕ.* 2 ℕ.+ (2 ℕ.+ ⟦ ys ⇓⟧ ℕ.* 2) ∎

lemma₂ : ∀ xs ys → ⟦ add₁ xs ys ⇓⟧ ℕ.* 2 ≡ (1 ℕ.+ ⟦ xs ⇓⟧ ℕ.* 2) ℕ.+ (1 ℕ.+ ⟦ ys ⇓⟧ ℕ.* 2)
lemma₂ xs ys =
  ⟦ add₁ xs ys ⇓⟧ ℕ.* 2 ≡⟨ cong (ℕ._* 2) (add₁-cong xs ys) ⟩
  (1 ℕ.+ ⟦ xs ⇓⟧ ℕ.+ ⟦ ys ⇓⟧) ℕ.* 2 ≡⟨ ℕ.+-*-distrib (1 ℕ.+ ⟦ xs ⇓⟧) ⟦ ys ⇓⟧ 2 ⟩
  2 ℕ.+ ⟦ xs ⇓⟧ ℕ.* 2 ℕ.+ ⟦ ys ⇓⟧ ℕ.* 2 ≡˘⟨ ℕ.+-suc (1 ℕ.+ ⟦ xs ⇓⟧ ℕ.* 2) (⟦ ys ⇓⟧ ℕ.* 2) ⟩
  (1 ℕ.+ ⟦ xs ⇓⟧ ℕ.* 2) ℕ.+ (1 ℕ.+ ⟦ ys ⇓⟧ ℕ.* 2) ∎

lemma₃ : ∀ xs ys → ⟦ add₂ xs ys ⇓⟧ ℕ.* 2 ≡ suc (suc (⟦ xs ⇓⟧ ℕ.* 2 ℕ.+ suc (suc (⟦ ys ⇓⟧ ℕ.* 2))))
lemma₃ xs ys =
  ⟦ add₂ xs ys ⇓⟧ ℕ.* 2 ≡⟨ cong (ℕ._* 2) (add₂-cong xs ys) ⟩
  (2 ℕ.+ ⟦ xs ⇓⟧ ℕ.+ ⟦ ys ⇓⟧) ℕ.* 2 ≡˘⟨ cong (ℕ._* 2) (ℕ.+-suc (1 ℕ.+ ⟦ xs ⇓⟧) ⟦ ys ⇓⟧) ⟩
  ((1 ℕ.+ ⟦ xs ⇓⟧) ℕ.+ (1 ℕ.+ ⟦ ys ⇓⟧)) ℕ.* 2 ≡⟨ ℕ.+-*-distrib (1 ℕ.+ ⟦ xs ⇓⟧) (1 ℕ.+ ⟦ ys ⇓⟧) 2 ⟩
  suc (suc (⟦ xs ⇓⟧ ℕ.* 2 ℕ.+ suc (suc (⟦ ys ⇓⟧ ℕ.* 2)))) ∎

add₁-cong 0ᵇ ys = inc-suc ys
add₁-cong (1ᵇ xs) 0ᵇ = cong (2 ℕ.+_) (sym (ℕ.+-idʳ (⟦ xs ⇓⟧ ℕ.* 2)))
add₁-cong (2ᵇ xs) 0ᵇ = cong suc (cong (ℕ._* 2) (inc-suc xs) ; cong (2 ℕ.+_) (sym (ℕ.+-idʳ (⟦ xs ⇓⟧ ℕ.* 2))))
add₁-cong (1ᵇ xs) (1ᵇ ys) = cong suc (lemma₂ xs ys)
add₁-cong (1ᵇ xs) (2ᵇ ys) = cong (2 ℕ.+_) (lemma₁ xs ys)
add₁-cong (2ᵇ xs) (1ᵇ ys) = cong (2 ℕ.+_) (lemma₂ xs ys)
add₁-cong (2ᵇ xs) (2ᵇ ys) = cong (1 ℕ.+_) (lemma₃ xs ys)

add₂-cong 0ᵇ 0ᵇ = refl
add₂-cong 0ᵇ (1ᵇ ys) = cong (1 ℕ.+_) (cong (ℕ._* 2) (inc-suc ys))
add₂-cong 0ᵇ (2ᵇ ys) = cong (2 ℕ.+_) (cong (ℕ._* 2) (inc-suc ys))
add₂-cong (1ᵇ xs) 0ᵇ = cong (1 ℕ.+_) ((cong (ℕ._* 2) (inc-suc xs)) ; cong (2 ℕ.+_) (sym (ℕ.+-idʳ _)))
add₂-cong (2ᵇ xs) 0ᵇ = cong (2 ℕ.+_) ((cong (ℕ._* 2) (inc-suc xs)) ; cong (2 ℕ.+_) (sym (ℕ.+-idʳ _)))
add₂-cong (1ᵇ xs) (1ᵇ ys) = cong (2 ℕ.+_ ) (lemma₂ xs ys)
add₂-cong (1ᵇ xs) (2ᵇ ys) = cong (1 ℕ.+_) (lemma₃ xs ys)
add₂-cong (2ᵇ xs) (1ᵇ ys) = cong (1 ℕ.+_) (lemma₃ xs ys ; ℕ.+-suc (2 ℕ.+ ⟦ xs ⇓⟧ ℕ.* 2) (1 ℕ.+ ⟦ ys ⇓⟧ ℕ.* 2))
add₂-cong (2ᵇ xs) (2ᵇ ys) = cong (2 ℕ.+_) (lemma₃ xs ys)

+-cong 0ᵇ ys = refl
+-cong (1ᵇ xs) 0ᵇ = cong suc (sym (ℕ.+-idʳ (⟦ xs ⇓⟧ ℕ.* 2)))
+-cong (2ᵇ xs) 0ᵇ = cong (suc ∘ suc) (sym (ℕ.+-idʳ (⟦ xs ⇓⟧ ℕ.* 2)))
+-cong (1ᵇ xs) (1ᵇ ys) =
  2 ℕ.+ ⟦ xs + ys ⇓⟧ ℕ.* 2 ≡⟨ cong (λ xy → 2 ℕ.+ xy ℕ.* 2) (+-cong xs ys) ⟩
  2 ℕ.+ (⟦ xs ⇓⟧ ℕ.+ ⟦ ys ⇓⟧) ℕ.* 2 ≡⟨ cong (2 ℕ.+_) (ℕ.+-*-distrib ⟦ xs ⇓⟧ ⟦ ys ⇓⟧ 2) ⟩
  2 ℕ.+ (⟦ xs ⇓⟧ ℕ.* 2 ℕ.+ ⟦ ys ⇓⟧ ℕ.* 2) ≡˘⟨ cong suc (ℕ.+-suc (⟦ xs ⇓⟧ ℕ.* 2) (⟦ ys ⇓⟧ ℕ.* 2)) ⟩
  1 ℕ.+ ⟦ xs ⇓⟧ ℕ.* 2 ℕ.+ (1 ℕ.+ ⟦ ys ⇓⟧ ℕ.* 2) ∎
+-cong (1ᵇ xs) (2ᵇ ys) = cong suc (lemma₁ xs ys)
+-cong (2ᵇ xs) (1ᵇ ys) = cong suc (lemma₂ xs ys)
+-cong (2ᵇ xs) (2ᵇ ys) = cong (2 ℕ.+_) (lemma₁ xs ys)

+-cong˘ : ∀ xs ys → ⟦ xs ℕ.+ ys ⇑⟧ ≡ ⟦ xs ⇑⟧ + ⟦ ys ⇑⟧
+-cong˘ xs ys =
  ⟦ xs ℕ.+ ys ⇑⟧ ≡˘⟨ cong ⟦_⇑⟧ (cong₂ ℕ._+_ (𝔹-rightInv xs) (𝔹-rightInv ys)) ⟩
  ⟦ ⟦ ⟦ xs ⇑⟧ ⇓⟧ ℕ.+ ⟦ ⟦ ys ⇑⟧ ⇓⟧ ⇑⟧ ≡˘⟨ cong ⟦_⇑⟧ (+-cong ⟦ xs ⇑⟧ ⟦ ys ⇑⟧) ⟩
  ⟦ ⟦ ⟦ xs ⇑⟧ + ⟦ ys ⇑⟧ ⇓⟧ ⇑⟧ ≡⟨ 𝔹-leftInv (⟦ xs ⇑⟧ + ⟦ ys ⇑⟧) ⟩
  ⟦ xs ⇑⟧ + ⟦ ys ⇑⟧ ∎


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of operations on the Delay type
------------------------------------------------------------------------

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

module Codata.Delay.Properties where

open import Size
import Data.Sum as Sum
open import Codata.Thunk using (Thunk; force)
open import Codata.Conat
open import Codata.Conat.Bisimilarity as Coℕ using (zero ; suc)
open import Codata.Delay
open import Codata.Delay.Bisimilarity
open import Function
open import Relation.Binary.PropositionalEquality as Eq using (_≡_)

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

 length-never : ∀ {i} → i Coℕ.⊢ length (never {A = A}) ≈ infinity
 length-never = suc λ where .force → length-never

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

 length-map : ∀ (f : A → B) da {i} → i Coℕ.⊢ length (map f da) ≈ length da
 length-map f (now a)    = zero
 length-map f (later da) = suc λ where .force → length-map f (da .force)

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

 length-zipWith : ∀ (f : A → B → C) da db {i} →
   i Coℕ.⊢ length (zipWith f da db) ≈ length da ⊔ length db
 length-zipWith f (now a)      db         = length-map (f a) db
 length-zipWith f da@(later _) (now b)    = length-map (λ a → f a b) da
 length-zipWith f (later da)   (later db) =
   suc λ where .force →  length-zipWith f (da .force) (db .force)

 map-map-fusion : ∀ (f : A → B) (g : B → C) da {i}  →
   i ⊢ map g (map f da) ≈ map (g ∘′ f) da
 map-map-fusion f g (now a)    = now Eq.refl
 map-map-fusion f g (later da) = later λ where .force → map-map-fusion f g (da .force)

 map-unfold-fusion : ∀ (f : B → C) n (s : A) {i} →
   i ⊢ map f (unfold n s) ≈ unfold (Sum.map id f ∘′ n) s
 map-unfold-fusion f n s with n s
 ... | Sum.inj₁ s′ = later λ where .force → map-unfold-fusion f n s′
 ... | Sum.inj₂ b  = now Eq.refl


text:
------------------------------------------------------------------------
-- Helpers intended to ease the development of "tactics" which use
-- proof by reflection
------------------------------------------------------------------------

open import Relation.Binary
open import Data.Nat
open import Data.Fin
open import Data.Vec as Vec
open import Data.Function

-- Think of the parameters as follows:
--
-- * Expr:    A representation of code.
-- * var:     The Expr type should support a notion of variables.
-- * ⟦_⟧:     Computes the semantics of an expression. Takes an
--            environment mapping variables to something.
-- * ⟦_⇓⟧:    Computes the semantics of the normal form of the
--            expression.
-- * correct: Normalisation preserves the semantics.
--
-- Given these parameters two "tactics" are returned, prove and solve.
--
-- For an example of the use of this module, see Algebra.RingSolver.

module Relation.Binary.Reflection
         {Expr : ℕ → Set} {A}
         Sem
         (var : ∀ {n} → Fin n → Expr n)
         (⟦_⟧ ⟦_⇓⟧ : ∀ {n} → Expr n → Vec A n → Setoid.carrier Sem)
         (correct : ∀ {n} (e : Expr n) ρ →
                    ⟦ e ⇓⟧ ρ ⟨ Setoid._≈_ Sem ⟩₁ ⟦ e ⟧ ρ)
         where

open import Data.Vec.N-ary
open import Data.Product
import Relation.Binary.EqReasoning as Eq

open Setoid Sem
open Eq Sem

-- If two normalised expressions are semantically equal, then their
-- non-normalised forms are also equal.

prove : ∀ {n} (ρ : Vec A n) e₁ e₂ →
        ⟦ e₁ ⇓⟧ ρ ≈ ⟦ e₂ ⇓⟧ ρ →
        ⟦ e₁  ⟧ ρ ≈ ⟦ e₂  ⟧ ρ
prove ρ e₁ e₂ hyp = begin
  ⟦ e₁  ⟧ ρ ≈⟨ sym (correct e₁ ρ) ⟩
  ⟦ e₁ ⇓⟧ ρ ≈⟨ hyp ⟩
  ⟦ e₂ ⇓⟧ ρ ≈⟨ correct e₂ ρ ⟩
  ⟦ e₂  ⟧ ρ ∎

-- Applies the function to all possible "variables".

close : ∀ {A} n → N-ary n (Expr n) A → A
close n f = f $ⁿ Vec.map var (allFin n)

-- A variant of prove which should in many cases be easier to use,
-- because variables and environments are handled in a less explicit
-- way.
--
-- If the type signature of solve is a bit daunting, then it may be
-- helpful to instantiate n with a small natural number and normalise
-- the remainder of the type.

solve : ∀ n (f : N-ary n (Expr n) (Expr n × Expr n)) →
  Eqʰ n _≈_ (curryⁿ ⟦ proj₁ (close n f) ⇓⟧) (curryⁿ ⟦ proj₂ (close n f) ⇓⟧) →
  Eq  n _≈_ (curryⁿ ⟦ proj₁ (close n f)  ⟧) (curryⁿ ⟦ proj₂ (close n f)  ⟧)
solve n f hyp =
  curryⁿ-pres ⟦ proj₁ (close n f) ⟧ ⟦ proj₂ (close n f) ⟧
    (λ ρ → prove ρ (proj₁ (close n f)) (proj₂ (close n f))
             (curryⁿ-pres⁻¹ ⟦ proj₁ (close n f) ⇓⟧ ⟦ proj₂ (close n f) ⇓⟧
                            (Eqʰ-to-Eq n hyp) ρ))

-- A variant of _,_ which is intended to make uses of solve look a
-- bit nicer.

infix 4 _⊜_

_⊜_ : ∀ {A} → A → A → A × A
_⊜_ = _,_

max_issues_repo_name: larrytheliquid/Lemmachine


text:
postulate
  T : Set → Set
  _>>=_ : ∀ {A B} → T A → (A → T B) → T B

argh : ∀ {A} → T A → T A
argh ta = do
  f x ← ta
  {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Common.Nat where

open import Agda.Builtin.Nat public
  using    ( Nat; zero; suc; _+_; _*_ )
  renaming ( _-_ to _∸_ )

{-# COMPILED_JS Nat function (x,v) { return (x < 1? v.zero(): v.suc(x-1)); } #-}
{-# COMPILED_JS zero 0 #-}
{-# COMPILED_JS suc function (x) { return x+1; } #-}

{-# COMPILED_JS _+_ function (x) { return function (y) { return x+y; }; } #-}
{-# COMPILED_JS _*_ function (x) { return function (y) { return x*y; }; } #-}
{-# COMPILED_JS _∸_ function (x) { return function (y) { return Math.max(0,x-y); }; } #-}

pred : Nat → Nat
pred zero    = zero
pred (suc n) = n


text:
-- You can have infix declarations in records.

module InfixRecordFields where

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

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

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

one = suc zero
two = suc (suc zero)

record A : Set where
  field x   : Nat
        _*_ : Nat -> Nat -> Nat
        h   : (one + one * x) == one  -- later fields make use of the fixity
  infixl 60 _*_

a : A
a = record { x = zero; _*_ = \ x y -> y; h = refl }

open module X = A a

-- The projection functions also have the right fixity.
p : (one + one * zero) == one
p = refl


text:
{-# OPTIONS --rewriting --confluence-check #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

data Unit : Set where ∗ : Unit

postulate
  A : Set
  a b c : Unit → A
  a→b : a ∗ ≡ b ∗
  a→c : ∀ x → a x ≡ c x
  b→c : b ∗ ≡ c ∗

{-# REWRITE a→b a→c b→c #-}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Solver for commutative ring or semiring equalities
------------------------------------------------------------------------

-- Uses ideas from the Coq ring tactic. See "Proving Equalities in a
-- Commutative Ring Done Right in Coq" by Grégoire and Mahboubi. The
-- code below is not optimised like theirs, though (in particular, our
-- Horner normal forms are not sparse).
--
-- At first the `WeaklyDecidable` type may at first glance look useless
-- as there is no guarantee that it doesn't always return `nothing`.
-- However the implementation of it affects the power of the solver. The
-- more equalities it returns, the more expressions the ring solver can
-- solve.

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

open import Algebra
open import Algebra.Solver.Ring.AlmostCommutativeRing
open import Relation.Binary.Core using (WeaklyDecidable)

module Algebra.Solver.Ring
  {r₁ r₂ r₃}
  (Coeff : RawRing r₁)               -- Coefficient "ring".
  (R : AlmostCommutativeRing r₂ r₃)  -- Main "ring".
  (morphism : Coeff -Raw-AlmostCommutative⟶ R)
  (_coeff≟_ : WeaklyDecidable (Induced-equivalence morphism))
  where

open import Algebra.Solver.Ring.Lemmas Coeff R morphism
private module C = RawRing Coeff
open AlmostCommutativeRing R
  renaming (zero to *-zero; zeroˡ to *-zeroˡ; zeroʳ to *-zeroʳ)
open import Algebra.FunctionProperties _≈_
open import Algebra.Morphism
open _-Raw-AlmostCommutative⟶_ morphism renaming (⟦_⟧ to ⟦_⟧′)
open import Algebra.Operations.Semiring semiring

open import Relation.Binary
open import Relation.Nullary using (yes; no)
open import Relation.Binary.Reasoning.Setoid setoid
import Relation.Binary.PropositionalEquality as PropEq
import Relation.Binary.Reflection as Reflection

open import Data.Nat.Base using (ℕ; suc; zero)
open import Data.Fin using (Fin; zero; suc)
open import Data.Vec using (Vec; []; _∷_; lookup)
open import Data.Maybe.Base using (just; nothing)
open import Function
open import Level using (_⊔_)

infix  9 :-_ -H_ -N_
infixr 9 _:×_ _:^_ _^N_
infix  8 _*x+_ _*x+HN_ _*x+H_
infixl 8 _:*_ _*N_ _*H_ _*NH_ _*HN_
infixl 7 _:+_ _:-_ _+H_ _+N_
infix  4 _≈H_ _≈N_

------------------------------------------------------------------------
-- Polynomials

data Op : Set where
  [+] : Op
  [*] : Op

-- The polynomials are indexed by the number of variables.

data Polynomial (m : ℕ) : Set r₁ where
  op   : (o : Op) (p₁ : Polynomial m) (p₂ : Polynomial m) → Polynomial m
  con  : (c : C.Carrier) → Polynomial m
  var  : (x : Fin m) → Polynomial m
  _:^_ : (p : Polynomial m) (n : ℕ) → Polynomial m
  :-_  : (p : Polynomial m) → Polynomial m

-- Short-hand notation.

_:+_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n
_:+_ = op [+]

_:*_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n
_:*_ = op [*]

_:-_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n
x :- y = x :+ :- y

_:×_ : ∀ {n} → ℕ → Polynomial n → Polynomial n
zero :× p = con C.0#
suc m :× p = p :+ m :× p

-- Semantics.

sem : Op → Op₂ Carrier
sem [+] = _+_
sem [*] = _*_

⟦_⟧ : ∀ {n} → Polynomial n → Vec Carrier n → Carrier
⟦ op o p₁ p₂ ⟧ ρ = ⟦ p₁ ⟧ ρ ⟨ sem o ⟩ ⟦ p₂ ⟧ ρ
⟦ con c      ⟧ ρ = ⟦ c ⟧′
⟦ var x      ⟧ ρ = lookup ρ x
⟦ p :^ n     ⟧ ρ = ⟦ p ⟧ ρ ^ n
⟦ :- p       ⟧ ρ = - ⟦ p ⟧ ρ

------------------------------------------------------------------------
-- Normal forms of polynomials

-- A univariate polynomial of degree d,
--
--     p = a_d x^d + a_{d-1}x^{d-1} + … + a_0,
--
-- is represented in Horner normal form by
--
--     p = ((a_d x + a_{d-1})x + …)x + a_0.
--
-- Note that Horner normal forms can be represented as lists, with the
-- empty list standing for the zero polynomial of degree "-1".
--
-- Given this representation of univariate polynomials over an
-- arbitrary ring, polynomials in any number of variables over the
-- ring C can be represented via the isomorphisms
--
--     C[] ≅ C
--
-- and
--
--     C[X_0,...X_{n+1}] ≅ C[X_0,...,X_n][X_{n+1}].

mutual

  -- The polynomial representations are indexed by the polynomial's
  -- degree.

  data HNF : ℕ → Set r₁ where
    ∅     : ∀ {n} → HNF (suc n)
    _*x+_ : ∀ {n} → HNF (suc n) → Normal n → HNF (suc n)

  data Normal : ℕ → Set r₁ where
    con  : C.Carrier → Normal zero
    poly : ∀ {n} → HNF (suc n) → Normal (suc n)

  -- Note that the data types above do /not/ ensure uniqueness of
  -- normal forms: the zero polynomial of degree one can be
  -- represented using both ∅ and ∅ *x+ con C.0#.

mutual

  -- Semantics.

  ⟦_⟧H : ∀ {n} → HNF (suc n) → Vec Carrier (suc n) → Carrier
  ⟦ ∅       ⟧H _       = 0#
  ⟦ p *x+ c ⟧H (x ∷ ρ) = ⟦ p ⟧H (x ∷ ρ) * x + ⟦ c ⟧N ρ

  ⟦_⟧N : ∀ {n} → Normal n → Vec Carrier n → Carrier
  ⟦ con c  ⟧N _ = ⟦ c ⟧′
  ⟦ poly p ⟧N ρ = ⟦ p ⟧H ρ

------------------------------------------------------------------------
-- Equality and decidability

mutual

  -- Equality.

  data _≈H_ : ∀ {n} → HNF n → HNF n → Set (r₁ ⊔ r₃) where
    ∅     : ∀ {n} → _≈H_ {suc n} ∅ ∅
    _*x+_ : ∀ {n} {p₁ p₂ : HNF (suc n)} {c₁ c₂ : Normal n} →
            p₁ ≈H p₂ → c₁ ≈N c₂ → (p₁ *x+ c₁) ≈H (p₂ *x+ c₂)

  data _≈N_ : ∀ {n} → Normal n → Normal n → Set (r₁ ⊔ r₃) where
    con  : ∀ {c₁ c₂} → ⟦ c₁ ⟧′ ≈ ⟦ c₂ ⟧′ → con c₁ ≈N con c₂
    poly : ∀ {n} {p₁ p₂ : HNF (suc n)} → p₁ ≈H p₂ → poly p₁ ≈N poly p₂

mutual

  -- Equality is weakly decidable.

  _≟H_ : ∀ {n} → WeaklyDecidable (_≈H_ {n = n})
  ∅           ≟H ∅           = just ∅
  ∅           ≟H (_ *x+ _)   = nothing
  (_ *x+ _)   ≟H ∅           = nothing
  (p₁ *x+ c₁) ≟H (p₂ *x+ c₂) with p₁ ≟H p₂ | c₁ ≟N c₂
  ... | just p₁≈p₂ | just c₁≈c₂ = just (p₁≈p₂ *x+ c₁≈c₂)
  ... | _          | nothing    = nothing
  ... | nothing    | _          = nothing

  _≟N_ : ∀ {n} → WeaklyDecidable (_≈N_ {n = n})
  con c₁ ≟N con c₂ with c₁ coeff≟ c₂
  ... | just c₁≈c₂ = just (con c₁≈c₂)
  ... | nothing    = nothing
  poly p₁ ≟N poly p₂ with p₁ ≟H p₂
  ... | just p₁≈p₂ = just (poly p₁≈p₂)
  ... | nothing    = nothing

mutual

  -- The semantics respect the equality relations defined above.

  ⟦_⟧H-cong : ∀ {n} {p₁ p₂ : HNF (suc n)} →
              p₁ ≈H p₂ → ∀ ρ → ⟦ p₁ ⟧H ρ ≈ ⟦ p₂ ⟧H ρ
  ⟦ ∅               ⟧H-cong _       = refl
  ⟦ p₁≈p₂ *x+ c₁≈c₂ ⟧H-cong (x ∷ ρ) =
    (⟦ p₁≈p₂ ⟧H-cong (x ∷ ρ) ⟨ *-cong ⟩ refl)
      ⟨ +-cong ⟩
    ⟦ c₁≈c₂ ⟧N-cong ρ

  ⟦_⟧N-cong :
    ∀ {n} {p₁ p₂ : Normal n} →
    p₁ ≈N p₂ → ∀ ρ → ⟦ p₁ ⟧N ρ ≈ ⟦ p₂ ⟧N ρ
  ⟦ con c₁≈c₂  ⟧N-cong _ = c₁≈c₂
  ⟦ poly p₁≈p₂ ⟧N-cong ρ = ⟦ p₁≈p₂ ⟧H-cong ρ

------------------------------------------------------------------------
-- Ring operations on Horner normal forms

-- Zero.

0H : ∀ {n} → HNF (suc n)
0H = ∅

0N : ∀ {n} → Normal n
0N {zero}  = con C.0#
0N {suc n} = poly 0H

mutual

  -- One.

  1H : ∀ {n} → HNF (suc n)
  1H {n} = ∅ *x+ 1N {n}

  1N : ∀ {n} → Normal n
  1N {zero}  = con C.1#
  1N {suc n} = poly 1H

-- A simplifying variant of _*x+_.

_*x+HN_ : ∀ {n} → HNF (suc n) → Normal n → HNF (suc n)
(p *x+ c′) *x+HN c = (p *x+ c′) *x+ c
∅          *x+HN c with c ≟N 0N
... | just c≈0 = ∅
... | nothing  = ∅ *x+ c

mutual

  -- Addition.

  _+H_ : ∀ {n} → HNF (suc n) → HNF (suc n) → HNF (suc n)
  ∅           +H p           = p
  p           +H ∅           = p
  (p₁ *x+ c₁) +H (p₂ *x+ c₂) = (p₁ +H p₂) *x+HN (c₁ +N c₂)

  _+N_ : ∀ {n} → Normal n → Normal n → Normal n
  con c₁  +N con c₂  = con (c₁ C.+ c₂)
  poly p₁ +N poly p₂ = poly (p₁ +H p₂)

-- Multiplication.

_*x+H_ : ∀ {n} → HNF (suc n) → HNF (suc n) → HNF (suc n)
p₁         *x+H (p₂ *x+ c) = (p₁ +H p₂) *x+HN c
∅          *x+H ∅          = ∅
(p₁ *x+ c) *x+H ∅          = (p₁ *x+ c) *x+ 0N

mutual

  _*NH_ : ∀ {n} → Normal n → HNF (suc n) → HNF (suc n)
  c *NH ∅          = ∅
  c *NH (p *x+ c′) with c ≟N 0N
  ... | just c≈0 = ∅
  ... | nothing  = (c *NH p) *x+ (c *N c′)

  _*HN_ : ∀ {n} → HNF (suc n) → Normal n → HNF (suc n)
  ∅          *HN c = ∅
  (p *x+ c′) *HN c with c ≟N 0N
  ... | just c≈0 = ∅
  ... | nothing  = (p *HN c) *x+ (c′ *N c)

  _*H_ : ∀ {n} → HNF (suc n) → HNF (suc n) → HNF (suc n)
  ∅           *H _           = ∅
  (_ *x+ _)   *H ∅           = ∅
  (p₁ *x+ c₁) *H (p₂ *x+ c₂) =
    ((p₁ *H p₂) *x+H (p₁ *HN c₂ +H c₁ *NH p₂)) *x+HN (c₁ *N c₂)

  _*N_ : ∀ {n} → Normal n → Normal n → Normal n
  con c₁  *N con c₂  = con (c₁ C.* c₂)
  poly p₁ *N poly p₂ = poly (p₁ *H p₂)

-- Exponentiation.

_^N_ : ∀ {n} → Normal n → ℕ → Normal n
p ^N zero  = 1N
p ^N suc n = p *N (p ^N n)

mutual

  -- Negation.

  -H_ : ∀ {n} → HNF (suc n) → HNF (suc n)
  -H p = (-N 1N) *NH p

  -N_ : ∀ {n} → Normal n → Normal n
  -N con c  = con (C.- c)
  -N poly p = poly (-H p)

------------------------------------------------------------------------
-- Normalisation

normalise-con : ∀ {n} → C.Carrier → Normal n
normalise-con {zero}  c = con c
normalise-con {suc n} c = poly (∅ *x+HN normalise-con c)

normalise-var : ∀ {n} → Fin n → Normal n
normalise-var zero    = poly ((∅ *x+ 1N) *x+ 0N)
normalise-var (suc i) = poly (∅ *x+HN normalise-var i)

normalise : ∀ {n} → Polynomial n → Normal n
normalise (op [+] t₁ t₂) = normalise t₁ +N normalise t₂
normalise (op [*] t₁ t₂) = normalise t₁ *N normalise t₂
normalise (con c)        = normalise-con c
normalise (var i)        = normalise-var i
normalise (t :^ k)       = normalise t ^N k
normalise (:- t)         = -N normalise t

-- Evaluation after normalisation.

⟦_⟧↓ : ∀ {n} → Polynomial n → Vec Carrier n → Carrier
⟦ p ⟧↓ ρ = ⟦ normalise p ⟧N ρ

------------------------------------------------------------------------
-- Homomorphism lemmas

0N-homo : ∀ {n} ρ → ⟦ 0N {n} ⟧N ρ ≈ 0#
0N-homo []      = 0-homo
0N-homo (x ∷ ρ) = refl

-- If c is equal to 0N, then c is semantically equal to 0#.

0≈⟦0⟧ : ∀ {n} {c : Normal n} → c ≈N 0N → ∀ ρ → 0# ≈ ⟦ c ⟧N ρ
0≈⟦0⟧ {c = c} c≈0 ρ = sym (begin
  ⟦ c  ⟧N ρ  ≈⟨ ⟦ c≈0 ⟧N-cong ρ ⟩
  ⟦ 0N ⟧N ρ  ≈⟨ 0N-homo ρ ⟩
  0#         ∎)

1N-homo : ∀ {n} ρ → ⟦ 1N {n} ⟧N ρ ≈ 1#
1N-homo []      = 1-homo
1N-homo (x ∷ ρ) = begin
  0# * x + ⟦ 1N ⟧N ρ  ≈⟨ refl ⟨ +-cong ⟩ 1N-homo ρ ⟩
  0# * x + 1#         ≈⟨ lemma₆ _ _ ⟩
  1#                  ∎

-- _*x+HN_ is equal to _*x+_.

*x+HN≈*x+ : ∀ {n} (p : HNF (suc n)) (c : Normal n) →
            ∀ ρ → ⟦ p *x+HN c ⟧H ρ ≈ ⟦ p *x+ c ⟧H ρ
*x+HN≈*x+ (p *x+ c′) c ρ       = refl
*x+HN≈*x+ ∅          c (x ∷ ρ) with c ≟N 0N
... | just c≈0 = begin
  0#                 ≈⟨ 0≈⟦0⟧ c≈0 ρ ⟩
  ⟦ c ⟧N ρ           ≈⟨ sym $ lemma₆ _ _ ⟩
  0# * x + ⟦ c ⟧N ρ  ∎
... | nothing = refl

∅*x+HN-homo : ∀ {n} (c : Normal n) x ρ →
              ⟦ ∅ *x+HN c ⟧H (x ∷ ρ) ≈ ⟦ c ⟧N ρ
∅*x+HN-homo c x ρ with c ≟N 0N
... | just c≈0 = 0≈⟦0⟧ c≈0 ρ
... | nothing = lemma₆ _ _

mutual

  +H-homo : ∀ {n} (p₁ p₂ : HNF (suc n)) →
            ∀ ρ → ⟦ p₁ +H p₂ ⟧H ρ ≈ ⟦ p₁ ⟧H ρ + ⟦ p₂ ⟧H ρ
  +H-homo ∅           p₂          ρ       = sym (+-identityˡ _)
  +H-homo (p₁ *x+ x₁) ∅           ρ       = sym (+-identityʳ _)
  +H-homo (p₁ *x+ c₁) (p₂ *x+ c₂) (x ∷ ρ) = begin
    ⟦ (p₁ +H p₂) *x+HN (c₁ +N c₂) ⟧H (x ∷ ρ)                           ≈⟨ *x+HN≈*x+ (p₁ +H p₂) (c₁ +N c₂) (x ∷ ρ) ⟩

    ⟦ p₁ +H p₂ ⟧H (x ∷ ρ) * x + ⟦ c₁ +N c₂ ⟧N ρ                        ≈⟨ (+H-homo p₁ p₂ (x ∷ ρ) ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ +N-homo c₁ c₂ ρ ⟩

    (⟦ p₁ ⟧H (x ∷ ρ) + ⟦ p₂ ⟧H (x ∷ ρ)) * x + (⟦ c₁ ⟧N ρ + ⟦ c₂ ⟧N ρ)  ≈⟨ lemma₁ _ _ _ _ _ ⟩

    (⟦ p₁ ⟧H (x ∷ ρ) * x + ⟦ c₁ ⟧N ρ) +
    (⟦ p₂ ⟧H (x ∷ ρ) * x + ⟦ c₂ ⟧N ρ)                                  ∎

  +N-homo : ∀ {n} (p₁ p₂ : Normal n) →
            ∀ ρ → ⟦ p₁ +N p₂ ⟧N ρ ≈ ⟦ p₁ ⟧N ρ + ⟦ p₂ ⟧N ρ
  +N-homo (con c₁)  (con c₂)  _ = +-homo _ _
  +N-homo (poly p₁) (poly p₂) ρ = +H-homo p₁ p₂ ρ

*x+H-homo :
  ∀ {n} (p₁ p₂ : HNF (suc n)) x ρ →
  ⟦ p₁ *x+H p₂ ⟧H (x ∷ ρ) ≈
  ⟦ p₁ ⟧H (x ∷ ρ) * x + ⟦ p₂ ⟧H (x ∷ ρ)
*x+H-homo ∅         ∅ _ _ = sym $ lemma₆ _ _
*x+H-homo (p *x+ c) ∅ x ρ = begin
  ⟦ p *x+ c ⟧H (x ∷ ρ) * x + ⟦ 0N ⟧N ρ  ≈⟨ refl ⟨ +-cong ⟩ 0N-homo ρ ⟩
  ⟦ p *x+ c ⟧H (x ∷ ρ) * x + 0#         ∎
*x+H-homo p₁         (p₂ *x+ c₂) x ρ = begin
  ⟦ (p₁ +H p₂) *x+HN c₂ ⟧H (x ∷ ρ)                         ≈⟨ *x+HN≈*x+ (p₁ +H p₂) c₂ (x ∷ ρ) ⟩
  ⟦ p₁ +H p₂ ⟧H (x ∷ ρ) * x + ⟦ c₂ ⟧N ρ                    ≈⟨ (+H-homo p₁ p₂ (x ∷ ρ) ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ refl ⟩
  (⟦ p₁ ⟧H (x ∷ ρ) + ⟦ p₂ ⟧H (x ∷ ρ)) * x + ⟦ c₂ ⟧N ρ      ≈⟨ lemma₀ _ _ _ _ ⟩
  ⟦ p₁ ⟧H (x ∷ ρ) * x + (⟦ p₂ ⟧H (x ∷ ρ) * x + ⟦ c₂ ⟧N ρ)  ∎

mutual

  *NH-homo :
    ∀ {n} (c : Normal n) (p : HNF (suc n)) x ρ →
    ⟦ c *NH p ⟧H (x ∷ ρ) ≈ ⟦ c ⟧N ρ * ⟦ p ⟧H (x ∷ ρ)
  *NH-homo c ∅          x ρ = sym (*-zeroʳ _)
  *NH-homo c (p *x+ c′) x ρ with c ≟N 0N
  ... | just c≈0 = begin
    0#                                            ≈⟨ sym (*-zeroˡ _) ⟩
    0# * (⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ)         ≈⟨ 0≈⟦0⟧ c≈0 ρ ⟨ *-cong ⟩ refl ⟩
    ⟦ c ⟧N ρ  * (⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ)  ∎
  ... | nothing = begin
    ⟦ c *NH p ⟧H (x ∷ ρ) * x + ⟦ c *N c′ ⟧N ρ                 ≈⟨ (*NH-homo c p x ρ ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ *N-homo c c′ ρ ⟩
    (⟦ c ⟧N ρ * ⟦ p ⟧H (x ∷ ρ)) * x + (⟦ c ⟧N ρ * ⟦ c′ ⟧N ρ)  ≈⟨ lemma₃ _ _ _ _ ⟩
    ⟦ c ⟧N ρ * (⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ)               ∎

  *HN-homo :
    ∀ {n} (p : HNF (suc n)) (c : Normal n) x ρ →
    ⟦ p *HN c ⟧H (x ∷ ρ) ≈ ⟦ p ⟧H (x ∷ ρ) * ⟦ c ⟧N ρ
  *HN-homo ∅          c x ρ = sym (*-zeroˡ _)
  *HN-homo (p *x+ c′) c x ρ with c ≟N 0N
  ... | just c≈0 = begin
    0#                                           ≈⟨ sym (*-zeroʳ _) ⟩
    (⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ) * 0#        ≈⟨ refl ⟨ *-cong ⟩ 0≈⟦0⟧ c≈0 ρ ⟩
    (⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ) * ⟦ c ⟧N ρ  ∎
  ... | nothing = begin
    ⟦ p *HN c ⟧H (x ∷ ρ) * x + ⟦ c′ *N c ⟧N ρ                 ≈⟨ (*HN-homo p c x ρ ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ *N-homo c′ c ρ ⟩
    (⟦ p ⟧H (x ∷ ρ) * ⟦ c ⟧N ρ) * x + (⟦ c′ ⟧N ρ * ⟦ c ⟧N ρ)  ≈⟨ lemma₂ _ _ _ _ ⟩
    (⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ) * ⟦ c ⟧N ρ               ∎

  *H-homo : ∀ {n} (p₁ p₂ : HNF (suc n)) →
            ∀ ρ → ⟦ p₁ *H p₂ ⟧H ρ ≈ ⟦ p₁ ⟧H ρ * ⟦ p₂ ⟧H ρ
  *H-homo ∅           p₂          ρ       = sym $ *-zeroˡ _
  *H-homo (p₁ *x+ c₁) ∅           ρ       = sym $ *-zeroʳ _
  *H-homo (p₁ *x+ c₁) (p₂ *x+ c₂) (x ∷ ρ) = begin
    ⟦ ((p₁ *H p₂) *x+H ((p₁ *HN c₂) +H (c₁ *NH p₂))) *x+HN
      (c₁ *N c₂) ⟧H (x ∷ ρ)                                              ≈⟨ *x+HN≈*x+ ((p₁ *H p₂) *x+H ((p₁ *HN c₂) +H (c₁ *NH p₂)))
                                                                                (c₁ *N c₂) (x ∷ ρ) ⟩
    ⟦ (p₁ *H p₂) *x+H
      ((p₁ *HN c₂) +H (c₁ *NH p₂)) ⟧H (x ∷ ρ) * x +
    ⟦ c₁ *N c₂ ⟧N ρ                                                      ≈⟨ (*x+H-homo (p₁ *H p₂) ((p₁ *HN c₂) +H (c₁ *NH p₂)) x ρ
                                                                               ⟨ *-cong ⟩
                                                                             refl)
                                                                              ⟨ +-cong ⟩
                                                                            *N-homo c₁ c₂ ρ ⟩
    (⟦ p₁ *H p₂ ⟧H (x ∷ ρ) * x +
     ⟦ (p₁ *HN c₂) +H (c₁ *NH p₂) ⟧H (x ∷ ρ)) * x +
    ⟦ c₁ ⟧N ρ * ⟦ c₂ ⟧N ρ                                                ≈⟨ (((*H-homo p₁ p₂ (x ∷ ρ) ⟨ *-cong ⟩ refl)
                                                                                ⟨ +-cong ⟩
                                                                              (+H-homo (p₁ *HN c₂) (c₁ *NH p₂) (x ∷ ρ)))
                                                                               ⟨ *-cong ⟩
                                                                             refl)
                                                                              ⟨ +-cong ⟩
                                                                            refl ⟩
    (⟦ p₁ ⟧H (x ∷ ρ) * ⟦ p₂ ⟧H (x ∷ ρ) * x +
     (⟦ p₁ *HN c₂ ⟧H (x ∷ ρ) + ⟦ c₁ *NH p₂ ⟧H (x ∷ ρ))) * x +
    ⟦ c₁ ⟧N ρ * ⟦ c₂ ⟧N ρ                                                ≈⟨ ((refl ⟨ +-cong ⟩ (*HN-homo p₁ c₂ x ρ ⟨ +-cong ⟩ *NH-homo c₁ p₂ x ρ))
                                                                               ⟨ *-cong ⟩
                                                                             refl)
                                                                              ⟨ +-cong ⟩
                                                                            refl ⟩
    (⟦ p₁ ⟧H (x ∷ ρ) * ⟦ p₂ ⟧H (x ∷ ρ) * x +
     (⟦ p₁ ⟧H (x ∷ ρ) * ⟦ c₂ ⟧N ρ + ⟦ c₁ ⟧N ρ * ⟦ p₂ ⟧H (x ∷ ρ))) * x +
    (⟦ c₁ ⟧N ρ * ⟦ c₂ ⟧N ρ)                                              ≈⟨ lemma₄ _ _ _ _ _ ⟩

    (⟦ p₁ ⟧H (x ∷ ρ) * x + ⟦ c₁ ⟧N ρ) *
    (⟦ p₂ ⟧H (x ∷ ρ) * x + ⟦ c₂ ⟧N ρ)                                    ∎

  *N-homo : ∀ {n} (p₁ p₂ : Normal n) →
            ∀ ρ → ⟦ p₁ *N p₂ ⟧N ρ ≈ ⟦ p₁ ⟧N ρ * ⟦ p₂ ⟧N ρ
  *N-homo (con c₁)  (con c₂)  _ = *-homo _ _
  *N-homo (poly p₁) (poly p₂) ρ = *H-homo p₁ p₂ ρ

^N-homo : ∀ {n} (p : Normal n) (k : ℕ) →
          ∀ ρ → ⟦ p ^N k ⟧N ρ ≈ ⟦ p ⟧N ρ ^ k
^N-homo p zero    ρ = 1N-homo ρ
^N-homo p (suc k) ρ = begin
  ⟦ p *N (p ^N k) ⟧N ρ       ≈⟨ *N-homo p (p ^N k) ρ ⟩
  ⟦ p ⟧N ρ * ⟦ p ^N k ⟧N ρ   ≈⟨ refl ⟨ *-cong ⟩ ^N-homo p k ρ ⟩
  ⟦ p ⟧N ρ * (⟦ p ⟧N ρ ^ k)  ∎

mutual

  -H‿-homo : ∀ {n} (p : HNF (suc n)) →
             ∀ ρ → ⟦ -H p ⟧H ρ ≈ - ⟦ p ⟧H ρ
  -H‿-homo p (x ∷ ρ) = begin
    ⟦ (-N 1N) *NH p ⟧H (x ∷ ρ)     ≈⟨ *NH-homo (-N 1N) p x ρ ⟩
    ⟦ -N 1N ⟧N ρ * ⟦ p ⟧H (x ∷ ρ)  ≈⟨ trans (-N‿-homo 1N ρ) (-‿cong (1N-homo ρ)) ⟨ *-cong ⟩ refl ⟩
    - 1# * ⟦ p ⟧H (x ∷ ρ)          ≈⟨ lemma₇ _ ⟩
    - ⟦ p ⟧H (x ∷ ρ)               ∎

  -N‿-homo : ∀ {n} (p : Normal n) →
             ∀ ρ → ⟦ -N p ⟧N ρ ≈ - ⟦ p ⟧N ρ
  -N‿-homo (con c)  _ = -‿homo _
  -N‿-homo (poly p) ρ = -H‿-homo p ρ

------------------------------------------------------------------------
-- Correctness

correct-con : ∀ {n} (c : C.Carrier) (ρ : Vec Carrier n) →
              ⟦ normalise-con c ⟧N ρ ≈ ⟦ c ⟧′
correct-con c []      = refl
correct-con c (x ∷ ρ) = begin
  ⟦ ∅ *x+HN normalise-con c ⟧H (x ∷ ρ)  ≈⟨ ∅*x+HN-homo (normalise-con c) x ρ ⟩
  ⟦ normalise-con c ⟧N ρ            ≈⟨ correct-con c ρ ⟩
  ⟦ c ⟧′                                   ∎

correct-var : ∀ {n} (i : Fin n) →
              ∀ ρ → ⟦ normalise-var i ⟧N ρ ≈ lookup ρ i
correct-var ()      []
correct-var (suc i) (x ∷ ρ) = begin
  ⟦ ∅ *x+HN normalise-var i ⟧H (x ∷ ρ)  ≈⟨ ∅*x+HN-homo (normalise-var i) x ρ ⟩
  ⟦ normalise-var i ⟧N ρ                ≈⟨ correct-var i ρ ⟩
  lookup ρ i                            ∎
correct-var zero (x ∷ ρ) = begin
  (0# * x + ⟦ 1N ⟧N ρ) * x + ⟦ 0N ⟧N ρ  ≈⟨ ((refl ⟨ +-cong ⟩ 1N-homo ρ) ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ 0N-homo ρ ⟩
  (0# * x + 1#) * x + 0#                ≈⟨ lemma₅ _ ⟩
  x                                     ∎

correct : ∀ {n} (p : Polynomial n) → ∀ ρ → ⟦ p ⟧↓ ρ ≈ ⟦ p ⟧ ρ
correct (op [+] p₁ p₂) ρ = begin
  ⟦ normalise p₁ +N normalise p₂ ⟧N ρ  ≈⟨ +N-homo (normalise p₁) (normalise p₂) ρ ⟩
  ⟦ p₁ ⟧↓ ρ + ⟦ p₂ ⟧↓ ρ                ≈⟨ correct p₁ ρ ⟨ +-cong ⟩ correct p₂ ρ ⟩
  ⟦ p₁ ⟧ ρ + ⟦ p₂ ⟧ ρ                  ∎
correct (op [*] p₁ p₂) ρ = begin
  ⟦ normalise p₁ *N normalise p₂ ⟧N ρ  ≈⟨ *N-homo (normalise p₁) (normalise p₂) ρ ⟩
  ⟦ p₁ ⟧↓ ρ * ⟦ p₂ ⟧↓ ρ                ≈⟨ correct p₁ ρ ⟨ *-cong ⟩ correct p₂ ρ ⟩
  ⟦ p₁ ⟧ ρ * ⟦ p₂ ⟧ ρ                  ∎
correct (con c)  ρ = correct-con c ρ
correct (var i)  ρ = correct-var i ρ
correct (p :^ k) ρ = begin
  ⟦ normalise p ^N k ⟧N ρ  ≈⟨ ^N-homo (normalise p) k ρ ⟩
  ⟦ p ⟧↓ ρ ^ k             ≈⟨ correct p ρ ⟨ ^-cong ⟩ PropEq.refl {x = k} ⟩
  ⟦ p ⟧ ρ ^ k              ∎
correct (:- p) ρ = begin
  ⟦ -N normalise p ⟧N ρ  ≈⟨ -N‿-homo (normalise p) ρ ⟩
  - ⟦ p ⟧↓ ρ             ≈⟨ -‿cong (correct p ρ) ⟩
  - ⟦ p ⟧ ρ              ∎

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

open Reflection setoid var ⟦_⟧ ⟦_⟧↓ correct public
  using (prove; solve) renaming (_⊜_ to _:=_)

-- For examples of how solve and _:=_ can be used to
-- semi-automatically prove ring equalities, see, for instance,
-- Data.Digit or Data.Nat.DivMod.


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommMonoid.Base where

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

open import Cubical.Data.Sigma

open import Cubical.Algebra.Monoid

open import Cubical.Displayed.Base
open import Cubical.Displayed.Auto
open import Cubical.Displayed.Record
open import Cubical.Displayed.Universe

open import Cubical.Reflection.RecordEquiv

open Iso

private
  variable
    ℓ ℓ' : Level

record IsCommMonoid {M : Type ℓ}
                    (ε : M) (_·_ : M → M → M) : Type ℓ where
  constructor iscommmonoid

  field
    isMonoid : IsMonoid ε _·_
    ·Comm     : (x y : M) → x · y ≡ y · x

  open IsMonoid isMonoid public

unquoteDecl IsCommMonoidIsoΣ = declareRecordIsoΣ IsCommMonoidIsoΣ (quote IsCommMonoid)

record CommMonoidStr (M : Type ℓ) : Type ℓ where
  constructor commmonoidstr

  field
    ε            : M
    _·_          : M → M → M
    isCommMonoid : IsCommMonoid ε _·_

  infixl 7 _·_

  open IsCommMonoid isCommMonoid public

CommMonoid : ∀ ℓ → Type (ℓ-suc ℓ)
CommMonoid ℓ = TypeWithStr ℓ CommMonoidStr

makeIsCommMonoid : {M : Type ℓ} {ε : M} {_·_ : M → M → M}
                 (is-setM : isSet M)
                 (·Assoc   : (x y z : M) → x · (y · z) ≡ (x · y) · z)
                 (·IdR     : (x : M) → x · ε ≡ x)
                 (·Comm    : (x y : M) → x · y ≡ y · x)
               → IsCommMonoid ε _·_
IsCommMonoid.isMonoid (makeIsCommMonoid is-setM ·Assoc ·IdR ·Comm) =
  makeIsMonoid is-setM ·Assoc ·IdR (λ x → ·Comm _ _ ∙ ·IdR x)
IsCommMonoid.·Comm (makeIsCommMonoid is-setM ·Assoc ·IdR ·Comm) = ·Comm

makeCommMonoid : {M : Type ℓ} (ε : M) (_·_ : M → M → M)
               (is-setM : isSet M)
               (·Assoc : (x y z : M) → x · (y · z) ≡ (x · y) · z)
               (·IdR : (x : M) → x · ε ≡ x)
               (·Comm    : (x y : M) → x · y ≡ y · x)
             → CommMonoid ℓ
fst (makeCommMonoid ε _·_ is-setM ·Assoc ·IdR ·Comm) = _
CommMonoidStr.ε (snd (makeCommMonoid ε _·_ is-setM ·Assoc ·IdR ·Comm)) = ε
CommMonoidStr._·_ (snd (makeCommMonoid ε _·_ is-setM ·Assoc ·IdR ·Comm)) = _·_
CommMonoidStr.isCommMonoid (snd (makeCommMonoid ε _·_ is-setM ·Assoc ·IdR ·Comm)) =
  makeIsCommMonoid is-setM ·Assoc ·IdR ·Comm

CommMonoidStr→MonoidStr : {A : Type ℓ} → CommMonoidStr A → MonoidStr A
CommMonoidStr→MonoidStr (commmonoidstr _ _ H) = monoidstr _ _ (IsCommMonoid.isMonoid H)

CommMonoid→Monoid : CommMonoid ℓ → Monoid ℓ
CommMonoid→Monoid (_ , commmonoidstr  _ _ M) = _ , monoidstr _ _ (IsCommMonoid.isMonoid M)

isSetFromIsCommMonoid :
  {M : Type ℓ} {ε : M} {_·_ : M → M → M}
  (isCommMonoid : IsCommMonoid ε _·_)
  → isSet M
isSetFromIsCommMonoid isCommMonoid =
  let open IsCommMonoid isCommMonoid
  in is-set

isSetCommMonoid : (M : CommMonoid ℓ) → isSet ⟨ M ⟩
isSetCommMonoid M =
  let open CommMonoidStr (snd M)
  in isSetFromIsCommMonoid isCommMonoid

CommMonoidHom : (L : CommMonoid ℓ) (M : CommMonoid ℓ') → Type (ℓ-max ℓ ℓ')
CommMonoidHom L M = MonoidHom (CommMonoid→Monoid L) (CommMonoid→Monoid M)

IsCommMonoidEquiv : {A : Type ℓ} {B : Type ℓ'}
  (M : CommMonoidStr A) (e : A ≃ B) (N : CommMonoidStr B) → Type (ℓ-max ℓ ℓ')
IsCommMonoidEquiv M e N = IsMonoidHom (CommMonoidStr→MonoidStr M) (e .fst) (CommMonoidStr→MonoidStr N)

CommMonoidEquiv : (M : CommMonoid ℓ) (N : CommMonoid ℓ') → Type (ℓ-max ℓ ℓ')
CommMonoidEquiv M N = Σ[ e ∈ (M .fst ≃ N .fst) ] IsCommMonoidEquiv (M .snd) e (N .snd)

isPropIsCommMonoid : {M : Type ℓ} (ε : M) (_·_ : M → M → M)
             → isProp (IsCommMonoid ε _·_)
isPropIsCommMonoid ε _·_  =
  isOfHLevelRetractFromIso 1 IsCommMonoidIsoΣ
    (isPropΣ (isPropIsMonoid ε _·_)
             λ mon → isPropΠ2 (λ _ _ → mon .is-set _ _))
  where
  open IsMonoid

𝒮ᴰ-CommMonoid : DUARel (𝒮-Univ ℓ) CommMonoidStr ℓ
𝒮ᴰ-CommMonoid =
  𝒮ᴰ-Record (𝒮-Univ _) IsCommMonoidEquiv
    (fields:
      data[ ε ∣ autoDUARel _ _ ∣ presε ]
      data[ _·_ ∣ autoDUARel _ _ ∣ pres· ]
      prop[ isCommMonoid ∣ (λ _ _ → isPropIsCommMonoid _ _) ])
  where
  open CommMonoidStr
  open IsMonoidHom

CommMonoidPath : (M N : CommMonoid ℓ) → CommMonoidEquiv M N ≃ (M ≡ N)
CommMonoidPath = ∫ 𝒮ᴰ-CommMonoid .UARel.ua

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module Limit where
  -- Statement that the limit of the function f at point l exists (and its value is L)
  -- This is expressed by converting the standard (ε,δ)-limit definition to Skolem normal form (TODO: ...I think? Is this correct?
  record Lim (f : ℝ → ℝ) (p : ℝ) (L : ℝ) : Stmt where
    field
      δ : ℝ₊ → ℝ₊ -- The delta function that is able to depend on epsilon
      satisfaction : ∀{ε : ℝ} → ⦃ ε > 𝟎 ⦄ → ∀{x : ℝ} → (𝟎 < ‖ x − p ‖ < δ(ε)) → (‖ f(x) − L ‖ < ε)

  -- Limit value function f (if the limit exists)
  lim : (f : ℝ → ℝ) → (p : ℝ) → ⦃ _ : ∃(Lim f(p)) ⦄ → ℝ
  lim _ _ ⦃ l ⦄ = Lim.L(l)

module Proofs where
  postulate [+]-limit : ∀{f g p} → ⦃ _ : ∃(Lim f(p)) ⦄ → ⦃ _ : ∃(Lim g(p)) ⦄ → Lim(x ↦ f(x) + g(x))(p)
  postulate [−]-limit : ∀{f g p} → ⦃ _ : ∃(Lim f(p)) ⦄ → ⦃ _ : ∃(Lim g(p)) ⦄ → Lim(x ↦ f(x) − g(x))(p)
  postulate [⋅]-limit : ∀{f g p} → ⦃ _ : ∃(Lim f(p)) ⦄ → ⦃ _ : ∃(Lim g(p)) ⦄ → Lim(x ↦ f(x) ⋅ g(x))(p)
  postulate [/]-limit : ∀{f g p} → ⦃ _ : ∃(Lim f(p)) ⦄ → ⦃ _ : ∃(Lim g(p)) ⦄ → Lim(x ↦ f(x) / g(x))(p)

  postulate [+]-lim : ∀{f g p} → ⦃ _ : ∃(Lim f(p)) ⦄ → ⦃ _ : ∃(Lim g(p)) ⦄ → (lim(x ↦ f(x) + g(x))(p) ≡ lim f(p) + lim g(p))
  postulate [−]-lim : ∀{f g p} → ⦃ _ : ∃(Lim f(p)) ⦄ → ⦃ _ : ∃(Lim g(p)) ⦄ → (lim(x ↦ f(x) − g(x))(p) ≡ lim f(p) − lim g(p))
  postulate [⋅]-lim : ∀{f g p} → ⦃ _ : ∃(Lim f(p)) ⦄ → ⦃ _ : ∃(Lim g(p)) ⦄ → (lim(x ↦ f(x) ⋅ g(x))(p) ≡ lim f(p) ⋅ lim g(p))
  postulate [/]-lim : ∀{f g p} → ⦃ _ : ∃(Lim f(p)) ⦄ → ⦃ _ : ∃(Lim g(p)) ⦄ → (lim(x ↦ f(x) / g(x))(p) ≡ lim f(p) / lim g(p))

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda