Very basic model of an interpretation of http header to show that it is a dependent type

basic-http-model.agda

{-# OPTIONS --without-K --safe #-}

Type = Set

record Σ {A : Type } (B : A → Type) : Type  where
  constructor
    _,_
  field
    pr₁ : A
    pr₂ : B pr₁

open Σ public
infixr 0 _,_

Sigma : (A : Type) (B : A → Type) → Type
Sigma A B = Σ {A} B

syntax Sigma A (λ x → b) = Σ x ꞉ A , b

infix -1 Sigma

_×_ : Type → Type → Type
A × B = Σ x ꞉ A , B

infixr 2 _×_

data ℕ : Type where
  zero : ℕ
  suc : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

data List (A : Type) : Type where
  [] : List A
  _::_ : A → List A → List A

infixr 10 _::_

data 𝟘 : Type where

data 𝟙 : Type where
  ⋆ : 𝟙  -- \star

data 𝟚 : Type where
  zero one : 𝟚

data _∔_ (A B : Type) : Type where
  inl : A → A ∔ B
  inr : B → A ∔ B

infixr 20 _∔_

data Mime : Type where
  xml rdf : Mime

-- dependent type for mime types
Tp : Mime → Type
Tp xml = ℕ   -- should be dom
Tp rdf = 𝟚   -- should be set of triples

HttpResponse : Type
HttpResponse =  Mime × List 𝟚  -- an http response consists of a header and bytes

-- Interpretation of HTTPResponses return either an parsing error ⋆
-- or the type of object corresponding to the mime type
-- realistic examples too complex
Inter : (r : HttpResponse) → (𝟙 ∔ Tp (pr₁ r))
Inter (rdf , one :: zero :: zero :: one :: [] ) = inr zero
Inter (xml , one :: one :: zero :: one :: [] ) = inr 22
Inter (m , bits) = inl ⋆