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.Relation.Binary.Properties.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.Relation.Binary.Bundles qualified
  import MAlonzo.Code.Relation.Binary.Construct.Composition 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
  
  -- Relation.Binary.Properties.Setoid._._≉_
  d__'8777'__18 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny -> AgdaAny -> ()
  d__'8777'__18 = erased
  -- Relation.Binary.Properties.Setoid.isPreorder
  d_isPreorder_36 ::
    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.Structures.T_IsPreorder_70
  d_isPreorder_36 ~v0 ~v1 v2 = du_isPreorder_36 v2
  du_isPreorder_36 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
  du_isPreorder_36 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_4003
        (coe
           MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_745
           erased erased erased)
        (\ v1 v2 v3 ->
           coe
             MAlonzo.Code.Relation.Binary.Structures.du_reflexive_40
             (coe
                MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0))
             v1)
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_trans_38
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0)))
  -- Relation.Binary.Properties.Setoid.≈-isPreorder
  d_'8776''45'isPreorder_38 ::
    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.Structures.T_IsPreorder_70
  d_'8776''45'isPreorder_38 ~v0 ~v1 v2
    = du_'8776''45'isPreorder_38 v2
  du_'8776''45'isPreorder_38 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
  du_'8776''45'isPreorder_38 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_4003
        (coe
           MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0))
        (coe (\ v1 v2 v3 -> v3))
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_trans_38
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0)))
  -- Relation.Binary.Properties.Setoid.≈-isPartialOrder
  d_'8776''45'isPartialOrder_40 ::
    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.Structures.T_IsPartialOrder_174
  d_'8776''45'isPartialOrder_40 ~v0 ~v1 v2
    = du_'8776''45'isPartialOrder_40 v2
  du_'8776''45'isPartialOrder_40 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
  du_'8776''45'isPartialOrder_40 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_9853
        (coe du_'8776''45'isPreorder_38 (coe v0))
        (coe (\ v1 v2 v3 v4 -> v3))
  -- Relation.Binary.Properties.Setoid.preorder
  d_preorder_46 ::
    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_Preorder_132
  d_preorder_46 ~v0 ~v1 v2 = du_preorder_46 v2
  du_preorder_46 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
  du_preorder_46 v0
    = coe
        MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_2267
        (coe du_isPreorder_36 (coe v0))
  -- Relation.Binary.Properties.Setoid.≈-preorder
  d_'8776''45'preorder_48 ::
    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_Preorder_132
  d_'8776''45'preorder_48 ~v0 ~v1 v2 = du_'8776''45'preorder_48 v2
  du_'8776''45'preorder_48 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
  du_'8776''45'preorder_48 v0
    = coe
        MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_2267
        (coe du_'8776''45'isPreorder_38 (coe v0))
  -- Relation.Binary.Properties.Setoid.≈-poset
  d_'8776''45'poset_50 ::
    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_Poset_314
  d_'8776''45'poset_50 ~v0 ~v1 v2 = du_'8776''45'poset_50 v2
  du_'8776''45'poset_50 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
  du_'8776''45'poset_50 v0
    = coe
        MAlonzo.Code.Relation.Binary.Bundles.C_Poset'46'constructor_6389
        (coe du_'8776''45'isPartialOrder_40 (coe v0))
  -- Relation.Binary.Properties.Setoid.≉-sym
  d_'8777''45'sym_52 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny ->
    (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
  d_'8777''45'sym_52 = erased
  -- Relation.Binary.Properties.Setoid.≉-respˡ
  d_'8777''45'resp'737'_56 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
  d_'8777''45'resp'737'_56 = erased
  -- Relation.Binary.Properties.Setoid.≉-respʳ
  d_'8777''45'resp'691'_62 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
  d_'8777''45'resp'691'_62 = erased
  -- Relation.Binary.Properties.Setoid.≉-resp₂
  d_'8777''45'resp'8322'_70 ::
    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.Builtin.Sigma.T_Σ_14
  d_'8777''45'resp'8322'_70 ~v0 ~v1 ~v2 = du_'8777''45'resp'8322'_70
  du_'8777''45'resp'8322'_70 ::
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_'8777''45'resp'8322'_70
    = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased
  -- Relation.Binary.Properties.Setoid.≉-irrefl
  d_'8777''45'irrefl_72 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
  d_'8777''45'irrefl_72 = erased
  -- Relation.Binary.Properties.Setoid.≈;≈⇒≈
  d_'8776''894''8776''8658''8776'_78 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
  d_'8776''894''8776''8658''8776'_78 ~v0 ~v1 v2 v3 v4
    = du_'8776''894''8776''8658''8776'_78 v2 v3 v4
  du_'8776''894''8776''8658''8776'_78 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
  du_'8776''894''8776''8658''8776'_78 v0 v1 v2
    = coe
        MAlonzo.Code.Relation.Binary.Construct.Composition.du_transitive'8658''8776''894''8776''8838''8776'_366
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_trans_38
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0)))
        (coe v1) (coe v2)
  -- Relation.Binary.Properties.Setoid.≈⇒≈;≈
  d_'8776''8658''8776''894''8776'_80 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8776''8658''8776''894''8776'_80 ~v0 ~v1 v2 v3 v4
    = du_'8776''8658''8776''894''8776'_80 v2 v3 v4
  du_'8776''8658''8776''894''8776'_80 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_'8776''8658''8776''894''8776'_80 v0 v1 v2
    = coe
        MAlonzo.Code.Relation.Binary.Construct.Composition.du_implies'737'_194
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_refl_34
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0)))
        (coe (\ v3 v4 v5 -> v5)) (coe v1) (coe v2)
  -- Relation.Binary.Properties.Setoid.respʳ-flip
  d_resp'691''45'flip_82 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_resp'691''45'flip_82 ~v0 ~v1 v2 v3 v4 v5 v6 v7
    = du_resp'691''45'flip_82 v2 v3 v4 v5 v6 v7
  du_resp'691''45'flip_82 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_resp'691''45'flip_82 v0 v1 v2 v3 v4 v5
    = coe
        MAlonzo.Code.Relation.Binary.Structures.d_trans_38
        (MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0))
        v1 v2 v3 v5
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_sym_36
           (MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0))
           v3 v2 v4)
  -- Relation.Binary.Properties.Setoid.respˡ-flip
  d_resp'737''45'flip_88 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_resp'737''45'flip_88 ~v0 ~v1 v2 v3 v4 v5
    = du_resp'737''45'flip_88 v2 v3 v4 v5
  du_resp'737''45'flip_88 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_resp'737''45'flip_88 v0 v1 v2 v3
    = coe
        MAlonzo.Code.Relation.Binary.Structures.d_trans_38
        (MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0))
        v3 v2 v1
  