content: {-# 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.Consequences.Setoid where
  
  import Data.Text qualified
  import MAlonzo.Code.Agda.Builtin.Sigma qualified
  import MAlonzo.Code.Agda.Primitive qualified
  import MAlonzo.Code.Data.Irrelevant qualified
  import MAlonzo.Code.Function.Consequences qualified
  import MAlonzo.Code.Relation.Binary.Bundles qualified
  import MAlonzo.Code.Relation.Binary.Structures qualified
  import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
                      mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
                      word64ToNat)
  import MAlonzo.RTE qualified
  
  -- Function.Consequences.Setoid.S._≈_
  d__'8776'__20 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny -> AgdaAny -> ()
  d__'8776'__20 = erased
  -- Function.Consequences.Setoid.S.Carrier
  d_Carrier_24 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 -> ()
  d_Carrier_24 = erased
  -- Function.Consequences.Setoid.contraInjective
  d_contraInjective_70 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
  d_contraInjective_70 = erased
  -- Function.Consequences.Setoid.inverseˡ⇒surjective
  d_inverse'737''8658'surjective_72 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_inverse'737''8658'surjective_72 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 v7
    = du_inverse'737''8658'surjective_72 v7
  du_inverse'737''8658'surjective_72 ::
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_inverse'737''8658'surjective_72 v0
    = coe
        MAlonzo.Code.Function.Consequences.du_inverse'737''8658'surjective_38
        (coe v0)
  -- Function.Consequences.Setoid.inverseʳ⇒injective
  d_inverse'691''8658'injective_76 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_inverse'691''8658'injective_76 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7
    = du_inverse'691''8658'injective_76 v4 v5 v6 v7
  du_inverse'691''8658'injective_76 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_inverse'691''8658'injective_76 v0 v1 v2 v3
    = coe
        MAlonzo.Code.Function.Consequences.du_inverse'691''8658'injective_50
        (coe v2) (coe v3)
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_refl_34
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v1)))
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_sym_36
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0)))
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_trans_38
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0)))
  -- Function.Consequences.Setoid.inverseᵇ⇒bijective
  d_inverse'7495''8658'bijective_80 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_inverse'7495''8658'bijective_80 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7
    = du_inverse'7495''8658'bijective_80 v4 v5 v6 v7
  du_inverse'7495''8658'bijective_80 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_inverse'7495''8658'bijective_80 v0 v1 v2 v3
    = coe
        MAlonzo.Code.Function.Consequences.du_inverse'7495''8658'bijective_72
        (coe v2) (coe v3)
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_refl_34
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v1)))
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_sym_36
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0)))
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_trans_38
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0)))
  -- Function.Consequences.Setoid.surjective⇒strictlySurjective
  d_surjective'8658'strictlySurjective_82 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_surjective'8658'strictlySurjective_82 ~v0 ~v1 ~v2 ~v3 v4 ~v5 ~v6
    = du_surjective'8658'strictlySurjective_82 v4
  du_surjective'8658'strictlySurjective_82 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_surjective'8658'strictlySurjective_82 v0
    = coe
        MAlonzo.Code.Function.Consequences.du_surjective'8658'strictlySurjective_90
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_refl_34
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0)))
  -- Function.Consequences.Setoid.strictlySurjective⇒surjective
  d_strictlySurjective'8658'surjective_84 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_strictlySurjective'8658'surjective_84 ~v0 ~v1 ~v2 ~v3 ~v4 v5 v6
    = du_strictlySurjective'8658'surjective_84 v5 v6
  du_strictlySurjective'8658'surjective_84 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_strictlySurjective'8658'surjective_84 v0 v1
    = coe
        MAlonzo.Code.Function.Consequences.du_strictlySurjective'8658'surjective_100
        (coe v1)
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_trans_38
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0)))
  -- Function.Consequences.Setoid.inverseˡ⇒strictlyInverseˡ
  d_inverse'737''8658'strictlyInverse'737'_86 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
  d_inverse'737''8658'strictlyInverse'737'_86 ~v0 ~v1 ~v2 ~v3 v4 ~v5
                                              ~v6 v7
    = du_inverse'737''8658'strictlyInverse'737'_86 v4 v7
  du_inverse'737''8658'strictlyInverse'737'_86 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
  du_inverse'737''8658'strictlyInverse'737'_86 v0 v1
    = coe
        MAlonzo.Code.Function.Consequences.du_inverse'737''8658'strictlyInverse'737'_118
        (coe v1)
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_refl_34
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0)))
  -- Function.Consequences.Setoid.strictlyInverseˡ⇒inverseˡ
  d_strictlyInverse'737''8658'inverse'737'_88 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_strictlyInverse'737''8658'inverse'737'_88 ~v0 ~v1 ~v2 ~v3 ~v4 v5
                                              v6 v7
    = du_strictlyInverse'737''8658'inverse'737'_88 v5 v6 v7
  du_strictlyInverse'737''8658'inverse'737'_88 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_strictlyInverse'737''8658'inverse'737'_88 v0 v1 v2
    = coe
        MAlonzo.Code.Function.Consequences.du_strictlyInverse'737''8658'inverse'737'_126
        (coe v1) (coe v2)
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_trans_38
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0)))
  -- Function.Consequences.Setoid.inverseʳ⇒strictlyInverseʳ
  d_inverse'691''8658'strictlyInverse'691'_90 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
  d_inverse'691''8658'strictlyInverse'691'_90 ~v0 ~v1 ~v2 ~v3 ~v4 v5
                                              v6 ~v7
    = du_inverse'691''8658'strictlyInverse'691'_90 v5 v6
  du_inverse'691''8658'strictlyInverse'691'_90 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
  du_inverse'691''8658'strictlyInverse'691'_90 v0 v1
    = coe
        MAlonzo.Code.Function.Consequences.du_inverse'691''8658'strictlyInverse'691'_142
        (coe v1)
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_refl_34
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0)))
  -- Function.Consequences.Setoid.strictlyInverseʳ⇒inverseʳ
  d_strictlyInverse'691''8658'inverse'691'_92 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_strictlyInverse'691''8658'inverse'691'_92 ~v0 ~v1 ~v2 ~v3 v4 ~v5
                                              v6 v7
    = du_strictlyInverse'691''8658'inverse'691'_92 v4 v6 v7
  du_strictlyInverse'691''8658'inverse'691'_92 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_strictlyInverse'691''8658'inverse'691'_92 v0 v1 v2
    = coe
        MAlonzo.Code.Function.Consequences.du_strictlyInverse'691''8658'inverse'691'_150
        (coe v1) (coe v2)
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_trans_38
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0)))
  