Documentation

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

d_'44''45'injective'691''45''8801'_54 :: T_Level_14 -> () -> T_Level_14 -> (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 Source #

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

d_'8801''45'dec_78 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T_Dec_32) -> (AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_32) -> T_Σ_14 -> T_Σ_14 -> T_Dec_32 Source #

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

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

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

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

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

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

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

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

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

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

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

d_Σ'45''8801''44''8801''8596''8801'_208 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 -> T_Inverse_1052 Source #

du_Σ'45''8801''44''8801''8596''8801'_208 :: T_Inverse_1052 Source #

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

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

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

d_'215''45''8801''44''8801''8596''8801'_234 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Σ_14 -> T_Σ_14 -> T_Inverse_1052 Source #

du_'215''45''8801''44''8801''8596''8801'_234 :: T_Inverse_1052 Source #

d_'8707''8707''8596''8707''8707'_250 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_Inverse_1052 Source #

du_'8707''8707''8596''8707''8707'_250 :: T_Inverse_1052 Source #

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

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

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

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