Documentation

d_'44''45'injective'737'_42 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #

d_'44''45'injective'691''45''8801'_54 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12) -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #

d_'44''45'injective'691''45'UIP_70 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12) -> T__'8801'__12 -> T__'8801'__12 #

d_'8801''45'dec_78 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T_Dec_20) -> (AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20) -> T_Σ_14 -> T_Σ_14 -> T_Dec_20 #

du_'8801''45'dec_78 :: (AgdaAny -> AgdaAny -> T_Dec_20) -> (AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20) -> T_Σ_14 -> T_Σ_14 -> T_Dec_20 #

d_'44''45'injective'691'_132 :: T_Level_18 -> () -> T_Level_18 -> () -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #

d_'44''45'injective_142 :: T_Level_18 -> () -> T_Level_18 -> () -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T_Σ_14 #

du_'44''45'injective_142 :: T_Σ_14 #

d_map'45'cong_152 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> (AgdaAny -> T__'8801'__12) -> T_Σ_14 -> T__'8801'__12 #

d_swap'45'involutive_162 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Σ_14 -> T__'8801'__12 #

d_Σ'45''8801''44''8801''8594''8801'_190 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14 -> T__'8801'__12 #

d_Σ'45''8801''44''8801''8592''8801'_194 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 -> T__'8801'__12 -> T_Σ_14 #

du_Σ'45''8801''44''8801''8592''8801'_194 :: T_Σ_14 #

d_left'45'inverse'45'of_200 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14 -> T__'8801'__12 #

d_right'45'inverse'45'of_204 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 -> T__'8801'__12 -> T__'8801'__12 #

d_Σ'45''8801''44''8801''8596''8801'_208 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 -> T_Inverse_1960 #

du_Σ'45''8801''44''8801''8596''8801'_208 :: T_Inverse_1960 #

d_'215''45''8801''44''8801''8594''8801'_230 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Σ_14 -> T_Σ_14 -> T_Σ_14 -> T__'8801'__12 #

d_'215''45''8801''44''8801''8592''8801'_232 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Σ_14 -> T_Σ_14 -> T__'8801'__12 -> T_Σ_14 #

du_'215''45''8801''44''8801''8592''8801'_232 :: T_Σ_14 #

d_'215''45''8801''44''8801''8596''8801'_234 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Σ_14 -> T_Σ_14 -> T_Inverse_1960 #

du_'215''45''8801''44''8801''8596''8801'_234 :: T_Inverse_1960 #

d_'46'extendedlambda0_236 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Σ_14 -> T_Σ_14 -> T__'8801'__12 -> T__'8801'__12 #

d_'46'extendedlambda1_238 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Σ_14 -> T_Σ_14 -> T_Σ_14 -> T__'8801'__12 #

d_'8707''8707''8596''8707''8707'_250 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Inverse_1960 #

du_'8707''8707''8596''8707''8707'_250 :: T_Inverse_1960 #

d_to_266 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 #

du_to_266 :: T_Σ_14 -> T_Σ_14 #

d_from_282 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 #

du_from_282 :: T_Σ_14 -> T_Σ_14 #