Skip to content

Commit

Permalink
The update
Browse files Browse the repository at this point in the history
  • Loading branch information
@brandonhewer
brandonhewer committed Nov 27, 2020
0 parents commit a078eef
Show file tree
Hide file tree
Showing 88 changed files with 3,560 additions and 0 deletions.
Binary file added .DS_Store
Binary file not shown.
Empty file added Operad.agda
Empty file.
Binary file added Operad/.DS_Store
Binary file not shown.
93 changes: 93 additions & 0 deletions Operad/Base.agda
Original file line number Diff line number Diff line change
@@ -0,0 +1,93 @@
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Operad.Base where

open import Cubical.Data.Empty renaming (rec to ⊥-rec)
open import Cubical.Data.Nat

open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Prelude hiding (comp)
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Transport

open import Cubical.Relation.Nullary hiding (⟪_⟫)

open import Operad.Fin
open import Operad.FinSet
open import Operad.Species

private
variable
ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ : Level
A : Type ℓ₁
B : A → Type ℓ₂
C : ∀ a → B a → Type ℓ₃
D : ∀ a b → C a b → Type ℓ₄
E : ∀ a b c → D a b c → Type ℓ₅

Comp : (FinSet ℓ₁ → Type ℓ₂) → (A : FinSet ℓ₁) (B : ⟦ A ⟧ → FinSet ℓ₁) → Type _
Comp K A B = K A → (bs : (a : ⟦ A ⟧) → K (B a)) → K (Σⁿ A B)

open Iso

Fin0↔a≢b : ∀ {ℓ₁} {A : Type ℓ₁} {a b : A} → a ≡ b → Iso (Fin 0) (¬ (a ≡ b))
fun (Fin0↔a≢b p) ()
inv (Fin0↔a≢b p) ¬p = ⊥-rec (¬p p)
rightInv (Fin0↔a≢b p) ¬p = ⊥-rec (¬p p)
leftInv (Fin0↔a≢b p) ()

Fin1↔a≢b : ∀ {ℓ₁} {A : Type ℓ₁} {a b : A} → ¬ (a ≡ b) → Iso (Fin 1) (¬ (a ≡ b))
fun (Fin1↔a≢b ¬p) zero = ¬p
inv (Fin1↔a≢b ¬p) _ = zero
rightInv (Fin1↔a≢b ¬p) ¬q = isProp¬ _ _ _
leftInv (Fin1↔a≢b ¬p) zero = refl

record Operad (ℓ₁ ℓ₂ : Level) : Type (ℓ-max (ℓ-suc ℓ₁) (ℓ-suc ℓ₂)) where
field
K : Species 2 ℓ₁ ℓ₂
id : typ (K (⊤-FinSet ℓ₁))
comp : ∀ A B → Comp (typ ∘ K) A B
idl′ : ∀ n k →
subst (typ ∘ K) Σⁿ-Idl (comp (⊤-FinSet ℓ₁) (λ _ → n-FinSet n) id (λ _ → k))
≡ k
idr′ : ∀ n k →
subst (typ ∘ K) Σⁿ-Idr (comp (n-FinSet n) (λ _ → ⊤-FinSet ℓ₁) k λ _ → id)
≡ k
assoc′ : ∀ n (ns : Fin n → ℕ) (nss : (i : Fin n) → Fin (ns i) → ℕ) k ks kss →
let A = n-FinSet n
B = n-FinSet ∘ ns ∘ lower
C i j = n-FinSet (nss (lower i) (lower j))
in subst (typ ∘ K) (Σⁿ-Assoc A B C)
(comp (Σⁿ A B) (uncurry C) (comp A B k ks) (uncurry kss))
≡ (comp A (λ a → Σⁿ (B a) (C a)) k λ a → comp (B a) (C a) (ks a) (kss a))

Ops : FinSet ℓ₁ → Type ℓ₂
Ops = typ ∘ K

isSetOps : ∀ A → isSet (Ops A)
isSetOps = str ∘ K

apply : (A : FinSet ℓ₁) (a : ⟦ A ⟧) → Ops A → Ops (⊥-FinSet ℓ₁) → Ops (A / a)
apply A a f x = subst Ops (Lift≡ _ _ refl) (comp A (A ⟨ a ≢_⟩) f fs)
where
fs : ∀ b → Ops (A ⟨ a ≢ b ⟩)
fs b with isDiscreteFinSet A a b
... | yes p = subst Ops (Lift≡ _ _ (isoToPath (compIso (invIso LiftIso) (Fin0↔a≢b p)))) x
... | no ¬p = subst Ops (Lift≡ _ _ (isoToPath (compIso (invIso LiftIso) (Fin1↔a≢b ¬p)))) id

