Documentation

d__'8594''45'setoid__26 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Setoid_44 Source #

du__'8594''45'setoid__26 :: T_Setoid_44 Source #

d__'8791'__36 :: T_Level_14 -> () -> T_Level_14 -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () Source #

d_'58''8594''45'to'45'Π_48 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> T_IndexedSetoid_18 -> (AgdaAny -> AgdaAny) -> T_Π_16 Source #

du_'58''8594''45'to'45'Π_48 :: T_IndexedSetoid_18 -> (AgdaAny -> AgdaAny) -> T_Π_16 Source #

d_'8594''45'to'45''10230'_68 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Π_16 Source #

du_'8594''45'to'45''10230'_68 :: T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Π_16 Source #

d_Reveal_'183'_is__86 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_Reveal_'183'_is__86 Source #

d_eq_100 :: T_Reveal_'183'_is__86 -> T__'8801'__12 Source #

d_inspect_114 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Reveal_'183'_is__86 Source #

d_isPropositional_120 :: T_Level_14 -> () -> () Source #

d_naturality_142 :: T_Level_14 -> () -> T_Level_14 -> () -> AgdaAny -> AgdaAny -> T__'8801'__12 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> T__'8801'__12 Source #

d_cong'45''8801'id_160 :: T_Level_14 -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> T__'8801'__12) -> T__'8801'__12 Source #

d_fx'8801'x_172 :: T_Level_14 -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> T__'8801'__12) -> T__'8801'__12 Source #

d_f'178'x'8801'x_174 :: T_Level_14 -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> T__'8801'__12) -> T__'8801'__12 Source #

d_'8801''45''8799''45'identity_194 :: T_Level_14 -> () -> (AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 Source #

d_'8802''45''8799''45'identity_200 :: T_Level_14 -> () -> (AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> (T__'8801'__12 -> T_'8869'_4) -> T_Σ_14 Source #

du_'8802''45''8799''45'identity_200 :: (AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> T_Σ_14 Source #

d_Extensionality_204 :: T_Level_14 -> T_Level_14 -> () Source #

d_extensionality'45'for'45'lower'45'levels_206 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> (() -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> T__'8801'__12) -> () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> T__'8801'__12 Source #

d_'8704''45'extensionality_208 :: T_Level_14 -> T_Level_14 -> (() -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> T__'8801'__12) -> () -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> T__'8801'__12) -> T__'8801'__12 Source #