{-# 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.Preorder where

import Data.Text qualified
import MAlonzo.Code.Agda.Builtin.Sigma qualified
import MAlonzo.Code.Agda.Primitive qualified
import MAlonzo.Code.Data.Product.Base qualified
import MAlonzo.Code.Relation.Binary.Bundles qualified
import MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd 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.Preorder._._≳_
d__'8819'__24 ::
  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_Preorder_132 ->
  AgdaAny -> AgdaAny -> ()
d__'8819'__24 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Preorder_132
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8819'__24 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Preorder_132
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Relation.Binary.Properties.Preorder.converse-isPreorder
d_converse'45'isPreorder_78 ::
  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_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_converse'45'isPreorder_78 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Preorder_132 -> T_IsPreorder_70
d_converse'45'isPreorder_78 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Preorder_132
v3
  = T_Preorder_132 -> T_IsPreorder_70
du_converse'45'isPreorder_78 T_Preorder_132
v3
du_converse'45'isPreorder_78 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_converse'45'isPreorder_78 :: T_Preorder_132 -> T_IsPreorder_70
du_converse'45'isPreorder_78 T_Preorder_132
v0
  = (T_IsPreorder_70 -> T_IsPreorder_70) -> AgdaAny -> T_IsPreorder_70
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_isPreorder_258
      ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0))
-- Relation.Binary.Properties.Preorder.converse-preorder
d_converse'45'preorder_80 ::
  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_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_converse'45'preorder_80 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Preorder_132 -> T_Preorder_132
d_converse'45'preorder_80 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Preorder_132
v3
  = T_Preorder_132 -> T_Preorder_132
du_converse'45'preorder_80 T_Preorder_132
v3
du_converse'45'preorder_80 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_converse'45'preorder_80 :: T_Preorder_132 -> T_Preorder_132
du_converse'45'preorder_80 T_Preorder_132
v0
  = (T_Preorder_132 -> T_Preorder_132) -> AgdaAny -> T_Preorder_132
forall a b. a -> b
coe
      T_Preorder_132 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_preorder_676
      (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0)
-- Relation.Binary.Properties.Preorder.InducedEquivalence
d_InducedEquivalence_82 ::
  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_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_InducedEquivalence_82 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Preorder_132 -> T_Setoid_44
d_InducedEquivalence_82 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Preorder_132
v3
  = T_Preorder_132 -> T_Setoid_44
du_InducedEquivalence_82 T_Preorder_132
v3
du_InducedEquivalence_82 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_InducedEquivalence_82 :: T_Preorder_132 -> T_Setoid_44
du_InducedEquivalence_82 T_Preorder_132
v0
  = (T_IsEquivalence_26 -> T_Setoid_44) -> AgdaAny -> T_Setoid_44
forall a b. a -> b
coe
      T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_733
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_745
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 ->
               (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                 ((T_IsPreorder_70 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_IsPreorder_70 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
                    ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0))
                    (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
                 ((T_IsPreorder_70 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_IsPreorder_70 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
                    ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0))
                    (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))))
         ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 -> (T_Σ_14 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_swap_370))
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
               ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_zip_198
                 ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
                    (T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> T_Preorder_132
forall a b. a -> b
coe T_Preorder_132
v0)) AgdaAny
v1
                    AgdaAny
v2 AgdaAny
v3)
                 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                    (\ AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 ->
                       (T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                         T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
                         (T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> T_Preorder_132
forall a b. a -> b
coe T_Preorder_132
v0)) AgdaAny
v3
                         AgdaAny
v2 AgdaAny
v1 AgdaAny
v7 AgdaAny
v6)))))
-- Relation.Binary.Properties.Preorder.invIsPreorder
d_invIsPreorder_88 ::
  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_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_invIsPreorder_88 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Preorder_132 -> T_IsPreorder_70
d_invIsPreorder_88 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Preorder_132
v3 = T_Preorder_132 -> T_IsPreorder_70
du_invIsPreorder_88 T_Preorder_132
v3
du_invIsPreorder_88 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_invIsPreorder_88 :: T_Preorder_132 -> T_IsPreorder_70
du_invIsPreorder_88 T_Preorder_132
v0 = (T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> T_IsPreorder_70
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
du_converse'45'isPreorder_78 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0)
-- Relation.Binary.Properties.Preorder.invPreorder
d_invPreorder_90 ::
  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_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_invPreorder_90 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Preorder_132 -> T_Preorder_132
d_invPreorder_90 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Preorder_132
v3 = T_Preorder_132 -> T_Preorder_132
du_invPreorder_90 T_Preorder_132
v3
du_invPreorder_90 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_invPreorder_90 :: T_Preorder_132 -> T_Preorder_132
du_invPreorder_90 T_Preorder_132
v0 = (T_Preorder_132 -> T_Preorder_132) -> AgdaAny -> T_Preorder_132
forall a b. a -> b
coe T_Preorder_132 -> T_Preorder_132
du_converse'45'preorder_80 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0)