idl : ∀ A k → subst Ops Σⁿ-Idl (comp (⊤-FinSet ℓ₁) (λ _ → A) id λ _ → k) ≡ k
idl = finiteProp (λ A → ∀ k → _) (λ _ → isPropΠ λ _ → isSetOps _ _ _) idl′

idr : ∀ A k → subst Ops Σⁿ-Idr (comp A (λ _ → ⊤-FinSet ℓ₁) k λ _ → id) ≡ k
idr = finiteProp (λ A → ∀ k → _) (λ _ → isPropΠ λ _ → isSetOps _ _ _) idr′

assoc : ∀ A B C k ks kss →
subst Ops (Σⁿ-Assoc A B C)
(comp (Σⁿ A B) (uncurry C) (comp A B k ks) (uncurry kss))
≡ (comp A (λ a → Σⁿ (B a) (C a)) k λ a → comp (B a) (C a) (ks a) (kss a))
assoc = finiteProp₃
(λ A B C → ∀ k ks kss → _)
(λ _ _ _ → isPropΠ3 λ _ _ _ → isSetOps _ _ _)
assoc′
Binary file added Operad/Base.agdai
Binary file not shown.
93 changes: 93 additions & 0 deletions Operad/Base.agda~
Original file line number Diff line number Diff line change
@@ -0,0 +1,93 @@
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Operad.Base where

open import Cubical.Data.Empty renaming (rec to ⊥-rec)
open import Cubical.Data.Nat

open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Prelude hiding (comp)
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Transport

open import Cubical.Relation.Nullary hiding (⟪_⟫)

open import Operad.Fin
open import Operad.FinSet
open import Operad.Species

private
variable
ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ : Level
A : Type ℓ₁
B : A → Type ℓ₂
C : ∀ a → B a → Type ℓ₃
D : ∀ a b → C a b → Type ℓ₄
E : ∀ a b c → D a b c → Type ℓ₅

Comp : (FinSet ℓ₁ → Type ℓ₂) → (A : FinSet ℓ₁) (B : ⟦ A ⟧ → FinSet ℓ₁) → Type _
Comp K A B = K A → (bs : (a : ⟦ A ⟧) → K (B a)) → K (Σⁿ A B)

open Iso

Fin0↔a≢b : ∀ {ℓ₁} {A : Type ℓ₁} {a b : A} → a ≡ b → Iso (Fin 0) (¬ (a ≡ b))
fun (Fin0↔a≢b p) ()
inv (Fin0↔a≢b p) ¬p = ⊥-rec (¬p p)
rightInv (Fin0↔a≢b p) ¬p = ⊥-rec (¬p p)
leftInv (Fin0↔a≢b p) ()

Fin1↔a≢b : ∀ {ℓ₁} {A : Type ℓ₁} {a b : A} → ¬ (a ≡ b) → Iso (Fin 1) (¬ (a ≡ b))
fun (Fin1↔a≢b ¬p) zero = ¬p
inv (Fin1↔a≢b ¬p) _ = zero
rightInv (Fin1↔a≢b ¬p) ¬q = isProp¬ _ _ _
leftInv (Fin1↔a≢b ¬p) zero = refl

record Operad (ℓ₁ ℓ₂ : Level) : Type (ℓ-max (ℓ-suc ℓ₁) (ℓ-suc ℓ₂)) where
field
K : hSpecies 2 ℓ₁ ℓ₂
id : typ (K (⊤-FinSet ℓ₁))
comp : ∀ A B → Comp (typ ∘ K) A B
idl′ : ∀ n k →
subst (typ ∘ K) Σⁿ-Idl (comp (⊤-FinSet ℓ₁) (λ _ → n-FinSet n) id (λ _ → k))
≡ k
idr′ : ∀ n k →
subst (typ ∘ K) Σⁿ-Idr (comp (n-FinSet n) (λ _ → ⊤-FinSet ℓ₁) k λ _ → id)
≡ k
assoc′ : ∀ n (ns : Fin n → ℕ) (nss : (i : Fin n) → Fin (ns i) → ℕ) k ks kss →
let A = n-FinSet n
B = n-FinSet ∘ ns ∘ lower
C i j = n-FinSet (nss (lower i) (lower j))
in subst (typ ∘ K) (Σⁿ-Assoc A B C)
(comp (Σⁿ A B) (uncurry C) (comp A B k ks) (uncurry kss))
≡ (comp A (λ a → Σⁿ (B a) (C a)) k λ a → comp (B a) (C a) (ks a) (kss a))

Ops : FinSet ℓ₁ → Type ℓ₂
Ops = typ ∘ K

