MagmaReflection.agda

open import Agda.Primitive using (Level; lsuc ; _⊔_)
open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Product

record Magma l : Set (lsuc l) where
  field
    Carrier : Set l
    eq : Carrier → Carrier → Set l
    plus : Carrier → Carrier → Carrier

open Magma

record _⇒_ {l} (M : Magma l) {l′} (N : Magma l′) : Set (l ⊔ l′) where
  field
    arr : Carrier M → Carrier N
    resp : ∀ {x y}
      → eq M x y → eq N (arr x) (arr y)
    plus : ∀ {x y}
      → eq N (plus N (arr x) (arr y)) (arr (plus M x y))

open _⇒_

_≤ℓ_ : Level -> Level -> Set
α ≤ℓ β = α ⊔ β ≡ β

data Coerce {β} : ∀ {α} -> α ≡ β -> Set α -> Set β where
  coerce : ∀ {A} -> A -> Coerce refl A

{-# NO_POSITIVITY_CHECK #-}
data Tm {l} (N : Magma l) : Set (lsuc l) where
  var : (x : Carrier N) → Tm N
  _+_ : (x y : Tm N) → Tm N
  hom : ∀ {l'} {q : lsuc l' ≤ℓ l} -> Coerce q (∃ λ (M : Magma l') → M ⇒ N × Tm M) → Tm N

mutual
  ⟦_⟧ʰ : ∀ {l l' k} {N : Magma l} {q : _ ≡ k} → Coerce q (∃ λ (M : Magma l') → M ⇒ N × Tm M) → Carrier N
  ⟦ coerce (_ , f , x) ⟧ʰ = arr f ⟦ x ⟧

  ⟦_⟧ : ∀ {l} {M : Magma l} → Tm M → Carrier M
  ⟦ var x ⟧ = x
  ⟦_⟧ {M = M} (x + y) = plus M ⟦ x ⟧ ⟦ y ⟧
  ⟦ hom p ⟧ = ⟦ p ⟧ʰ