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.Construct.Intersection 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.Data.Product.Base qualified
  import MAlonzo.Code.Data.Sum.Base qualified
  import MAlonzo.Code.Relation.Binary.Structures qualified
  import MAlonzo.Code.Relation.Nullary.Decidable.Core 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.Construct.Intersection._∩_
  d__'8745'__28 ::
    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 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> ()
  d__'8745'__28 = erased
  -- Relation.Binary.Construct.Intersection._.reflexive
  d_reflexive_52 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_reflexive_52 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8
    = du_reflexive_52 v6 v7 v8
  du_reflexive_52 ::
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_reflexive_52 v0 v1 v2
    = coe
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v0 v2) (coe v1 v2)
  -- Relation.Binary.Construct.Intersection._.symmetric
  d_symmetric_58 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_symmetric_58 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9
    = du_symmetric_58 v6 v7 v8 v9
  du_symmetric_58 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_symmetric_58 v0 v1 v2 v3
    = coe
        MAlonzo.Code.Data.Product.Base.du_map_128 (coe v0 v2 v3)
        (coe (\ v4 -> coe v1 v2 v3))
  -- Relation.Binary.Construct.Intersection._.transitive
  d_transitive_64 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_transitive_64 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9 v10
    = du_transitive_64 v6 v7 v8 v9 v10
  du_transitive_64 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_transitive_64 v0 v1 v2 v3 v4
    = coe
        MAlonzo.Code.Data.Product.Base.du_zip_198 (coe v0 v2 v3 v4)
        (coe (\ v5 v6 -> coe v1 v2 v3 v4))
  -- Relation.Binary.Construct.Intersection._.respects
  d_respects_74 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny -> AgdaAny
  d_respects_74 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8 v9 v10 v11
    = du_respects_74 v8 v9 v10 v11
  du_respects_74 ::
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny -> AgdaAny
  du_respects_74 v0 v1 v2 v3
    = case coe v3 of
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v4 v5
          -> coe
               MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93'_52
               (coe (\ v6 -> coe v6 v1 v2 v4)) (coe (\ v6 -> coe v6 v1 v2 v5))
               (coe v0)
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Relation.Binary.Construct.Intersection._.min
  d_min_90 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    AgdaAny ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_min_90 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 v7 v8 = du_min_90 v7 v8
  du_min_90 ::
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_min_90 v0 v1
    = coe
        MAlonzo.Code.Data.Product.Base.du_'60'_'44'_'62'_112 (coe v0)
        (coe v1)
  -- Relation.Binary.Construct.Intersection._.max
  d_max_98 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    AgdaAny ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_max_98 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 v7 v8 = du_max_98 v7 v8
  du_max_98 ::
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_max_98 v0 v1
    = coe
        MAlonzo.Code.Data.Product.Base.du_'60'_'44'_'62'_112 (coe v0)
        (coe v1)
  -- Relation.Binary.Construct.Intersection._.implies
  d_implies_124 ::
    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.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_implies_124 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 v10 v11 v12
                v13
    = du_implies_124 v10 v11 v12 v13
  du_implies_124 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_implies_124 v0 v1 v2 v3
    = coe
        MAlonzo.Code.Data.Product.Base.du_'60'_'44'_'62'_112 (coe v0 v2 v3)
        (coe v1 v2 v3)
  -- Relation.Binary.Construct.Intersection._.irreflexive
  d_irreflexive_150 ::
    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.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
  d_irreflexive_150 = erased
  -- Relation.Binary.Construct.Intersection._.respectsˡ
  d_respects'737'_182 ::
    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 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_respects'737'_182 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8 v9 v10 v11
                      v12 v13
    = du_respects'737'_182 v8 v9 v10 v11 v12 v13
  du_respects'737'_182 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_respects'737'_182 v0 v1 v2 v3 v4 v5
    = coe
        MAlonzo.Code.Data.Product.Base.du_map_128 (coe v0 v2 v3 v4 v5)
        (coe (\ v6 -> coe v1 v2 v3 v4 v5))
  -- Relation.Binary.Construct.Intersection._.respectsʳ
  d_respects'691'_190 ::
    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 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_respects'691'_190 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8 v9 v10 v11
                      v12 v13
    = du_respects'691'_190 v8 v9 v10 v11 v12 v13
  du_respects'691'_190 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_respects'691'_190 v0 v1 v2 v3 v4 v5
    = coe
        MAlonzo.Code.Data.Product.Base.du_map_128 (coe v0 v2 v3 v4 v5)
        (coe (\ v6 -> coe v1 v2 v3 v4 v5))
  -- Relation.Binary.Construct.Intersection._.respects₂
  d_respects'8322'_198 ::
    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 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_respects'8322'_198 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8 v9
    = du_respects'8322'_198 v8 v9
  du_respects'8322'_198 ::
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_respects'8322'_198 v0 v1
    = case coe v0 of
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v2 v3
          -> case coe v1 of
               MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v4 v5
                 -> coe
                      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                      (coe du_respects'691'_190 (coe v2) (coe v4))
                      (coe du_respects'737'_182 (coe v3) (coe v5))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Relation.Binary.Construct.Intersection._.antisymmetric
  d_antisymmetric_208 ::
    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 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
  d_antisymmetric_208 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8 v9 v10 v11
                      v12
    = du_antisymmetric_208 v8 v9 v10 v11 v12
  du_antisymmetric_208 ::
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
  du_antisymmetric_208 v0 v1 v2 v3 v4
    = case coe v0 of
        MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 v5
          -> case coe v3 of
               MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v6 v7
                 -> case coe v4 of
                      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v8 v9
                        -> coe v5 v1 v2 v6 v8
                      _ -> MAlonzo.RTE.mazUnreachableError
               _ -> MAlonzo.RTE.mazUnreachableError
        MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 v5
          -> case coe v3 of
               MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v6 v7
                 -> case coe v4 of
                      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v8 v9
                        -> coe v5 v1 v2 v7 v9
                      _ -> MAlonzo.RTE.mazUnreachableError
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Relation.Binary.Construct.Intersection._.decidable
  d_decidable_238 ::
    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 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  d_decidable_238 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8 v9 v10 v11
    = du_decidable_238 v8 v9 v10 v11
  du_decidable_238 ::
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  du_decidable_238 v0 v1 v2 v3
    = coe
        MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
        (coe v0 v2 v3) (coe v1 v2 v3)
  -- Relation.Binary.Construct.Intersection.isEquivalence
  d_isEquivalence_248 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  d_isEquivalence_248 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7
    = du_isEquivalence_248 v6 v7
  du_isEquivalence_248 ::
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  du_isEquivalence_248 v0 v1
    = coe
        MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_745
        (coe
           du_reflexive_52
           (coe MAlonzo.Code.Relation.Binary.Structures.d_refl_34 (coe v0))
           (coe MAlonzo.Code.Relation.Binary.Structures.d_refl_34 (coe v1)))
        (coe
           du_symmetric_58
           (coe MAlonzo.Code.Relation.Binary.Structures.d_sym_36 (coe v0))
           (coe MAlonzo.Code.Relation.Binary.Structures.d_sym_36 (coe v1)))
        (coe
           du_transitive_64
           (coe MAlonzo.Code.Relation.Binary.Structures.d_trans_38 (coe v0))
           (coe MAlonzo.Code.Relation.Binary.Structures.d_trans_38 (coe v1)))
  -- Relation.Binary.Construct.Intersection.isDecEquivalence
  d_isDecEquivalence_286 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
  d_isDecEquivalence_286 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7
    = du_isDecEquivalence_286 v6 v7
  du_isDecEquivalence_286 ::
    MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
  du_isDecEquivalence_286 v0 v1
    = coe
        MAlonzo.Code.Relation.Binary.Structures.C_IsDecEquivalence'46'constructor_3083
        (coe
           du_isEquivalence_248
           (coe
              MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_50
              (coe v0))
           (coe
              MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_50
              (coe v1)))
        (coe
           du_decidable_238
           (coe
              MAlonzo.Code.Relation.Binary.Structures.d__'8799'__52 (coe v0))
           (coe
              MAlonzo.Code.Relation.Binary.Structures.d__'8799'__52 (coe v1)))
  -- Relation.Binary.Construct.Intersection.isPreorder
  d_isPreorder_328 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
  d_isPreorder_328 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8 v9
    = du_isPreorder_328 v8 v9
  du_isPreorder_328 ::
    MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
  du_isPreorder_328 v0 v1
    = coe
        MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_4003
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
           (coe v0))
        (coe
           du_implies_124
           (coe
              MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82 (coe v0))
           (coe
              MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82 (coe v1)))
        (coe
           du_transitive_64
           (coe MAlonzo.Code.Relation.Binary.Structures.d_trans_84 (coe v0))
           (coe MAlonzo.Code.Relation.Binary.Structures.d_trans_84 (coe v1)))
  -- Relation.Binary.Construct.Intersection.isPartialOrderˡ
  d_isPartialOrder'737'_412 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
  d_isPartialOrder'737'_412 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8 v9
    = du_isPartialOrder'737'_412 v8 v9
  du_isPartialOrder'737'_412 ::
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
  du_isPartialOrder'737'_412 v0 v1
    = coe
        MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_9853
        (coe
           du_isPreorder_328
           (coe
              MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182 (coe v0))
           (coe v1))
        (coe
           du_antisymmetric_208
           (coe
              MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
              (coe
                 MAlonzo.Code.Relation.Binary.Structures.d_antisym_184 (coe v0))))
  -- Relation.Binary.Construct.Intersection.isPartialOrderʳ
  d_isPartialOrder'691'_500 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
  d_isPartialOrder'691'_500 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8 v9
    = du_isPartialOrder'691'_500 v8 v9
  du_isPartialOrder'691'_500 ::
    MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
  du_isPartialOrder'691'_500 v0 v1
    = coe
        MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_9853
        (coe
           du_isPreorder_328 (coe v0)
           (coe
              MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182 (coe v1)))
        (coe
           du_antisymmetric_208
           (coe
              MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
              (coe
                 MAlonzo.Code.Relation.Binary.Structures.d_antisym_184 (coe v1))))
  -- Relation.Binary.Construct.Intersection.isStrictPartialOrderˡ
  d_isStrictPartialOrder'737'_588 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290 ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290
  d_isStrictPartialOrder'737'_588 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8
                                  v9 v10
    = du_isStrictPartialOrder'737'_588 v8 v9 v10
  du_isStrictPartialOrder'737'_588 ::
    MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290 ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290
  du_isStrictPartialOrder'737'_588 v0 v1 v2
    = coe
        MAlonzo.Code.Relation.Binary.Structures.C_IsStrictPartialOrder'46'constructor_14045
        (MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_302
           (coe v0))
        (coe
           du_transitive_64
           (coe MAlonzo.Code.Relation.Binary.Structures.d_trans_306 (coe v0))
           (coe v1))
        (coe
           du_respects'8322'_198
           (coe
              MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_308
              (coe v0))
           (coe v2))
  -- Relation.Binary.Construct.Intersection.isStrictPartialOrderʳ
  d_isStrictPartialOrder'691'_634 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290
  d_isStrictPartialOrder'691'_634 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8
                                  v9 v10
    = du_isStrictPartialOrder'691'_634 v8 v9 v10
  du_isStrictPartialOrder'691'_634 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290
  du_isStrictPartialOrder'691'_634 v0 v1 v2
    = coe
        MAlonzo.Code.Relation.Binary.Structures.C_IsStrictPartialOrder'46'constructor_14045
        (MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_302
           (coe v2))
        (coe
           du_transitive_64 (coe v0)
           (coe MAlonzo.Code.Relation.Binary.Structures.d_trans_306 (coe v2)))
        (coe
           du_respects'8322'_198 (coe v1)
           (coe
              MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_308
              (coe v2)))
  