{-# 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_487 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__44 :: T_GeneralizeTel_487
-> T_Equivalence_1858 -> AgdaAny -> AgdaAny -> ()
d__'8776'__44 = T_GeneralizeTel_487
-> T_Equivalence_1858 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Function.Properties.RightInverse._.Eq₂._≈_
d__'8776'__70 ::
  T_GeneralizeTel_487 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__70 :: T_GeneralizeTel_487
-> T_Equivalence_1858 -> AgdaAny -> AgdaAny -> ()
d__'8776'__70 = T_GeneralizeTel_487
-> T_Equivalence_1858 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Function.Properties.RightInverse.mkRightInverse
d_mkRightInverse_94 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036
d_mkRightInverse_94 :: ()
-> ()
-> T_Setoid_46
-> ()
-> ()
-> T_Setoid_46
-> T_Equivalence_1858
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_RightInverse_2036
d_mkRightInverse_94 ~()
v0 ~()
v1 ~T_Setoid_46
v2 ~()
v3 ~()
v4 ~T_Setoid_46
v5 T_Equivalence_1858
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7
  = T_Equivalence_1858
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_RightInverse_2036
du_mkRightInverse_94 T_Equivalence_1858
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7
du_mkRightInverse_94 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036
du_mkRightInverse_94 :: T_Equivalence_1858
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_RightInverse_2036
du_mkRightInverse_94 T_Equivalence_1858
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_RightInverse_2036)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_RightInverse_2036
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_RightInverse_2036
MAlonzo.Code.Function.Bundles.C_constructor_2120
      ((T_Equivalence_1858 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1868 (T_Equivalence_1858 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858
v0))
      ((T_Equivalence_1858 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1870 (T_Equivalence_1858 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858
v0))
      ((T_Equivalence_1858 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_1872 (T_Equivalence_1858 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858
v0))
      ((T_Equivalence_1858 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1874 (T_Equivalence_1858 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858
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_172 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942
d_RightInverse'8658'LeftInverse_172 :: ()
-> ()
-> T_Setoid_46
-> ()
-> ()
-> T_Setoid_46
-> T_RightInverse_2036
-> T_LeftInverse_1942
d_RightInverse'8658'LeftInverse_172 ~()
v0 ~()
v1 ~T_Setoid_46
v2 ~()
v3 ~()
v4 ~T_Setoid_46
v5 T_RightInverse_2036
v6
  = T_RightInverse_2036 -> T_LeftInverse_1942
du_RightInverse'8658'LeftInverse_172 T_RightInverse_2036
v6
du_RightInverse'8658'LeftInverse_172 ::
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942
du_RightInverse'8658'LeftInverse_172 :: T_RightInverse_2036 -> T_LeftInverse_1942
du_RightInverse'8658'LeftInverse_172 T_RightInverse_2036
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_LeftInverse_1942)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_LeftInverse_1942
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_LeftInverse_1942
MAlonzo.Code.Function.Bundles.C_constructor_2034
      ((T_RightInverse_2036 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_2050 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v0))
      ((T_RightInverse_2036 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_2048 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v0))
      ((T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_2054 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v0))
      ((T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_2052 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v0))
      ((T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_inverse'691'_2056 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v0))
-- Function.Properties.RightInverse.LeftInverse⇒RightInverse
d_LeftInverse'8658'RightInverse_252 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036
d_LeftInverse'8658'RightInverse_252 :: ()
-> ()
-> T_Setoid_46
-> ()
-> ()
-> T_Setoid_46
-> T_LeftInverse_1942
-> T_RightInverse_2036
d_LeftInverse'8658'RightInverse_252 ~()
v0 ~()
v1 ~T_Setoid_46
v2 ~()
v3 ~()
v4 ~T_Setoid_46
v5 T_LeftInverse_1942
v6
  = T_LeftInverse_1942 -> T_RightInverse_2036
du_LeftInverse'8658'RightInverse_252 T_LeftInverse_1942
v6
du_LeftInverse'8658'RightInverse_252 ::
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036
du_LeftInverse'8658'RightInverse_252 :: T_LeftInverse_1942 -> T_RightInverse_2036
du_LeftInverse'8658'RightInverse_252 T_LeftInverse_1942
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_RightInverse_2036)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_RightInverse_2036
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_RightInverse_2036
MAlonzo.Code.Function.Bundles.C_constructor_2120
      ((T_LeftInverse_1942 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1956 (T_LeftInverse_1942 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942
v0))
      ((T_LeftInverse_1942 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1954 (T_LeftInverse_1942 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942
v0))
      ((T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1960 (T_LeftInverse_1942 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942
v0))
      ((T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_1958 (T_LeftInverse_1942 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942
v0))
      ((T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_inverse'737'_1962 (T_LeftInverse_1942 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942
v0))
-- Function.Properties.RightInverse.RightInverse⇒Surjection
d_RightInverse'8658'Surjection_338 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_918
d_RightInverse'8658'Surjection_338 :: ()
-> ()
-> T_Setoid_46
-> ()
-> ()
-> T_Setoid_46
-> T_RightInverse_2036
-> T_Surjection_918
d_RightInverse'8658'Surjection_338 ~()
v0 ~()
v1 ~T_Setoid_46
v2 ~()
v3 ~()
v4 ~T_Setoid_46
v5 T_RightInverse_2036
v6
  = T_RightInverse_2036 -> T_Surjection_918
du_RightInverse'8658'Surjection_338 T_RightInverse_2036
v6
du_RightInverse'8658'Surjection_338 ::
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_918
du_RightInverse'8658'Surjection_338 :: T_RightInverse_2036 -> T_Surjection_918
du_RightInverse'8658'Surjection_338 T_RightInverse_2036
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> T_Σ_14)
 -> T_Surjection_918)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Surjection_918
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Σ_14)
-> T_Surjection_918
MAlonzo.Code.Function.Bundles.C_constructor_1002
      ((T_RightInverse_2036 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_2050 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v0))
      ((T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_2054 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
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_2036 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_2048 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v0))
         ((T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_inverse'691'_2056 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v0)))
-- Function.Properties.RightInverse.↪⇒↠
d_'8618''8658''8608'_418 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_918
d_'8618''8658''8608'_418 :: () -> () -> () -> () -> T_RightInverse_2036 -> T_Surjection_918
d_'8618''8658''8608'_418 ~()
v0 ~()
v1 ~()
v2 ~()
v3
  = T_RightInverse_2036 -> T_Surjection_918
du_'8618''8658''8608'_418
du_'8618''8658''8608'_418 ::
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_918
du_'8618''8658''8608'_418 :: T_RightInverse_2036 -> T_Surjection_918
du_'8618''8658''8608'_418 = (T_RightInverse_2036 -> T_Surjection_918)
-> T_RightInverse_2036 -> T_Surjection_918
forall a b. a -> b
coe T_RightInverse_2036 -> T_Surjection_918
du_RightInverse'8658'Surjection_338
-- Function.Properties.RightInverse.↪⇒↩
d_'8618''8658''8617'_420 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942
d_'8618''8658''8617'_420 :: () -> () -> () -> () -> T_RightInverse_2036 -> T_LeftInverse_1942
d_'8618''8658''8617'_420 ~()
v0 ~()
v1 ~()
v2 ~()
v3
  = T_RightInverse_2036 -> T_LeftInverse_1942
du_'8618''8658''8617'_420
du_'8618''8658''8617'_420 ::
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942
du_'8618''8658''8617'_420 :: T_RightInverse_2036 -> T_LeftInverse_1942
du_'8618''8658''8617'_420
  = (T_RightInverse_2036 -> T_LeftInverse_1942)
-> T_RightInverse_2036 -> T_LeftInverse_1942
forall a b. a -> b
coe T_RightInverse_2036 -> T_LeftInverse_1942
du_RightInverse'8658'LeftInverse_172
-- Function.Properties.RightInverse.↩⇒↪
d_'8617''8658''8618'_422 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036
d_'8617''8658''8618'_422 :: () -> () -> () -> () -> T_LeftInverse_1942 -> T_RightInverse_2036
d_'8617''8658''8618'_422 ~()
v0 ~()
v1 ~()
v2 ~()
v3
  = T_LeftInverse_1942 -> T_RightInverse_2036
du_'8617''8658''8618'_422
du_'8617''8658''8618'_422 ::
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036
du_'8617''8658''8618'_422 :: T_LeftInverse_1942 -> T_RightInverse_2036
du_'8617''8658''8618'_422
  = (T_LeftInverse_1942 -> T_RightInverse_2036)
-> T_LeftInverse_1942 -> T_RightInverse_2036
forall a b. a -> b
coe T_LeftInverse_1942 -> T_RightInverse_2036
du_LeftInverse'8658'RightInverse_252
-- Function.Properties.RightInverse._._.Eq₁._≈_
d__'8776'__456 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__456 :: ()
-> ()
-> T_Setoid_46
-> ()
-> ()
-> T_Setoid_46
-> T_RightInverse_2036
-> AgdaAny
-> AgdaAny
-> ()
d__'8776'__456 = ()
-> ()
-> T_Setoid_46
-> ()
-> ()
-> T_Setoid_46
-> T_RightInverse_2036
-> AgdaAny
-> AgdaAny
-> ()
forall a. a
erased
-- Function.Properties.RightInverse..generalizedField-S.a
d_'46'generalizedField'45'S'46'a_475 ::
  T_GeneralizeTel_487 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'S'46'a_475 :: T_GeneralizeTel_487 -> ()
d_'46'generalizedField'45'S'46'a_475 T_GeneralizeTel_487
v0
  = case T_GeneralizeTel_487 -> T_GeneralizeTel_487
forall a b. a -> b
coe T_GeneralizeTel_487
v0 of
      C_mkGeneralizeTel_489 ()
v1 ()
v2 T_Setoid_46
v3 ()
v4 ()
v5 T_Setoid_46
v6 -> () -> ()
forall a b. a -> b
coe ()
v1
      T_GeneralizeTel_487
_ -> ()
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.RightInverse..generalizedField-S.ℓ₁
d_'46'generalizedField'45'S'46'ℓ'8321'_477 ::
  T_GeneralizeTel_487 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'S'46'ℓ'8321'_477 :: T_GeneralizeTel_487 -> ()
d_'46'generalizedField'45'S'46'ℓ'8321'_477 T_GeneralizeTel_487
v0
  = case T_GeneralizeTel_487 -> T_GeneralizeTel_487
forall a b. a -> b
coe T_GeneralizeTel_487
v0 of
      C_mkGeneralizeTel_489 ()
v1 ()
v2 T_Setoid_46
v3 ()
v4 ()
v5 T_Setoid_46
v6 -> () -> ()
forall a b. a -> b
coe ()
v2
      T_GeneralizeTel_487
_ -> ()
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.RightInverse..generalizedField-S
d_'46'generalizedField'45'S_479 ::
  T_GeneralizeTel_487 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46
d_'46'generalizedField'45'S_479 :: T_GeneralizeTel_487 -> T_Setoid_46
d_'46'generalizedField'45'S_479 T_GeneralizeTel_487
v0
  = case T_GeneralizeTel_487 -> T_GeneralizeTel_487
forall a b. a -> b
coe T_GeneralizeTel_487
v0 of
      C_mkGeneralizeTel_489 ()
v1 ()
v2 T_Setoid_46
v3 ()
v4 ()
v5 T_Setoid_46
v6 -> T_Setoid_46 -> T_Setoid_46
forall a b. a -> b
coe T_Setoid_46
v3
      T_GeneralizeTel_487
_ -> T_Setoid_46
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.RightInverse..generalizedField-T.a
d_'46'generalizedField'45'T'46'a_481 ::
  T_GeneralizeTel_487 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'T'46'a_481 :: T_GeneralizeTel_487 -> ()
d_'46'generalizedField'45'T'46'a_481 T_GeneralizeTel_487
v0
  = case T_GeneralizeTel_487 -> T_GeneralizeTel_487
forall a b. a -> b
coe T_GeneralizeTel_487
v0 of
      C_mkGeneralizeTel_489 ()
v1 ()
v2 T_Setoid_46
v3 ()
v4 ()
v5 T_Setoid_46
v6 -> () -> ()
forall a b. a -> b
coe ()
v4
      T_GeneralizeTel_487
_ -> ()
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.RightInverse._._.Eq₂._≈_
d__'8776'__482 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__482 :: ()
-> ()
-> T_Setoid_46
-> ()
-> ()
-> T_Setoid_46
-> T_RightInverse_2036
-> AgdaAny
-> AgdaAny
-> ()
d__'8776'__482 = ()
-> ()
-> T_Setoid_46
-> ()
-> ()
-> T_Setoid_46
-> T_RightInverse_2036
-> AgdaAny
-> AgdaAny
-> ()
forall a. a
erased
-- Function.Properties.RightInverse..generalizedField-T.ℓ₁
d_'46'generalizedField'45'T'46'ℓ'8321'_483 ::
  T_GeneralizeTel_487 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'T'46'ℓ'8321'_483 :: T_GeneralizeTel_487 -> ()
d_'46'generalizedField'45'T'46'ℓ'8321'_483 T_GeneralizeTel_487
v0
  = case T_GeneralizeTel_487 -> T_GeneralizeTel_487
forall a b. a -> b
coe T_GeneralizeTel_487
v0 of
      C_mkGeneralizeTel_489 ()
v1 ()
v2 T_Setoid_46
v3 ()
v4 ()
v5 T_Setoid_46
v6 -> () -> ()
forall a b. a -> b
coe ()
v5
      T_GeneralizeTel_487
_ -> ()
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.RightInverse..generalizedField-T
d_'46'generalizedField'45'T_485 ::
  T_GeneralizeTel_487 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46
d_'46'generalizedField'45'T_485 :: T_GeneralizeTel_487 -> T_Setoid_46
d_'46'generalizedField'45'T_485 T_GeneralizeTel_487
v0
  = case T_GeneralizeTel_487 -> T_GeneralizeTel_487
forall a b. a -> b
coe T_GeneralizeTel_487
v0 of
      C_mkGeneralizeTel_489 ()
v1 ()
v2 T_Setoid_46
v3 ()
v4 ()
v5 T_Setoid_46
v6 -> T_Setoid_46 -> T_Setoid_46
forall a b. a -> b
coe T_Setoid_46
v6
      T_GeneralizeTel_487
_ -> T_Setoid_46
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Properties.RightInverse.GeneralizeTel
d_GeneralizeTel_487 :: ()
d_GeneralizeTel_487 = ()
data T_GeneralizeTel_487
  = C_mkGeneralizeTel_489 MAlonzo.Code.Agda.Primitive.T_Level_18
                          MAlonzo.Code.Agda.Primitive.T_Level_18
                          MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46
                          MAlonzo.Code.Agda.Primitive.T_Level_18
                          MAlonzo.Code.Agda.Primitive.T_Level_18
                          MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46
-- Function.Properties.RightInverse._.to-from
d_to'45'from_510 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_to'45'from_510 :: ()
-> ()
-> T_Setoid_46
-> ()
-> ()
-> T_Setoid_46
-> T_RightInverse_2036
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_to'45'from_510 ~()
v0 ~()
v1 T_Setoid_46
v2 ~()
v3 ~()
v4 T_Setoid_46
v5 T_RightInverse_2036
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
  = T_Setoid_46
-> T_Setoid_46
-> T_RightInverse_2036
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_to'45'from_510 T_Setoid_46
v2 T_Setoid_46
v5 T_RightInverse_2036
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
du_to'45'from_510 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_to'45'from_510 :: T_Setoid_46
-> T_Setoid_46
-> T_RightInverse_2036
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_to'45'from_510 T_Setoid_46
v0 T_Setoid_46
v1 T_RightInverse_2036
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
  = (T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
      (T_Setoid_46 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_62 (T_Setoid_46 -> T_Setoid_46
forall a b. a -> b
coe T_Setoid_46
v0))
      (((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_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_2050 (T_RightInverse_2036 -> T_RightInverse_2036
forall a b. a -> b
coe T_RightInverse_2036
v2))
         (\ AgdaAny
v6 AgdaAny
v7 -> AgdaAny
v6) AgdaAny
v4
         ((T_RightInverse_2036 -> AgdaAny -> AgdaAny)
-> T_RightInverse_2036 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_2048 T_RightInverse_2036
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
v6 AgdaAny
v7 -> AgdaAny
v7)
         (T_RightInverse_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_2050 (T_RightInverse_2036 -> T_RightInverse_2036
forall a b. a -> b
coe T_RightInverse_2036
v2)) AgdaAny
v4
         ((T_RightInverse_2036 -> AgdaAny -> AgdaAny)
-> T_RightInverse_2036 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_2048 T_RightInverse_2036
v2 AgdaAny
v3))
      AgdaAny
v3
      ((T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_2054 T_RightInverse_2036
v2 AgdaAny
v4
         ((T_RightInverse_2036 -> AgdaAny -> AgdaAny)
-> T_RightInverse_2036 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_2048 T_RightInverse_2036
v2 AgdaAny
v3)
         ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
            (T_Setoid_46 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_62 (T_Setoid_46 -> T_Setoid_46
forall a b. a -> b
coe T_Setoid_46
v1))
            ((T_RightInverse_2036 -> AgdaAny -> AgdaAny)
-> T_RightInverse_2036 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_2048 T_RightInverse_2036
v2 AgdaAny
v3) AgdaAny
v4 AgdaAny
v5))
      (((AgdaAny -> AgdaAny)
 -> T_IsRightInverse_438 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> T_IsRightInverse_438 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.du_strictlyInverse'691'_516
         ((T_RightInverse_2036 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_2048 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v2))
         ((T_Setoid_46
 -> T_Setoid_46 -> T_RightInverse_2036 -> T_IsRightInverse_438)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_46
-> T_Setoid_46 -> T_RightInverse_2036 -> T_IsRightInverse_438
MAlonzo.Code.Function.Bundles.du_isRightInverse_2060 (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe T_Setoid_46
v0)
            (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe T_Setoid_46
v1) (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v2))
         (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))