isSetOps : ∀ A → isSet (Ops A)
isSetOps = str ∘ K

apply : (A : FinSet ℓ₁) (a : ⟦ A ⟧) → Ops A → Ops (⊥-FinSet ℓ₁) → Ops (A / a)
apply A a f x = subst Ops (Lift≡ _ _ refl) (comp A (A ⟨ a ≢_⟩) f fs)
where
fs : ∀ b → Ops (A ⟨ a ≢ b ⟩)
fs b with isDiscreteFinSet A a b
... | yes p = subst Ops (Lift≡ _ _ (isoToPath (compIso (invIso LiftIso) (Fin0↔a≢b p)))) x
... | no ¬p = subst Ops (Lift≡ _ _ (isoToPath (compIso (invIso LiftIso) (Fin1↔a≢b ¬p)))) id

idl : ∀ A k → subst Ops Σⁿ-Idl (comp (⊤-FinSet ℓ₁) (λ _ → A) id λ _ → k) ≡ k
idl = finiteProp (λ A → ∀ k → _) (λ _ → isPropΠ λ _ → isSetOps _ _ _) idl′

idr : ∀ A k → subst Ops Σⁿ-Idr (comp A (λ _ → ⊤-FinSet ℓ₁) k λ _ → id) ≡ k
idr = finiteProp (λ A → ∀ k → _) (λ _ → isPropΠ λ _ → isSetOps _ _ _) idr′

assoc : ∀ A B C k ks kss →
subst Ops (Σⁿ-Assoc A B C)
(comp (Σⁿ A B) (uncurry C) (comp A B k ks) (uncurry kss))
≡ (comp A (λ a → Σⁿ (B a) (C a)) k λ a → comp (B a) (C a) (ks a) (kss a))
assoc = finiteProp₃
(λ A B C → ∀ k ks kss → _)
(λ _ _ _ → isPropΠ3 λ _ _ _ → isSetOps _ _ _)
assoc′
8 changes: 8 additions & 0 deletions Operad/Fin.agda
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Operad.Fin where

open import Cubical.Data.FinData hiding (rec) public

open import Operad.Fin.Base public
open import Operad.Fin.Properties public
Binary file added Operad/Fin.agdai
Binary file not shown.
8 changes: 8 additions & 0 deletions Operad/Fin.agda~
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Operad.Fin where

open import Cubical.Data.FinData

