{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Function.Properties.RightInverse where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Function.Base
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Function.Consequences
import qualified MAlonzo.Code.Function.Structures
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Function.Properties.RightInverse._.Eq₁._≈_
d__'8776'__44 ::
  T_GeneralizeTel_407 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__44 :: T_GeneralizeTel_407
-> T_Equivalence_1714 -> AgdaAny -> AgdaAny -> ()
d__'8776'__44 = T_GeneralizeTel_407
-> T_Equivalence_1714 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Function.Properties.RightInverse._.Eq₂._≈_
d__'8776'__68 ::
  T_GeneralizeTel_407 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__68 :: T_GeneralizeTel_407
-> T_Equivalence_1714 -> AgdaAny -> AgdaAny -> ()
d__'8776'__68 = T_GeneralizeTel_407
-> T_Equivalence_1714 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Function.Properties.RightInverse.mkRightInverse
d_mkRightInverse_90 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
d_mkRightInverse_90 :: ()
-> ()
-> T_Setoid_44
-> ()
-> ()
-> T_Setoid_44
-> T_Equivalence_1714
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_RightInverse_1880
d_mkRightInverse_90 ~()
v0 ~()
v1 ~T_Setoid_44
v2 ~()
v3 ~()
v4 ~T_Setoid_44
v5 T_Equivalence_1714
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7
  = T_Equivalence_1714
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_RightInverse_1880
du_mkRightInverse_90 T_Equivalence_1714
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7
du_mkRightInverse_90 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
du_mkRightInverse_90 :: T_Equivalence_1714
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_RightInverse_1880
du_mkRightInverse_90 T_Equivalence_1714
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_RightInverse_1880)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_RightInverse_1880
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_RightInverse_1880
MAlonzo.Code.Function.Bundles.C_RightInverse'46'constructor_34573
      ((T_Equivalence_1714 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1724 (T_Equivalence_1714 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714
v0))
      ((T_Equivalence_1714 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1726 (T_Equivalence_1714 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714
v0))
      ((T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_1728 (T_Equivalence_1714 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714
v0))
      ((T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1730 (T_Equivalence_1714 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714
v0))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1)
-- Function.Properties.RightInverse.RightInverse⇒LeftInverse
d_RightInverse'8658'LeftInverse_164 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
d_RightInverse'8658'LeftInverse_164 :: ()
-> ()
-> T_Setoid_44
-> ()
-> ()
-> T_Setoid_44
-> T_RightInverse_1880
-> T_LeftInverse_1792
d_RightInverse'8658'LeftInverse_164 ~()
v0 ~()
v1 ~T_Setoid_44
v2 ~()
v3 ~()
v4 ~T_Setoid_44
v5 T_RightInverse_1880
v6
  = T_RightInverse_1880 -> T_LeftInverse_1792
du_RightInverse'8658'LeftInverse_164 T_RightInverse_1880
v6
du_RightInverse'8658'LeftInverse_164 ::
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
du_RightInverse'8658'LeftInverse_164 :: T_RightInverse_1880 -> T_LeftInverse_1792
du_RightInverse'8658'LeftInverse_164 T_RightInverse_1880
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_LeftInverse_1792)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_LeftInverse_1792
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_LeftInverse_1792
MAlonzo.Code.Function.Bundles.C_LeftInverse'46'constructor_29775
      ((T_RightInverse_1880 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1894 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v0))
      ((T_RightInverse_1880 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1892 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v0))
      ((T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1898 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v0))
      ((T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_1896 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v0))
      ((T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_inverse'691'_1900 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v0))
-- Function.Properties.RightInverse.LeftInverse⇒RightInverse
d_LeftInverse'8658'RightInverse_240 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
d_LeftInverse'8658'RightInverse_240 :: ()
-> ()
-> T_Setoid_44
-> ()
-> ()
-> T_Setoid_44
-> T_LeftInverse_1792
-> T_RightInverse_1880
d_LeftInverse'8658'RightInverse_240 ~()
v0 ~()
v1 ~T_Setoid_44
v2 ~()
v3 ~()
v4 ~T_Setoid_44
v5 T_LeftInverse_1792
v6
  = T_LeftInverse_1792 -> T_RightInverse_1880
du_LeftInverse'8658'RightInverse_240 T_LeftInverse_1792
v6
du_LeftInverse'8658'RightInverse_240 ::
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
du_LeftInverse'8658'RightInverse_240 :: T_LeftInverse_1792 -> T_RightInverse_1880
du_LeftInverse'8658'RightInverse_240 T_LeftInverse_1792
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_RightInverse_1880)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_RightInverse_1880
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_RightInverse_1880
MAlonzo.Code.Function.Bundles.C_RightInverse'46'constructor_34573
      ((T_LeftInverse_1792 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1806 (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v0))
      ((T_LeftInverse_1792 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1804 (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v0))
      ((T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1810 (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v0))
      ((T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_1808 (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v0))
      ((T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_inverse'737'_1812 (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v0))
-- Function.Properties.RightInverse.RightInverse⇒Surjection
d_RightInverse'8658'Surjection_322 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
d_RightInverse'8658'Surjection_322 :: ()
-> ()
-> T_Setoid_44
-> ()
-> ()
-> T_Setoid_44
-> T_RightInverse_1880
-> T_Surjection_846
d_RightInverse'8658'Surjection_322 ~()
v0 ~()
v1 ~T_Setoid_44
v2 ~()
v3 ~()
v4 ~T_Setoid_44
v5 T_RightInverse_1880
v6
  = T_RightInverse_1880 -> T_Surjection_846
du_RightInverse'8658'Surjection_322 T_RightInverse_1880
v6
du_RightInverse'8658'Surjection_322 ::
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
du_RightInverse'8658'Surjection_322 :: T_RightInverse_1880 -> T_Surjection_846
du_RightInverse'8658'Surjection_322 T_RightInverse_1880
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> T_Σ_14)
 -> T_Surjection_846)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Surjection_846
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Σ_14)
-> T_Surjection_846
MAlonzo.Code.Function.Bundles.C_Surjection'46'constructor_11197
      ((T_RightInverse_1880 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1894 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v0))
      ((T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1898 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v0))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14
MAlonzo.Code.Function.Consequences.du_inverse'737''8658'surjective_38
         ((T_RightInverse_1880 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1892 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v0))
         ((T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_inverse'691'_1900 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v0)))
-- Function.Properties.RightInverse..generalizedField-S.a
d_'46'generalizedField'45'S'46'a_395 ::
  T_GeneralizeTel_407 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'S'46'a_395 :: T_GeneralizeTel_407 -> ()
d_'46'generalizedField'45'S'46'a_395 T_GeneralizeTel_407
v0
  = case T_GeneralizeTel_407 -> T_GeneralizeTel_407
forall a b. a -> b
coe T_GeneralizeTel_407
v0 of
      C_mkGeneralizeTel_409 ()
v1 ()
v2 T_Setoid_44
v3 ()
v4 ()
v5 T_Setoid_44
v6 -> () -> ()
forall a b. a -> b
coe ()
v1
      T_GeneralizeTel_407
_ -> ()
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.RightInverse..generalizedField-S.ℓ₁
d_'46'generalizedField'45'S'46'ℓ'8321'_397 ::
  T_GeneralizeTel_407 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'S'46'ℓ'8321'_397 :: T_GeneralizeTel_407 -> ()
d_'46'generalizedField'45'S'46'ℓ'8321'_397 T_GeneralizeTel_407
v0
  = case T_GeneralizeTel_407 -> T_GeneralizeTel_407
forall a b. a -> b
coe T_GeneralizeTel_407
v0 of
      C_mkGeneralizeTel_409 ()
v1 ()
v2 T_Setoid_44
v3 ()
v4 ()
v5 T_Setoid_44
v6 -> () -> ()
forall a b. a -> b
coe ()
v2
      T_GeneralizeTel_407
_ -> ()
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.RightInverse.↪⇒↠
d_'8618''8658''8608'_398 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
d_'8618''8658''8608'_398 :: () -> () -> () -> () -> T_RightInverse_1880 -> T_Surjection_846
d_'8618''8658''8608'_398 ~()
v0 ~()
v1 ~()
v2 ~()
v3
  = T_RightInverse_1880 -> T_Surjection_846
du_'8618''8658''8608'_398
du_'8618''8658''8608'_398 ::
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
du_'8618''8658''8608'_398 :: T_RightInverse_1880 -> T_Surjection_846
du_'8618''8658''8608'_398 = (T_RightInverse_1880 -> T_Surjection_846)
-> T_RightInverse_1880 -> T_Surjection_846
forall a b. a -> b
coe T_RightInverse_1880 -> T_Surjection_846
du_RightInverse'8658'Surjection_322
-- Function.Properties.RightInverse..generalizedField-S
d_'46'generalizedField'45'S_399 ::
  T_GeneralizeTel_407 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_'46'generalizedField'45'S_399 :: T_GeneralizeTel_407 -> T_Setoid_44
d_'46'generalizedField'45'S_399 T_GeneralizeTel_407
v0
  = case T_GeneralizeTel_407 -> T_GeneralizeTel_407
forall a b. a -> b
coe T_GeneralizeTel_407
v0 of
      C_mkGeneralizeTel_409 ()
v1 ()
v2 T_Setoid_44
v3 ()
v4 ()
v5 T_Setoid_44
v6 -> T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
v3
      T_GeneralizeTel_407
_ -> T_Setoid_44
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.RightInverse.↪⇒↩
d_'8618''8658''8617'_400 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
d_'8618''8658''8617'_400 :: () -> () -> () -> () -> T_RightInverse_1880 -> T_LeftInverse_1792
d_'8618''8658''8617'_400 ~()
v0 ~()
v1 ~()
v2 ~()
v3
  = T_RightInverse_1880 -> T_LeftInverse_1792
du_'8618''8658''8617'_400
du_'8618''8658''8617'_400 ::
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
du_'8618''8658''8617'_400 :: T_RightInverse_1880 -> T_LeftInverse_1792
du_'8618''8658''8617'_400
  = (T_RightInverse_1880 -> T_LeftInverse_1792)
-> T_RightInverse_1880 -> T_LeftInverse_1792
forall a b. a -> b
coe T_RightInverse_1880 -> T_LeftInverse_1792
du_RightInverse'8658'LeftInverse_164
-- Function.Properties.RightInverse..generalizedField-T.a
d_'46'generalizedField'45'T'46'a_401 ::
  T_GeneralizeTel_407 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'T'46'a_401 :: T_GeneralizeTel_407 -> ()
d_'46'generalizedField'45'T'46'a_401 T_GeneralizeTel_407
v0
  = case T_GeneralizeTel_407 -> T_GeneralizeTel_407
forall a b. a -> b
coe T_GeneralizeTel_407
v0 of
      C_mkGeneralizeTel_409 ()
v1 ()
v2 T_Setoid_44
v3 ()
v4 ()
v5 T_Setoid_44
v6 -> () -> ()
forall a b. a -> b
coe ()
v4
      T_GeneralizeTel_407
_ -> ()
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.RightInverse.↩⇒↪
d_'8617''8658''8618'_402 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
d_'8617''8658''8618'_402 :: () -> () -> () -> () -> T_LeftInverse_1792 -> T_RightInverse_1880
d_'8617''8658''8618'_402 ~()
v0 ~()
v1 ~()
v2 ~()
v3
  = T_LeftInverse_1792 -> T_RightInverse_1880
du_'8617''8658''8618'_402
du_'8617''8658''8618'_402 ::
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
du_'8617''8658''8618'_402 :: T_LeftInverse_1792 -> T_RightInverse_1880
du_'8617''8658''8618'_402
  = (T_LeftInverse_1792 -> T_RightInverse_1880)
-> T_LeftInverse_1792 -> T_RightInverse_1880
forall a b. a -> b
coe T_LeftInverse_1792 -> T_RightInverse_1880
du_LeftInverse'8658'RightInverse_240
-- Function.Properties.RightInverse..generalizedField-T.ℓ₁
d_'46'generalizedField'45'T'46'ℓ'8321'_403 ::
  T_GeneralizeTel_407 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'T'46'ℓ'8321'_403 :: T_GeneralizeTel_407 -> ()
d_'46'generalizedField'45'T'46'ℓ'8321'_403 T_GeneralizeTel_407
v0
  = case T_GeneralizeTel_407 -> T_GeneralizeTel_407
forall a b. a -> b
coe T_GeneralizeTel_407
v0 of
      C_mkGeneralizeTel_409 ()
v1 ()
v2 T_Setoid_44
v3 ()
v4 ()
v5 T_Setoid_44
v6 -> () -> ()
forall a b. a -> b
coe ()
v5
      T_GeneralizeTel_407
_ -> ()
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.RightInverse..generalizedField-T
d_'46'generalizedField'45'T_405 ::
  T_GeneralizeTel_407 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_'46'generalizedField'45'T_405 :: T_GeneralizeTel_407 -> T_Setoid_44
d_'46'generalizedField'45'T_405 T_GeneralizeTel_407
v0
  = case T_GeneralizeTel_407 -> T_GeneralizeTel_407
forall a b. a -> b
coe T_GeneralizeTel_407
v0 of
      C_mkGeneralizeTel_409 ()
v1 ()
v2 T_Setoid_44
v3 ()
v4 ()
v5 T_Setoid_44
v6 -> T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
v6
      T_GeneralizeTel_407
_ -> T_Setoid_44
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.RightInverse.GeneralizeTel
d_GeneralizeTel_407 :: ()
d_GeneralizeTel_407 = ()
data T_GeneralizeTel_407
  = C_mkGeneralizeTel_409 MAlonzo.Code.Agda.Primitive.T_Level_18
                          MAlonzo.Code.Agda.Primitive.T_Level_18
                          MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
                          MAlonzo.Code.Agda.Primitive.T_Level_18
                          MAlonzo.Code.Agda.Primitive.T_Level_18
                          MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
-- Function.Properties.RightInverse._._.Eq₁._≈_
d__'8776'__436 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__436 :: ()
-> ()
-> T_Setoid_44
-> ()
-> ()
-> T_Setoid_44
-> T_RightInverse_1880
-> AgdaAny
-> AgdaAny
-> ()
d__'8776'__436 = ()
-> ()
-> T_Setoid_44
-> ()
-> ()
-> T_Setoid_44
-> T_RightInverse_1880
-> AgdaAny
-> AgdaAny
-> ()
forall a. a
erased
-- Function.Properties.RightInverse._._.Eq₂._≈_
d__'8776'__460 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__460 :: ()
-> ()
-> T_Setoid_44
-> ()
-> ()
-> T_Setoid_44
-> T_RightInverse_1880
-> AgdaAny
-> AgdaAny
-> ()
d__'8776'__460 = ()
-> ()
-> T_Setoid_44
-> ()
-> ()
-> T_Setoid_44
-> T_RightInverse_1880
-> AgdaAny
-> AgdaAny
-> ()
forall a. a
erased
-- Function.Properties.RightInverse._.to-from
d_to'45'from_486 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_to'45'from_486 :: ()
-> ()
-> T_Setoid_44
-> ()
-> ()
-> T_Setoid_44
-> T_RightInverse_1880
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_to'45'from_486 ~()
v0 ~()
v1 T_Setoid_44
v2 ~()
v3 ~()
v4 T_Setoid_44
v5 T_RightInverse_1880
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
  = T_Setoid_44
-> T_Setoid_44
-> T_RightInverse_1880
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_to'45'from_486 T_Setoid_44
v2 T_Setoid_44
v5 T_RightInverse_1880
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
du_to'45'from_486 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_to'45'from_486 :: T_Setoid_44
-> T_Setoid_44
-> T_RightInverse_1880
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_to'45'from_486 T_Setoid_44
v0 T_Setoid_44
v1 T_RightInverse_1880
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
  = let v6 :: t
v6
          = (T_Setoid_44
 -> T_Setoid_44 -> T_RightInverse_1880 -> T_IsRightInverse_408)
-> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
              T_Setoid_44
-> T_Setoid_44 -> T_RightInverse_1880 -> T_IsRightInverse_408
MAlonzo.Code.Function.Bundles.du_isRightInverse_1904 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0)
              (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v1) (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v2) in
    AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (let v7 :: T_IsCongruent_22
v7
             = T_IsRightInverse_408 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_420 (AgdaAny -> T_IsRightInverse_408
forall a b. a -> b
coe AgdaAny
forall a. a
v6) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v8 :: t
v8
                = (T_IsCongruent_22 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_IsCongruent_22 -> T_Setoid_44
MAlonzo.Code.Function.Structures.du_setoid_40 (T_IsCongruent_22 -> AgdaAny
forall a b. a -> b
coe T_IsCongruent_22
v7) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
               (T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (AgdaAny -> T_Setoid_44
forall a b. a -> b
coe AgdaAny
forall a. a
v8))
               (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'45''10216'_'8739'_292
                  (T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1894 (T_RightInverse_1880 -> T_RightInverse_1880
forall a b. a -> b
coe T_RightInverse_1880
v2))
                  (\ AgdaAny
v9 AgdaAny
v10 -> AgdaAny
v9) AgdaAny
v4
                  ((T_RightInverse_1880 -> AgdaAny -> AgdaAny)
-> T_RightInverse_1880 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1892 T_RightInverse_1880
v2 AgdaAny
v3))
               (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du_'8739'_'10217''45'__298
                  (\ AgdaAny
v9 AgdaAny
v10 -> AgdaAny
v10)
                  (T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1894 (T_RightInverse_1880 -> T_RightInverse_1880
forall a b. a -> b
coe T_RightInverse_1880
v2)) AgdaAny
v4
                  ((T_RightInverse_1880 -> AgdaAny -> AgdaAny)
-> T_RightInverse_1880 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1892 T_RightInverse_1880
v2 AgdaAny
v3))
               AgdaAny
v3
               ((T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1898 T_RightInverse_1880
v2 AgdaAny
v4
                  ((T_RightInverse_1880 -> AgdaAny -> AgdaAny)
-> T_RightInverse_1880 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1892 T_RightInverse_1880
v2 AgdaAny
v3)
                  (let v9 :: t
v9
                         = (T_Setoid_44
 -> T_Setoid_44 -> T_RightInverse_1880 -> T_IsRightInverse_408)
-> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
                             T_Setoid_44
-> T_Setoid_44 -> T_RightInverse_1880 -> T_IsRightInverse_408
MAlonzo.Code.Function.Bundles.du_isRightInverse_1904 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0)
                             (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v1) (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v2) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (let v10 :: T_IsCongruent_22
v10
                            = T_IsRightInverse_408 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_420 (AgdaAny -> T_IsRightInverse_408
forall a b. a -> b
coe AgdaAny
forall a. a
v9) in
                      AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        (let v11 :: t
v11
                               = (T_IsCongruent_22 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_IsCongruent_22 -> T_Setoid_44
MAlonzo.Code.Function.Structures.du_setoid_66 (T_IsCongruent_22 -> AgdaAny
forall a b. a -> b
coe T_IsCongruent_22
v10) in
                         AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
                              (T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (AgdaAny -> T_Setoid_44
forall a b. a -> b
coe AgdaAny
forall a. a
v11))
                              ((T_RightInverse_1880 -> AgdaAny -> AgdaAny)
-> T_RightInverse_1880 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1892 T_RightInverse_1880
v2 AgdaAny
v3) AgdaAny
v4 AgdaAny
v5)))))
               (((AgdaAny -> AgdaAny)
 -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.du_strictlyInverse'691'_482
                  ((T_RightInverse_1880 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1892 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v2))
                  ((T_Setoid_44
 -> T_Setoid_44 -> T_RightInverse_1880 -> T_IsRightInverse_408)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Setoid_44
-> T_Setoid_44 -> T_RightInverse_1880 -> T_IsRightInverse_408
MAlonzo.Code.Function.Bundles.du_isRightInverse_1904 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0)
                     (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v1) (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v2))
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)))))