search

pufferffish / agda-symmetries

MIT License
5 stars 1 forks source link

refactor as (Tree σ Unit -> Tree σ X) × (Tree σ Unit -> Tree σ X) ? #46

Open github-actions[bot] opened 9 months ago

github-actions[bot] commented 9 months ago

https://api.github.com/pufferffish/agda-symmetries/blob/0ff92bdb19aba58e89e9690583a23f811cdcca95/Cubical/Structures/Eq.agda#L35


free (finEqSig σ) = Fin ∘ σ .snd

module _ {f a e n : Level} (σ : Sig f a) (τ : EqSig e n) where
  -- TODO: refactor as (Tree σ Unit -> Tree σ X) × (Tree σ Unit -> Tree σ X) ?
  seq : Type (ℓ-max (ℓ-max (ℓ-max f a) e) n)
  seq = (e : τ .name) -> Tree σ (τ .free e) × Tree σ (τ .free e)

module _ {f a e n s : Level} {σ : Sig f a} {τ : EqSig e n} where
  -- type of structure satisfying equations
  -- TODO: refactor as a coequaliser
  infix 30 _⊨_
  _⊨_ : struct s σ -> (ε : seq σ τ) -> Type (ℓ-max s (ℓ-max e n))
  𝔛 ⊨ ε = (eqn : τ .name) (ρ : τ .free eqn -> 𝔛 .carrier)
       -> sharp σ 𝔛 ρ (ε eqn .fst) ≡ sharp σ 𝔛 ρ (ε eqn .snd)