Documentation

d_'8660'_36 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Equivalence_16 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Equivalence_16 Source #

du_'8660'_36 :: T_Equivalence_16 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Equivalence_16 Source #

d_'8660''45''8608'_52 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Surjection_54 -> (AgdaAny -> T_Equivalence_16) -> T_Equivalence_16 Source #

du_'8660''45''8608'_52 :: T_Surjection_54 -> (AgdaAny -> T_Equivalence_16) -> T_Equivalence_16 Source #

d_'8611'_70 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> T_Injection_88 Source #

du_'8611'_70 :: T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> T_Injection_88 Source #

d_A'8321''8771'A'8322'_80 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> T__'8771'__12 Source #

du_A'8321''8771'A'8322'_80 :: T_Inverse_58 -> T__'8771'__12 Source #

d_from_84 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> AgdaAny -> AgdaAny Source #

du_from_84 :: T_Inverse_58 -> AgdaAny -> AgdaAny Source #

d_to_96 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> AgdaAny -> AgdaAny Source #

du_to_96 :: T_Inverse_58 -> AgdaAny -> AgdaAny Source #

d_subst'45'application'8242'_110 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> AgdaAny -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T__'8801'__12 -> T__'8801'__12 Source #

d_from_128 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> AgdaAny -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T__'8801'__12 -> AgdaAny -> AgdaAny Source #

du_from_128 :: T_Inverse_58 -> AgdaAny -> AgdaAny Source #

d_to_140 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> AgdaAny -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T__'8801'__12 -> AgdaAny -> AgdaAny Source #

du_to_140 :: T_Inverse_58 -> AgdaAny -> AgdaAny Source #

d_g'8242'_144 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> AgdaAny -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T__'8801'__12 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_g'8242'_144 :: T_Inverse_58 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_g'8242''45'lemma_152 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> AgdaAny -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T__'8801'__12 -> AgdaAny -> AgdaAny -> T__'8801'__12 Source #

d_lemma_168 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> AgdaAny -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T__'8801'__12 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> T__'8801'__12 Source #

d_to_172 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> T_Σ_14 -> T_Σ_14 Source #

du_to_172 :: T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> T_Σ_14 -> T_Σ_14 Source #

d_to'45'injective_176 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> T_Σ_14 -> T_Σ_14 -> T__'8801'__12 -> T__'8801'__12 Source #

d_'8606'_210 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_LeftInverse_82 -> (AgdaAny -> T_LeftInverse_82) -> T_LeftInverse_82 Source #

du_'8606'_210 :: T_LeftInverse_82 -> (AgdaAny -> T_LeftInverse_82) -> T_LeftInverse_82 Source #

d_from_220 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_LeftInverse_82 -> (AgdaAny -> T_LeftInverse_82) -> T_Σ_14 -> T_Σ_14 Source #

du_from_220 :: T_LeftInverse_82 -> (AgdaAny -> T_LeftInverse_82) -> T_Σ_14 -> T_Σ_14 Source #

d_to_226 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_LeftInverse_82 -> (AgdaAny -> T_LeftInverse_82) -> T_Σ_14 -> T_Σ_14 Source #

du_to_226 :: T_LeftInverse_82 -> (AgdaAny -> T_LeftInverse_82) -> T_Σ_14 -> T_Σ_14 Source #

d_left'45'inverse'45'of_236 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_LeftInverse_82 -> (AgdaAny -> T_LeftInverse_82) -> T_Σ_14 -> T__'8801'__12 Source #

d_'8608'_246 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Surjection_54 -> (AgdaAny -> T_Surjection_54) -> T_Surjection_54 Source #

du_'8608'_246 :: T_Surjection_54 -> (AgdaAny -> T_Surjection_54) -> T_Surjection_54 Source #

d_to_256 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Surjection_54 -> (AgdaAny -> T_Surjection_54) -> T_Σ_14 -> T_Σ_14 Source #

du_to_256 :: T_Surjection_54 -> (AgdaAny -> T_Surjection_54) -> T_Σ_14 -> T_Σ_14 Source #

d_from_262 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Surjection_54 -> (AgdaAny -> T_Surjection_54) -> T_Σ_14 -> T_Σ_14 Source #

du_from_262 :: T_Surjection_54 -> (AgdaAny -> T_Surjection_54) -> T_Σ_14 -> T_Σ_14 Source #

d_right'45'inverse'45'of_272 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Surjection_54 -> (AgdaAny -> T_Surjection_54) -> T_Σ_14 -> T__'8801'__12 Source #

d_'8596'_282 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Inverse_58 -> (AgdaAny -> T_Inverse_58) -> T_Inverse_58 Source #

du_'8596'_282 :: T_Inverse_58 -> (AgdaAny -> T_Inverse_58) -> T_Inverse_58 Source #

d_A'8321''8771'A'8322'_292 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Inverse_58 -> (AgdaAny -> T_Inverse_58) -> T__'8771'__12 Source #

du_A'8321''8771'A'8322'_292 :: T_Inverse_58 -> T__'8771'__12 Source #

d_surjection'8242'_294 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Inverse_58 -> (AgdaAny -> T_Inverse_58) -> T_Surjection_54 Source #

du_surjection'8242'_294 :: T_Inverse_58 -> (AgdaAny -> T_Inverse_58) -> T_Surjection_54 Source #

d_left'45'inverse'45'of_298 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Inverse_58 -> (AgdaAny -> T_Inverse_58) -> T_Σ_14 -> T__'8801'__12 Source #

d_swap'45'coercions_340 :: T_Kind_6 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Inverse_58 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny Source #

du_swap'45'coercions_340 :: T_Kind_6 -> T_Inverse_58 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny Source #

d_cong_380 :: T_Kind_6 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> T_Inverse_58 -> (AgdaAny -> AgdaAny) -> AgdaAny Source #

du_cong_380 :: T_Kind_6 -> T_Inverse_58 -> (AgdaAny -> AgdaAny) -> AgdaAny Source #