module IIDg where open import LF -- Codes for indexed inductive types data OPg (I : Set) : Set1 where ι : I -> OPg I σ : (A : Set)(γ : A -> OPg I) -> OPg I δ : (H : Set)(i : H -> I)(γ : OPg I) -> OPg I -- The top-level structure of values in an IIDg Args : {I : Set}(γ : OPg I)(U : I -> Set) -> Set Args (ι _) U = One Args (σ A γ) U = A × \a -> Args (γ a) U Args (δ H i γ) U = ((x : H) -> U (i x)) × \_ -> Args γ U -- The index of a value in an IIDg Index : {I : Set}(γ : OPg I)(U : I -> Set) -> Args γ U -> I Index (ι i) U _ = i Index (σ A γ) U < a | b > = Index (γ a) U b Index (δ _ _ γ) U < _ | b > = Index γ U b -- The assumptions of a particular inductive occurrence. IndArg : {I : Set}(γ : OPg I)(U : I -> Set) -> Args γ U -> Set IndArg (ι _) U _ = Zero IndArg (σ A γ) U < a | b > = IndArg (γ a) U b IndArg (δ H i γ) U < _ | b > = H + IndArg γ U b -- The index of an inductive occurrence. IndIndex : {I : Set}(γ : OPg I)(U : I -> Set)(a : Args γ U) -> IndArg γ U a -> I IndIndex (ι _) U _ () IndIndex (σ A γ) U < a | b > h = IndIndex (γ a) U b h IndIndex (δ A i γ) U < g | b > (inl h) = i h IndIndex (δ A i γ) U < g | b > (inr h) = IndIndex γ U b h -- An inductive occurrence. Ind : {I : Set}(γ : OPg I)(U : I -> Set)(a : Args γ U)(h : IndArg γ U a) -> U (IndIndex γ U a h) Ind (ι _) U _ () Ind (σ A γ) U < a | b > h = Ind (γ a) U b h Ind (δ H i γ) U < g | b > (inl h) = g h Ind (δ H i γ) U < _ | b > (inr h) = Ind γ U b h -- The type of induction hypotheses. IndHyp : {I : Set}(γ : OPg I)(U : I -> Set)(C : (i : I) -> U i -> Set)(a : Args γ U) -> Set IndHyp γ U C a = (hyp : IndArg γ U a) -> C (IndIndex γ U a hyp) (Ind γ U a hyp) -- Large induction hypostheses. IndHyp₁ : {I : Set}(γ : OPg I)(U : I -> Set)(C : (i : I) -> U i -> Set1)(a : Args γ U) -> Set1 IndHyp₁ γ U C a = (hyp : IndArg γ U a) -> C (IndIndex γ U a hyp) (Ind γ U a hyp)