{-# 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 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.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Product.Base
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Relation.Binary.Properties.Preorder._._∼ᵒ_
d__'8764''7506'__26 ::
  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_142 ->
  AgdaAny -> AgdaAny -> ()
d__'8764''7506'__26 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Preorder_142
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8764''7506'__26 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Preorder_142
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Relation.Binary.Properties.Preorder.converse-isPreorder
d_converse'45'isPreorder_86 ::
  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_142 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76
d_converse'45'isPreorder_86 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Preorder_142 -> T_IsPreorder_76
d_converse'45'isPreorder_86 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Preorder_142
v3
  = T_Preorder_142 -> T_IsPreorder_76
du_converse'45'isPreorder_86 T_Preorder_142
v3
du_converse'45'isPreorder_86 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76
du_converse'45'isPreorder_86 :: T_Preorder_142 -> T_IsPreorder_76
du_converse'45'isPreorder_86 T_Preorder_142
v0
  = (T_IsPreorder_76 -> T_IsPreorder_76) -> AgdaAny -> T_IsPreorder_76
forall a b. a -> b
coe
      T_IsPreorder_76 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_isPreorder_258
      ((T_Preorder_142 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Preorder_142 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_164 (T_Preorder_142 -> AgdaAny
forall a b. a -> b
coe T_Preorder_142
v0))
-- Relation.Binary.Properties.Preorder.converse-preorder
d_converse'45'preorder_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_142 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
d_converse'45'preorder_88 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Preorder_142 -> T_Preorder_142
d_converse'45'preorder_88 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Preorder_142
v3
  = T_Preorder_142 -> T_Preorder_142
du_converse'45'preorder_88 T_Preorder_142
v3
du_converse'45'preorder_88 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
du_converse'45'preorder_88 :: T_Preorder_142 -> T_Preorder_142
du_converse'45'preorder_88 T_Preorder_142
v0
  = (T_Preorder_142 -> T_Preorder_142) -> AgdaAny -> T_Preorder_142
forall a b. a -> b
coe
      T_Preorder_142 -> T_Preorder_142
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_preorder_682
      (T_Preorder_142 -> AgdaAny
forall a b. a -> b
coe T_Preorder_142
v0)
-- Relation.Binary.Properties.Preorder.InducedEquivalence
d_InducedEquivalence_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_142 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46
d_InducedEquivalence_90 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Preorder_142 -> T_Setoid_46
d_InducedEquivalence_90 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Preorder_142
v3
  = T_Preorder_142 -> T_Setoid_46
du_InducedEquivalence_90 T_Preorder_142
v3
du_InducedEquivalence_90 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46
du_InducedEquivalence_90 :: T_Preorder_142 -> T_Setoid_46
du_InducedEquivalence_90 T_Preorder_142
v0
  = (T_IsEquivalence_28 -> T_Setoid_46) -> AgdaAny -> T_Setoid_46
forall a b. a -> b
coe
      T_IsEquivalence_28 -> T_Setoid_46
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_84
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.C_constructor_46
         ((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_76 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_IsPreorder_76 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_104
                    ((T_Preorder_142 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Preorder_142 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_164 (T_Preorder_142 -> AgdaAny
forall a b. a -> b
coe T_Preorder_142
v0))
                    (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
                 ((T_IsPreorder_76 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_IsPreorder_76 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_104
                    ((T_Preorder_142 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Preorder_142 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_164 (T_Preorder_142 -> AgdaAny
forall a b. a -> b
coe T_Preorder_142
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_76
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_IsPreorder_76
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_90
                    (T_Preorder_142 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_164 (T_Preorder_142 -> T_Preorder_142
forall a b. a -> b
coe T_Preorder_142
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_76
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_76
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                         T_IsPreorder_76
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_90
                         (T_Preorder_142 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_164 (T_Preorder_142 -> T_Preorder_142
forall a b. a -> b
coe T_Preorder_142
v0)) AgdaAny
v3
                         AgdaAny
v2 AgdaAny
v1 AgdaAny
v7 AgdaAny
v6)))))
-- Relation.Binary.Properties.Preorder.invIsPreorder
d_invIsPreorder_96 ::
  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_142 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76
d_invIsPreorder_96 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Preorder_142 -> T_IsPreorder_76
d_invIsPreorder_96 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Preorder_142
v3 = T_Preorder_142 -> T_IsPreorder_76
du_invIsPreorder_96 T_Preorder_142
v3
du_invIsPreorder_96 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76
du_invIsPreorder_96 :: T_Preorder_142 -> T_IsPreorder_76
du_invIsPreorder_96 T_Preorder_142
v0 = (T_Preorder_142 -> T_IsPreorder_76) -> AgdaAny -> T_IsPreorder_76
forall a b. a -> b
coe T_Preorder_142 -> T_IsPreorder_76
du_converse'45'isPreorder_86 (T_Preorder_142 -> AgdaAny
forall a b. a -> b
coe T_Preorder_142
v0)
-- Relation.Binary.Properties.Preorder.invPreorder
d_invPreorder_98 ::
  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_142 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
d_invPreorder_98 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Preorder_142 -> T_Preorder_142
d_invPreorder_98 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Preorder_142
v3 = T_Preorder_142 -> T_Preorder_142
du_invPreorder_98 T_Preorder_142
v3
du_invPreorder_98 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
du_invPreorder_98 :: T_Preorder_142 -> T_Preorder_142
du_invPreorder_98 T_Preorder_142
v0 = (T_Preorder_142 -> T_Preorder_142) -> AgdaAny -> T_Preorder_142
forall a b. a -> b
coe T_Preorder_142 -> T_Preorder_142
du_converse'45'preorder_88 (T_Preorder_142 -> AgdaAny
forall a b. a -> b
coe T_Preorder_142
v0)