open import Operad.Fin.Base public
open import Operad.Fin.Properties public
70 changes: 70 additions & 0 deletions Operad/Fin/Base.agda
Original file line number Diff line number Diff line change
@@ -0,0 +1,70 @@
{-# OPTIONS --cubical --safe #-}

module Operad.Fin.Base where

open import Cubical.Data.Empty renaming (rec to ⊥-rec)
open import Cubical.Data.FinData
open import Cubical.Data.Nat renaming (_·_ to _*_)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Sigma
open import Cubical.Data.Sum

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

open import Cubical.Relation.Nullary

finiteFold : ∀ {ℓ} {A : Type ℓ} (_∙_ : A → A → A) (ε : A) →
∀ n → (Fin n → A) → A
finiteFold _∙_ ε zero as = ε
finiteFold _∙_ ε (suc n) as = as zero ∙ finiteFold _∙_ ε n (as ∘ suc)

ΣFin : ∀ n → (Fin n → ℕ) → ℕ
ΣFin = finiteFold _+_ 0

ΠFin : ∀ n → (Fin n → ℕ) → ℕ
ΠFin = finiteFold _*_ 1

⊎Fin : ∀ n → (Fin n → ℕ) → Type ℓ-zero
⊎Fin n ns = finiteFold _⊎_ (Fin 0) n (Fin ∘ ns)

×Fin : ∀ n → (Fin n → ℕ) → Type ℓ-zero
×Fin n ns = finiteFold _×_ (Fin 1) n (Fin ∘ ns)

inject+ : ∀ {m} n → Fin m → Fin (m + n)
inject+ {suc m} n zero = zero
inject+ {suc m} n (suc i) = suc (inject+ n i)

inject+′ : ∀ {m} n → Fin m → Fin (n + m)
inject+′ {suc m} zero i = i
inject+′ {suc m} (suc n) i = suc (inject+′ n i)

inject* : ∀ {m} n → Fin m → Fin (m * suc n)
inject* {suc m} n zero = zero
inject* {suc m} n (suc i) = suc (inject+′ n (inject* n i))

raise : ∀ m {n} → Fin n → Fin (m + n)
raise zero i = i
raise (suc m) = suc ∘ raise m

splitAt : ∀ m {n} → Fin (m + n) → Fin m ⊎ Fin n
splitAt zero i = inr i
splitAt (suc m) zero = inl zero
splitAt (suc m) (suc i) = map suc (λ x → x) (splitAt m i)

fromℕ< : ∀ {m n} → m < n → Fin n
fromℕ< {zero} {zero} p = ⊥-rec (¬m<m p)
fromℕ< {zero} {suc n} p = zero
fromℕ< {suc m} {zero} p = ⊥-rec (¬-<-zero p)
fromℕ< {suc m} {suc n} p = suc (fromℕ< (pred-≤-pred p))

punchOut : ∀ {m} {i j : Fin (suc m)} → ¬ i ≡ j → Fin m
punchOut {_} {zero} {zero} i≢j = ⊥-rec (i≢j refl)
punchOut {_} {zero} {suc j} _ = j
punchOut {suc m} {suc i} {zero} _ = zero
punchOut {suc m} {suc i} {suc j} i≢j = suc (punchOut (i≢j ∘ cong suc))

punchIn : ∀ {m} → Fin (suc m) → Fin m → Fin (suc m)
punchIn zero j = suc j
punchIn (suc i) zero = zero
punchIn (suc i) (suc j) = suc (punchIn i j)
Binary file added Operad/Fin/Base.agdai
Binary file not shown.
70 changes: 70 additions & 0 deletions Operad/Fin/Base.agda~
Original file line number Diff line number Diff line change
@@ -0,0 +1,70 @@
{-# OPTIONS --cubical --safe #-}

module Operad.Fin.Base where

open import Cubical.Data.Empty renaming (rec to ⊥-rec)
open import Cubical.Data.FinData
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Sigma
open import Cubical.Data.Sum

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

open import Cubical.Relation.Nullary

finiteFold : ∀ {ℓ} {A : Type ℓ} (_∙_ : A → A → A) (ε : A) →
∀ n → (Fin n → A) → A
finiteFold _∙_ ε zero as = ε
finiteFold _∙_ ε (suc n) as = as zero ∙ finiteFold _∙_ ε n (as ∘ suc)

ΣFin : ∀ n → (Fin n → ℕ) → ℕ
ΣFin = finiteFold _+_ 0

ΠFin : ∀ n → (Fin n → ℕ) → ℕ
ΠFin = finiteFold _*_ 1

⊎Fin : ∀ n → (Fin n → ℕ) → Type ℓ-zero
⊎Fin n ns = finiteFold _⊎_ (Fin 0) n (Fin ∘ ns)

×Fin : ∀ n → (Fin n → ℕ) → Type ℓ-zero
×Fin n ns = finiteFold _×_ (Fin 1) n (Fin ∘ ns)

inject+ : ∀ {m} n → Fin m → Fin (m + n)
inject+ {suc m} n zero = zero
inject+ {suc m} n (suc i) = suc (inject+ n i)

inject+′ : ∀ {m} n → Fin m → Fin (n + m)
inject+′ {suc m} zero i = i
inject+′ {suc m} (suc n) i = suc (inject+′ n i)

inject* : ∀ {m} n → Fin m → Fin (m * suc n)
inject* {suc m} n zero = zero
inject* {suc m} n (suc i) = suc (inject+′ n (inject* n i))

raise : ∀ m {n} → Fin n → Fin (m + n)
raise zero i = i
raise (suc m) = suc ∘ raise m

splitAt : ∀ m {n} → Fin (m + n) → Fin m ⊎ Fin n
splitAt zero i = inr i
splitAt (suc m) zero = inl zero
splitAt (suc m) (suc i) = map suc (λ x → x) (splitAt m i)

fromℕ< : ∀ {m n} → m < n → Fin n
fromℕ< {zero} {zero} p = ⊥-rec (¬m<m p)
fromℕ< {zero} {suc n} p = zero
fromℕ< {suc m} {zero} p = ⊥-rec (¬-<-zero p)
fromℕ< {suc m} {suc n} p = suc (fromℕ< (pred-≤-pred p))

punchOut : ∀ {m} {i j : Fin (suc m)} → ¬ i ≡ j → Fin m
punchOut {_} {zero} {zero} i≢j = ⊥-rec (i≢j refl)
punchOut {_} {zero} {suc j} _ = j
punchOut {suc m} {suc i} {zero} _ = zero
punchOut {suc m} {suc i} {suc j} i≢j = suc (punchOut (i≢j ∘ cong suc))

punchIn : ∀ {m} → Fin (suc m) → Fin m → Fin (suc m)
punchIn zero j = suc j
punchIn (suc i) zero = zero
punchIn (suc i) (suc j) = suc (punchIn i j)
Loading

0 comments on commit a078eef

Please sign in to comment.