open import 1Lab.Prelude
module Cat.CartesianClosed.Free.Signature where

Signatures for free CCCsπŸ”—

module types {β„“} (T : Type β„“) where
  infixr 22 _`β‡’_
  infixr 20 _`Γ—_
  infix 25 `_

The type of simple types over a type of base types is the inductive type with a constructor for base types, a nullary constructor for the unit type, and binary constructors for products and functions.

  data Ty : Type β„“ where
    `⊀        : Ty
    `_        : T β†’ Ty
    _`Γ—_ _`β‡’_ : Ty β†’ Ty β†’ Ty
We’ll need an β€œobservational” equality on types, both to show that the types of a given are a set, and later to show this also of further constructions on syntax. 
  module code ⦃ _ : H-Level T 2 ⦄ where
    same-ty : Ty β†’ Ty β†’ Prop β„“
    same-ty `⊀ `⊀ = el! (Lift _ ⊀)
    same-ty `⊀ _  = el! (Lift _ βŠ₯)

    same-ty (` x) (` y) = el! (x ≑ y)
    same-ty (` x) _     = el! (Lift _ βŠ₯)

    same-ty (a `Γ— x) (b `Γ— y) = el! (⌞ same-ty a b ⌟ Γ— ⌞ same-ty x y ⌟)
    same-ty (a `Γ— x) _        = el! (Lift _ βŠ₯)

    same-ty (a `β‡’ x) (b `β‡’ y) = el! (⌞ same-ty a b ⌟ Γ— ⌞ same-ty x y ⌟)
    same-ty (a `β‡’ x) _        = el! (Lift _ βŠ₯)

    refl-same-ty : βˆ€ x β†’ ⌞ same-ty x x ⌟
    refl-same-ty `⊀       = lift tt
    refl-same-ty (` x)    = refl
    refl-same-ty (a `Γ— b) = refl-same-ty a , refl-same-ty b
    refl-same-ty (a `β‡’ b) = refl-same-ty a , refl-same-ty b

    from-same-ty : βˆ€ x y β†’ ⌞ same-ty x y ⌟ β†’ x ≑ y
    from-same-ty `⊀       `⊀       p = refl
    from-same-ty (` x)    (` y)    p = ap `_ p
    from-same-ty (a `Γ— x) (b `Γ— y) p = apβ‚‚ _`Γ—_ (from-same-ty a b (p .fst)) (from-same-ty x y (p .snd))
    from-same-ty (a `β‡’ x) (b `β‡’ y) p = apβ‚‚ _`β‡’_ (from-same-ty a b (p .fst)) (from-same-ty x y (p .snd))

    instance
      H-Level-Ty : βˆ€ {n} β†’ H-Level Ty (2 + n)
      H-Level-Ty = basic-instance 2 $ set-identity-system→hlevel
        (Ξ» x y β†’ ⌞ same-ty x y ⌟) refl-same-ty (Ξ» x y β†’ hlevel 1) from-same-ty
open types using (module Ty ; `_ ; _`Γ—_ ; _`β‡’_ ; `⊀) public

A consists of a set of base types, and, for each simple type and base type a set of operations 

record Ξ»-Signature β„“ : Type (lsuc β„“) where
  field
    Ob         : Type β„“
    Ob-is-set  : is-set Ob
    Hom        : types.Ty Ob β†’ Ob β†’ Type β„“
    Hom-is-set : βˆ€ {Ο„ Οƒ} β†’ is-set (Hom Ο„ Οƒ)
  -- This module is meant to always be opened instantiated, so we don't
  -- provide these as instances.

  instance
    H-Level-Ob : βˆ€ {n} β†’ H-Level Ob (2 + n)
    H-Level-Ob = basic-instance 2 Ob-is-set

    H-Level-Hom : βˆ€ {Ο„ Οƒ n} β†’ H-Level (Hom Ο„ Οƒ) (2 + n)
    H-Level-Hom = basic-instance 2 Hom-is-set

  open types Ob using (Ty) public
  open types.code Ob ⦃ auto ⦄ public