Dependent GC scratchpad

DGC.agda

open import Data.Product
postulate
  P₁ P₂ P₃ : Set
  T₁ : P₁ → Set
  T₂ : P₂ → Set
  T₃ : P₃ → Set
  f₁ : P₁ → P₂
  f₂ : P₂ → P₃
  f₁⁻¹ : P₂ → P₁
  f₂⁻² : P₃ → P₂

  F₁ : Σ P₂ T₂ → Σ P₁ T₁
  F₂ : Σ P₃ T₃ → Σ P₂ T₂

open import Function

( U , Σ U T where T : U → Set , α :  U × Σ U T → L)
( V , Σ V S where S : V → Set , β :  V × Σ V S → L)

maps
f : U → V
F : Σ V S → Σ U T    need to specify a map _ : V → U ...
F (v, S[v]) := ( f⁻¹ v ??? , ? )

(u : U)(x : Σ V S) → α u (F x) ≤  β (f u) x

_ : P₁ → P₃
_ = f₂ ∘ f₁

_ : Σ P₃ T₃ → Σ P₁ T₁
_ = λ{ (p , T₃[p]) → let
                     x = F₂ (p , T₃[p])
                     y = F₁ (proj₁ x , proj₂ x)
                     in y}

Re conversation with Bruno about resource awareness on the index p
give it a multiplicity of 0