{-# 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__'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)