Documentation

d_Ren_4 ∷ () → () → () Source #

d_lift_14 ∷ () → () → (AgdaAny → AgdaAny) → Maybe AgdaAny → Maybe AgdaAny Source #

du_lift_14 ∷ (AgdaAny → AgdaAny) → Maybe AgdaAny → Maybe AgdaAny Source #

d_renList_26 ∷ () → () → (AgdaAny → AgdaAny) → [T__'8866'_14] → [T__'8866'_14] Source #

du_renList_26 ∷ (AgdaAny → AgdaAny) → [T__'8866'_14] → [T__'8866'_14] Source #

d_ren_32 ∷ () → () → (AgdaAny → AgdaAny) → T__'8866'_14 → T__'8866'_14 Source #

du_ren_32 ∷ (AgdaAny → AgdaAny) → T__'8866'_14 → T__'8866'_14 Source #

d_weaken_88 ∷ () → T__'8866'_14 → T__'8866'_14 Source #

du_weaken_88 ∷ T__'8866'_14 → T__'8866'_14 Source #

d_lift'45'cong_104 ∷ () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → Maybe AgdaAny → T__'8801'__12 Source #

d_renList'45'cong_124 ∷ () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → [T__'8866'_14] → T__'8801'__12 Source #

d_ren'45'cong_138 ∷ () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → T__'8866'_14 → T__'8801'__12 Source #

d_lift'45'id_196 ∷ () → Maybe AgdaAny → T__'8801'__12 Source #

d_lift'45'comp_212 ∷ () → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → Maybe AgdaAny → T__'8801'__12 Source #

d_renList'45'id_228 ∷ () → [T__'8866'_14] → T__'8801'__12 Source #

d_ren'45'id_234 ∷ () → T__'8866'_14 → T__'8801'__12 Source #

d_renList'45'comp_276 ∷ () → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → [T__'8866'_14] → T__'8801'__12 Source #

d_ren'45'comp_290 ∷ () → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T__'8866'_14 → T__'8801'__12 Source #

d_Sub_368 ∷ () → () → () Source #

d_lifts_378 ∷ () → () → (AgdaAny → T__'8866'_14) → Maybe AgdaAny → T__'8866'_14 Source #

du_lifts_378 ∷ (AgdaAny → T__'8866'_14) → Maybe AgdaAny → T__'8866'_14 Source #

d_subList_390 ∷ () → () → (AgdaAny → T__'8866'_14) → [T__'8866'_14] → [T__'8866'_14] Source #

du_subList_390 ∷ (AgdaAny → T__'8866'_14) → [T__'8866'_14] → [T__'8866'_14] Source #

d_sub_396 ∷ () → () → (AgdaAny → T__'8866'_14) → T__'8866'_14 → T__'8866'_14 Source #

du_sub_396 ∷ (AgdaAny → T__'8866'_14) → T__'8866'_14 → T__'8866'_14 Source #

d_extend_454 ∷ () → () → (AgdaAny → T__'8866'_14) → T__'8866'_14 → Maybe AgdaAny → T__'8866'_14 Source #

du_extend_454 ∷ (AgdaAny → T__'8866'_14) → T__'8866'_14 → Maybe AgdaAny → T__'8866'_14 Source #

d__'91'_'93'_468 ∷ () → T__'8866'_14 → T__'8866'_14 → T__'8866'_14 Source #

du__'91'_'93'_468 ∷ T__'8866'_14 → T__'8866'_14 → T__'8866'_14 Source #

d_lifts'45'cong_486 ∷ () → () → (AgdaAny → T__'8866'_14) → (AgdaAny → T__'8866'_14) → (AgdaAny → T__'8801'__12) → Maybe AgdaAny → T__'8801'__12 Source #

d_subList'45'cong_506 ∷ () → () → (AgdaAny → T__'8866'_14) → (AgdaAny → T__'8866'_14) → (AgdaAny → T__'8801'__12) → [T__'8866'_14] → T__'8801'__12 Source #

d_sub'45'cong_520 ∷ () → () → (AgdaAny → T__'8866'_14) → (AgdaAny → T__'8866'_14) → (AgdaAny → T__'8801'__12) → T__'8866'_14 → T__'8801'__12 Source #

d_lifts'45'id_578 ∷ () → Maybe AgdaAny → T__'8801'__12 Source #

d_subList'45'id_586 ∷ () → [T__'8866'_14] → T__'8801'__12 Source #

d_sub'45'id_592 ∷ () → T__'8866'_14 → T__'8801'__12 Source #

d_lifts'45'lift_634 ∷ () → () → () → (AgdaAny → AgdaAny) → (AgdaAny → T__'8866'_14) → Maybe AgdaAny → T__'8801'__12 Source #

d_subList'45'ren_658 ∷ () → () → () → (AgdaAny → AgdaAny) → (AgdaAny → T__'8866'_14) → [T__'8866'_14] → T__'8801'__12 Source #

d_sub'45'ren_672 ∷ () → () → () → (AgdaAny → AgdaAny) → (AgdaAny → T__'8866'_14) → T__'8866'_14 → T__'8801'__12 Source #

d_ren'45'lift'45'lifts_762 ∷ () → () → () → (AgdaAny → T__'8866'_14) → (AgdaAny → AgdaAny) → Maybe AgdaAny → T__'8801'__12 Source #

d_renList'45'sub_786 ∷ () → () → () → (AgdaAny → T__'8866'_14) → (AgdaAny → AgdaAny) → [T__'8866'_14] → T__'8801'__12 Source #

d_ren'45'sub_800 ∷ () → () → () → (AgdaAny → T__'8866'_14) → (AgdaAny → AgdaAny) → T__'8866'_14 → T__'8801'__12 Source #

d_lifts'45'comp_890 ∷ () → () → () → (AgdaAny → T__'8866'_14) → (AgdaAny → T__'8866'_14) → Maybe AgdaAny → T__'8801'__12 Source #

d_subList'45'comp_914 ∷ () → () → () → (AgdaAny → T__'8866'_14) → (AgdaAny → T__'8866'_14) → [T__'8866'_14] → T__'8801'__12 Source #

d_sub'45'comp_928 ∷ () → () → () → (AgdaAny → T__'8866'_14) → (AgdaAny → T__'8866'_14) → T__'8866'_14 → T__'8801'__12 Source #