Documentation

d_reify'45'reflect_12 ∷ T_Kind_476 → T_Ctx'8902'_2 → T__'8866'Ne'8902'__6 → T__'8801'__12 Source #

d_evalCRSubst_38 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Kind_476 → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → T__'8866''8902'__20 → T__'8866''8902'__20 → T__'8801'__12 → AgdaAny Source #

du_evalCRSubst_38 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Kind_476 → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → T__'8866''8902'__20 → T__'8866''8902'__20 → AgdaAny Source #

d_ren'45'nf_56 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Kind_476 → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → T__'8866''8902'__20 → T__'8801'__12 Source #

d_ren'45'nf'45'μ_74 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Kind_476 → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → T__'8866'Nf'8902'__4 → T__'8866'Nf'8902'__4 → T__'8801'__12 Source #

d_SubNf_90 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → () Source #

d_subNf_104 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4) → T_Kind_476 → T__'8866'Nf'8902'__4 → T__'8866'Nf'8902'__4 Source #

d_subNf'45'id_116 ∷ T_Ctx'8902'_2 → T_Kind_476 → T__'8866'Nf'8902'__4 → T__'8801'__12 Source #

d_subNf'45'id''_126 ∷ T_Ctx'8902'_2 → T_Kind_476 → T__'8866'Nf'8902'__4 → T__'8801'__12 Source #

d_subNf'45''8715'_142 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Kind_476 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4) → T__'8715''8902'__14 → T__'8801'__12 Source #

d_subNf'45'nf_160 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4) → T_Kind_476 → T__'8866''8902'__20 → T__'8801'__12 Source #

d_subNf'45'comp_182 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4) → (T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4) → T_Kind_476 → T__'8866'Nf'8902'__4 → T__'8801'__12 Source #

d_extsNf_198 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4) → T_Kind_476 → T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4 Source #

du_extsNf_198 ∷ T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4) → T_Kind_476 → T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4 Source #

d_subNf'45'cons_218 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4) → T_Kind_476 → T__'8866'Nf'8902'__4 → T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4 Source #

du_subNf'45'cons_218 ∷ (T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4) → T__'8866'Nf'8902'__4 → T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4 Source #

d__'91'_'93'Nf_236 ∷ T_Ctx'8902'_2 → T_Kind_476 → T_Kind_476 → T__'8866'Nf'8902'__4 → T__'8866'Nf'8902'__4 → T__'8866'Nf'8902'__4 Source #

d_subNf'45'cong_260 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4) → (T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4) → (T_Kind_476 → T__'8715''8902'__14 → T__'8801'__12) → T_Kind_476 → T__'8866'Nf'8902'__4 → T__'8801'__12 Source #

d_subNf'45'cong''_280 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4) → T_Kind_476 → T__'8866'Nf'8902'__4 → T__'8866'Nf'8902'__4 → T__'8801'__12 → T__'8801'__12 Source #

d_renNf'45'subNf_300 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4) → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → T_Kind_476 → T__'8866'Nf'8902'__4 → T__'8801'__12 Source #

d_subNf'45'renNf_324 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → (T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4) → T_Kind_476 → T__'8866'Nf'8902'__4 → T__'8801'__12 Source #

d_ren'91''93'Nf_350 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Kind_476 → T_Kind_476 → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → T__'8866'Nf'8902'__4 → T__'8866'Nf'8902'__4 → T__'8801'__12 Source #

d_sub'91''93'Nf_378 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Kind_476 → T_Kind_476 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4) → T__'8866'Nf'8902'__4 → T__'8866'Nf'8902'__4 → T__'8801'__12 Source #

d_subNf'45'lemma_404 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Kind_476 → T_Kind_476 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4) → T__'8866''8902'__20 → T__'8801'__12 Source #

d_subNf'45'lemma''_422 ∷ T_Ctx'8902'_2 → T_Kind_476 → T_Kind_476 → T__'8866''8902'__20 → T__'8801'__12 Source #

d_sub'91''93'Nf''_446 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Kind_476 → T_Kind_476 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4) → T__'8866'Nf'8902'__4 → T__'8866'Nf'8902'__4 → T__'8801'__12 Source #

d_weakenNf'45'renNf_464 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → T_Kind_476 → T__'8866'Nf'8902'__4 → T__'8801'__12 Source #

d_weakenNf'45'subNf_480 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4) → T_Kind_476 → T__'8866'Nf'8902'__4 → T__'8801'__12 Source #

d_weakenNf'91''93'_494 ∷ T_Ctx'8902'_2 → T_Kind_476 → T__'8866'Nf'8902'__4 → T__'8866'Nf'8902'__4 → T__'8801'__12 Source #

d_sub'45'nf'45'Π_510 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4) → T_Kind_476 → T__'8866'Nf'8902'__4 → T__'8801'__12 Source #

d_sub'45'nf'45'μ_528 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Kind_476 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4) → T__'8866'Nf'8902'__4 → T__'8866'Nf'8902'__4 → T__'8801'__12 Source #

d_subNf'45'cons'45''91''93'Nf_548 ∷ T_Ctx'8902'_2 → T_Kind_476 → T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4) → T__'8866'Nf'8902'__4 → T__'8866'Nf'8902'__4 → T__'8801'__12 Source #

d_subNf'8709'_566 ∷ T_Ctx'8902'_2 → T_Kind_476 → T__'8866'Nf'8902'__4 → T__'8866'Nf'8902'__4 Source #

d_subNf'8709''8801'subNf_582 ∷ T_Ctx'8902'_2 → T_Kind_476 → T__'8866'Nf'8902'__4 → T__'8801'__12 Source #

d_subNf'8709''45'renNf_600 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Kind_476 → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → T__'8866'Nf'8902'__4 → T__'8801'__12 Source #

d_subNf'8709''45'subNf_616 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Kind_476 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866'Nf'8902'__4) → T__'8866'Nf'8902'__4 → T__'8801'__12 Source #