DepDial internal hom

Ihom.agda

record Poly : Set₁ where
  constructor _◂_◂_ 
  field
    pos : Set
    dir : pos → Set
    α : (p : pos)(d : dir p) → Set

open import Data.Product
 
_⇒_ : Poly → Poly → Poly
(p₁ ◂ d₁ ◂ α) ⇒ (p₂ ◂ d₂ ◂ β) = Σ (p₁ → p₂) (λ f → (u : p₁)(y : d₂ (f u))→ d₁ u) ◂ (λ{ (f , F) → Σ p₁ (λ u → d₂(f u))}) ◂ λ{ (f , F) (u , y) → α u (F u y) × β (f u) y}

_⇒_ : Poly → Poly → Poly
p ⇒ q = positions ◂ directions ◂ relation
  where
    -- using Valeria's variable names
    -- ((u : U), Vᵤ, α)
    open Poly p renaming (pos to U; dir to X)
    -- ((v : V), Yᵥ, β)
    open Poly q renaming (pos to V; dir to Y; α to β)

    -- a product of the types of `f` and `F`
    -- it is a sigma because the type of `F` is dependent on `f`
    positions : Set
    positions = Σ[ f ∈ (U → V) ] ((u : U)(y : Y(f(u))) → X(u))
             -- type of f ^                  type of F ^ 
  

    -- ((u : U), Y(f(u))
    -- the input type of the relation
    -- depends on the map `f` defined previously 
    directions : positions → Set
    directions (f , F) = Σ[ u ∈ U ] Y(f(u))


    -- relation (or 'eval') computes the relations and demand they both hold 
    relation : (p : positions)→ directions p → Set
    relation (f , F)(u , y) = α u (F u y) × β (f u) y