Unityped type theories

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-04-14.
Last modified on 2023-06-24.

{-# OPTIONS --guardedness --allow-unsolved-metas #-}

module type-theories.unityped-type-theories where
Imports 
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.sets
open import foundation.universe-levels

Idea

Unityped type theories are type theories in which all terms have the same type. They are sometimes called untyped type theories. The category of unityped type theories is equivalent to the category of single sorted algebraic theories.

Definitions

module unityped where

  record system (l : Level) : UU (lsuc l)
    where
    coinductive
    field
      element : UU l
      slice : system l

  record system-Set (l : Level) : UU (lsuc l)
    where
    coinductive
    field
      element : Set l
      slice : system-Set l

  record hom-system
    {l1 l2 : Level} (σ : system l1) (T : system l2) : UU (l1 ⊔ l2)
    where
    coinductive
    field
      element : system.element σ → system.element T
      slice : hom-system (system.slice σ) (system.slice T)

  id-hom-system :
    {l : Level} (σ : system l) → hom-system σ σ
  hom-system.element (id-hom-system σ) = id
  hom-system.slice (id-hom-system σ) = id-hom-system (system.slice σ)

  comp-hom-system :
    {l1 l2 l3 : Level} {σ : system l1} {τ : system l2} {υ : system l3}
    (β : hom-system τ υ) (α : hom-system σ τ) → hom-system σ υ
  hom-system.element (comp-hom-system β α) =
    hom-system.element β ∘ hom-system.element α
  hom-system.slice (comp-hom-system β α) =
    comp-hom-system (hom-system.slice β) (hom-system.slice α)

  record htpy-hom-system
    {l1 l2 : Level}
    {σ : system l1} {τ : system l2} (g h : hom-system σ τ) :
    UU (l1 ⊔ l2)
    where
    coinductive
    field
      element : hom-system.element g ~ hom-system.element h
      slice : htpy-hom-system (hom-system.slice g) (hom-system.slice h)

  record weakening
    {l : Level} (σ : system l) : UU l
    where
    coinductive
    field
      element : hom-system σ (system.slice σ)
      slice : weakening (system.slice σ)

  record preserves-weakening
    {l1 l2 : Level}
    {σ : system l1} {τ : system l2}
    (Wσ : weakening σ) (Wτ : weakening τ)
    (h : hom-system σ τ) : UU (l1 ⊔ l2)
    where
    coinductive
    field
      element :
        htpy-hom-system
          ( comp-hom-system
            ( hom-system.slice h)
            ( weakening.element Wσ))
          ( comp-hom-system
            ( weakening.element Wτ)
            ( h))
      slice :
        preserves-weakening
          ( weakening.slice Wσ)
          ( weakening.slice Wτ)
          ( hom-system.slice h)

  record substitution
    {l : Level} (σ : system l) : UU l
    where
    coinductive
    field
      element :
        system.element σ → hom-system (system.slice σ) σ
      slice : substitution (system.slice σ)

  record preserves-substitution
    {l1 l2 : Level}
    {σ : system l1} {τ : system l2}
    (Sσ : substitution σ) (Sτ : substitution τ)
    (h : hom-system σ τ) : UU (l1 ⊔ l2)
    where
    coinductive
    field
      element :
        (x : system.element σ) →
        htpy-hom-system
          ( comp-hom-system
            ( h)
            ( substitution.element Sσ x))
          ( comp-hom-system
            ( substitution.element Sτ
              ( hom-system.element h x))
            ( hom-system.slice h))
      slice :
        preserves-substitution
          ( substitution.slice Sσ)
          ( substitution.slice Sτ)
          ( hom-system.slice h)

  record generic-element
    {l : Level} (σ : system l) : UU l
    where
    coinductive
    field
      element : system.element (system.slice σ)
      slice : generic-element (system.slice σ)

  record preserves-generic-element
    {l1 l2 : Level} {σ : system l1} {τ : system l2}
    (δσ : generic-element σ) (δτ : generic-element τ)
    (h : hom-system σ τ) : UU (l1 ⊔ l2)
    where
    coinductive
    field
      element :
        Id
          ( hom-system.element
            ( hom-system.slice h)
            ( generic-element.element δσ))
          ( generic-element.element δτ)
      slice :
        preserves-generic-element
          ( generic-element.slice δσ)
          ( generic-element.slice δτ)
          ( hom-system.slice h)

  record weakening-preserves-weakening
    {l : Level} {σ : system l} (W : weakening σ) : UU l
    where
    coinductive
    field
      element :
        preserves-weakening
          ( W)
          ( weakening.slice W)
          ( weakening.element W)
      slice :
        weakening-preserves-weakening (weakening.slice W)

  record substitution-preserves-substitution
    {l : Level} {σ : system l} (S : substitution σ) : UU l
    where
    coinductive
    field
      element :
        (x : system.element σ) →
        preserves-substitution
          ( substitution.slice S)
          ( S)
          ( substitution.element S x)
      slice :
        substitution-preserves-substitution (substitution.slice S)

  record weakening-preserves-substitution
    {l : Level} {σ : system l}
    (W : weakening σ) (S : substitution σ) : UU l
    where
    coinductive
    field
      element :
        preserves-substitution
          ( S)
          ( substitution.slice S)
          ( weakening.element W)
      slice :
        weakening-preserves-substitution
          ( weakening.slice W)
          ( substitution.slice S)

  record substitution-preserves-weakening
    {l : Level} {σ : system l} (W : weakening σ) (S : substitution σ) : UU l
    where
    coinductive
    field
      element :
        (x : system.element σ) →
        preserves-weakening
          ( weakening.slice W)
          ( W)
          ( substitution.element S x)
      slice :
        substitution-preserves-weakening
          ( weakening.slice W)
          ( substitution.slice S)

  record weakening-preserves-generic-element
    {l : Level} {σ : system l} (W : weakening σ) (δ : generic-element σ) : UU l
    where
    coinductive
    field
      element :
        preserves-generic-element
          ( δ)
          ( generic-element.slice δ)
          ( weakening.element W)
      slice :
        weakening-preserves-generic-element
          ( weakening.slice W)
          ( generic-element.slice δ)

  record substitution-preserves-generic-element
    {l : Level} {σ : system l} (S : substitution σ) (δ : generic-element σ) :
    UU l
    where
    coinductive
    field
      element :
        (x : system.element σ) →
        preserves-generic-element
          ( generic-element.slice δ)
          ( δ)
          ( substitution.element S x)
      slice :
        substitution-preserves-generic-element
          ( substitution.slice S)
          ( generic-element.slice δ)

  record substitution-cancels-weakening
    {l : Level} {σ : system l} (W : weakening σ) (S : substitution σ) : UU l
    where
    coinductive
    field
      element :
        (x : system.element σ) →
        htpy-hom-system
          ( comp-hom-system
            ( substitution.element S x)
            ( weakening.element W))
          ( id-hom-system σ)
      slice :
        substitution-cancels-weakening
          ( weakening.slice W)
          ( substitution.slice S)

  record generic-element-is-identity
    {l : Level} {σ : system l} (S : substitution σ) (δ : generic-element σ) :
    UU l
    where
    coinductive
    field
      element :
        (x : system.element σ) →
        Id ( hom-system.element
              ( substitution.element S x)
              ( generic-element.element δ))
            ( x)
      slice :
        generic-element-is-identity
          ( substitution.slice S)
          ( generic-element.slice δ)

  record substitution-by-generic-element
    {l : Level} {σ : system l} (W : weakening σ) (S : substitution σ)
    (δ : generic-element σ) : UU l
    where
    coinductive
    field
      element :
        htpy-hom-system
          ( comp-hom-system
            ( substitution.element
              ( substitution.slice S)
              ( generic-element.element δ))
            ( weakening.element (weakening.slice W)))
          ( id-hom-system (system.slice σ))
      slice :
        substitution-by-generic-element
          ( weakening.slice W)
          ( substitution.slice S)
          ( generic-element.slice δ)

  record type-theory
    (l : Level) : UU (lsuc l)
    where
    field
      sys : system l
      W : weakening sys
      S : substitution sys
      δ : generic-element sys
      WW : weakening-preserves-weakening W
      SS : substitution-preserves-substitution S
      WS : weakening-preserves-substitution W S
      SW : substitution-preserves-weakening W S
      Wδ : weakening-preserves-generic-element W δ
      Sδ : substitution-preserves-generic-element S δ
      S!W : substitution-cancels-weakening W S
      δid : generic-element-is-identity S δ
      Sδ! : substitution-by-generic-element W S δ

  slice-type-theory :
    {l : Level} (T : type-theory l) → type-theory l
  type-theory.sys (slice-type-theory T) =
    system.slice (type-theory.sys T)
  type-theory.W (slice-type-theory T) =
    weakening.slice (type-theory.W T)
  type-theory.S (slice-type-theory T) =
    substitution.slice (type-theory.S T)
  type-theory.δ (slice-type-theory T) =
    generic-element.slice (type-theory.δ T)
  type-theory.WW (slice-type-theory T) =
    weakening-preserves-weakening.slice (type-theory.WW T)
  type-theory.SS (slice-type-theory T) =
    substitution-preserves-substitution.slice (type-theory.SS T)
  type-theory.WS (slice-type-theory T) =
    weakening-preserves-substitution.slice (type-theory.WS T)
  type-theory.SW (slice-type-theory T) =
    substitution-preserves-weakening.slice (type-theory.SW T)
  type-theory.Wδ (slice-type-theory T) =
    weakening-preserves-generic-element.slice (type-theory.Wδ T)
  type-theory.Sδ (slice-type-theory T) =
    substitution-preserves-generic-element.slice (type-theory.Sδ T)
  type-theory.S!W (slice-type-theory T) =
    substitution-cancels-weakening.slice (type-theory.S!W T)
  type-theory.δid (slice-type-theory T) =
    generic-element-is-identity.slice (type-theory.δid T)
  type-theory.Sδ! (slice-type-theory T) =
    substitution-by-generic-element.slice (type-theory.Sδ! T)

  module C-system where

    El : {l : Level} (A : type-theory l) → ℕ → UU l
    El A zero-ℕ = system.element (type-theory.sys A)
    El A (succ-ℕ n) = El (slice-type-theory A) n

    iterated-weakening :
      {l : Level} {A : type-theory l} {m n : ℕ} →
      El A n → El A (succ-ℕ (m +ℕ n))
    iterated-weakening {l} {A} {zero-ℕ} {n} x =
      {!hom-system.element (weakening.element (type-theory.W A)) !}
    iterated-weakening {l} {A} {succ-ℕ m} {n} x = {!!}

hom(X,Y) := Tm(W(X,Y))

    hom : {l : Level} (A : type-theory l) → ℕ → ℕ → UU l
    hom A m n = El A (succ-ℕ (m +ℕ n))

    id-hom : {l : Level} (A : type-theory l) (n : ℕ) → hom A n n
    id-hom A zero-ℕ = generic-element.element (type-theory.δ A)
    id-hom A (succ-ℕ n) = {!!}

The forgetful functor from unityped type theories to simple type theories

module simple-unityped where

{-
  system :
    {l : Level} → unityped.system l → simple.system l unit
  simple.system.element (system A) x = unityped.system.element A
  simple.system.slice (system A) x = system (unityped.system.slice A)

  hom-system :
    {l1 l2 : Level} {A : unityped.system l1} {B : unityped.system l2} →
    unityped.hom-system A B →
    simple.hom-system id
      ( system A)
      ( system B)
  simple.hom-system.element (hom-system f) = unityped.hom-system.element f
  simple.hom-system.slice (hom-system f) x =
    hom-system (unityped.hom-system.slice f)

  id-hom-system :
    {l : Level} (A : unityped.system l) →
    simple.htpy-hom-system
      ( hom-system (unityped.id-hom-system A))
      ( simple.id-hom-system (system A))
  simple.htpy-hom-system.element (id-hom-system A) x = refl-htpy
  simple.htpy-hom-system.slice (id-hom-system A) x =
    id-hom-system (unityped.system.slice A)

  comp-hom-system :
    {l1 l2 l3 : Level} {A : unityped.system l1} {B : unityped.system l2}
    {C : unityped.system l3} (g : unityped.hom-system B C)
    (f : unityped.hom-system A B) →
    simple.htpy-hom-system
      ( hom-system (unityped.comp-hom-system g f))
      ( simple.comp-hom-system
        ( hom-system g)
        ( hom-system f))
  simple.htpy-hom-system.element (comp-hom-system g f) x = refl-htpy
  simple.htpy-hom-system.slice (comp-hom-system g f) x =
    comp-hom-system
      ( unityped.hom-system.slice g)
      ( unityped.hom-system.slice f)

  htpy-hom-system :
    {l1 l2 : Level} {A : unityped.system l1} {B : unityped.system l2}
    {f g : unityped.hom-system A B} →
    unityped.htpy-hom-system f g →
    simple.htpy-hom-system (hom-system f) (hom-system g)
  simple.htpy-hom-system.element (htpy-hom-system H) x =
    unityped.htpy-hom-system.element H
  simple.htpy-hom-system.slice (htpy-hom-system H) x =
    htpy-hom-system (unityped.htpy-hom-system.slice H)

  weakening :
    {l : Level} {A : unityped.system l} → unityped.weakening A →
    simple.weakening (system A)
  simple.weakening.element (weakening W) x =
    hom-system (unityped.weakening.element W)
  simple.weakening.slice (weakening W) x =
    weakening (unityped.weakening.slice W)

  preserves-weakening :
    {l1 l2 : Level} {A : unityped.system l1} {B : unityped.system l2}
    {WA : unityped.weakening A} {WB : unityped.weakening B}
    {f : unityped.hom-system A B} →
    unityped.preserves-weakening WA WB f →
    simple.preserves-weakening (weakening WA) (weakening WB) (hom-system f)
  simple.preserves-weakening.element (preserves-weakening Wf) x =
    {!simple.concat-htpy-hom-system!}
  simple.preserves-weakening.slice (preserves-weakening Wf) = {!!}

  substitution :
    {l : Level} {A : unityped.system l} → unityped.substitution A →
    simple.substitution (system A)
  simple.substitution.element (substitution S) x =
    hom-system (unityped.substitution.element S x)
  simple.substitution.slice (substitution S) x =
    substitution (unityped.substitution.slice S)

  generic-element :
    {l : Level} {A : unityped.system l} → unityped.generic-element A →
    simple.generic-element (system A)
  simple.generic-element.element (generic-element δ) x =
    unityped.generic-element.element δ
  simple.generic-element.slice (generic-element δ) x =
    generic-element (unityped.generic-element.slice δ)
-}

Recent changes