62 lines
2.0 KiB
Plaintext
62 lines
2.0 KiB
Plaintext
{-# OPTIONS --cubical --safe --exact-split #-}
|
||
|
||
module Cubical.Structures.Sig where
|
||
|
||
open import Cubical.Foundations.Everything
|
||
open import Cubical.Foundations.Equiv
|
||
open import Cubical.Functions.Image
|
||
open import Cubical.HITs.PropositionalTruncation as P
|
||
open import Cubical.Data.Nat
|
||
open import Cubical.Data.Fin
|
||
open import Cubical.Data.List as L
|
||
open import Cubical.Data.Sigma
|
||
open import Cubical.Data.Empty as ⊥
|
||
open import Cubical.Data.Sum as ⊎
|
||
open import Cubical.Reflection.RecordEquiv
|
||
open import Cubical.HITs.SetQuotients as Q
|
||
open import Agda.Primitive
|
||
|
||
record Sig (f a : Level) : Type ((ℓ-suc f) ⊔ (ℓ-suc a)) where
|
||
field
|
||
symbol : Type f
|
||
arity : symbol -> Type a
|
||
open Sig public
|
||
|
||
FinSig : (f : Level) -> Type (ℓ-suc f)
|
||
FinSig f = Σ (Type f) \sym -> sym -> ℕ
|
||
|
||
finSig : {f : Level} -> FinSig f -> Sig f ℓ-zero
|
||
symbol (finSig σ) = σ .fst
|
||
arity (finSig σ) = Fin ∘ σ .snd
|
||
|
||
emptySig : Sig ℓ-zero ℓ-zero
|
||
symbol emptySig = ⊥.⊥
|
||
arity emptySig = ⊥.rec
|
||
|
||
sumSig : {f a g b : Level} -> Sig f a -> Sig g b -> Sig (ℓ-max f g) (ℓ-max a b)
|
||
symbol (sumSig σ τ) = symbol σ ⊎ symbol τ
|
||
arity (sumSig {b = b} σ τ) (inl x) = Lift {j = b} ((arity σ) x)
|
||
arity (sumSig {a = a} σ τ) (inr x) = Lift {j = a} ((arity τ) x)
|
||
|
||
signature functor
|
||
module _ {f a n : Level} (σ : Sig f a) where
|
||
sig : Type n -> Type (ℓ-max f (ℓ-max a n))
|
||
sig X = Σ (σ .symbol) \f -> σ .arity f -> X
|
||
|
||
sig≡ : {X : Type n} (f : σ .symbol) {i j : σ .arity f -> X}
|
||
-> ((a : σ .arity f) -> i a ≡ j a)
|
||
-> Path (sig X) (f , i) (f , j)
|
||
sig≡ f H = ΣPathP (refl , funExt H)
|
||
|
||
sigF : {X Y : Type n} -> (X -> Y) -> sig X -> sig Y
|
||
sigF h (f , i) = f , h ∘ i
|
||
|
||
module _ {f n : Level} (σ : FinSig f) where
|
||
sigFin : (X : Type n) -> Type (ℓ-max f n)
|
||
sigFin X = sig (finSig σ) X
|
||
|
||
sigFin≡ : {X : Type n} (f : σ .fst) {i j : finSig σ .arity f -> X}
|
||
-> ((a : finSig σ .arity f) -> i a ≡ j a)
|
||
-> Path (sigFin X) (f , i) (f , j)
|
||
sigFin≡ = sig≡ (finSig σ)
|