{-# 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.Indexed.Heterogeneous.Construct.Trivial 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.Primitive
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles
import qualified MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Relation.Binary.Indexed.Heterogeneous.Construct.Trivial._.Aᵢ
d_A'7522'_24 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> AgdaAny -> ()
d_A'7522'_24 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Level_18 -> AgdaAny -> T_Level_18
d_A'7522'_24 = T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Level_18 -> AgdaAny -> T_Level_18
forall a. a
erased
-- Relation.Binary.Indexed.Heterogeneous.Construct.Trivial._.isIndexedEquivalence
d_isIndexedEquivalence_32 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.T_IsIndexedEquivalence_22
d_isIndexedEquivalence_32 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_28
-> T_IsIndexedEquivalence_22
d_isIndexedEquivalence_32 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 T_IsEquivalence_28
v6
  = T_IsEquivalence_28 -> T_IsIndexedEquivalence_22
du_isIndexedEquivalence_32 T_IsEquivalence_28
v6
du_isIndexedEquivalence_32 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.T_IsIndexedEquivalence_22
du_isIndexedEquivalence_32 :: T_IsEquivalence_28 -> T_IsIndexedEquivalence_22
du_isIndexedEquivalence_32 T_IsEquivalence_28
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny
     -> AgdaAny
     -> AgdaAny
     -> AgdaAny
     -> AgdaAny
     -> AgdaAny
     -> AgdaAny
     -> AgdaAny
     -> AgdaAny)
 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsIndexedEquivalence_22
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny
    -> AgdaAny
    -> AgdaAny
    -> AgdaAny
    -> AgdaAny
    -> AgdaAny
    -> AgdaAny
    -> AgdaAny)
-> T_IsIndexedEquivalence_22
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.C_constructor_40
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 ->
            T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36 (T_IsEquivalence_28 -> T_IsEquivalence_28
forall a b. a -> b
coe T_IsEquivalence_28
v0)))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 ->
            T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38 (T_IsEquivalence_28 -> T_IsEquivalence_28
forall a b. a -> b
coe T_IsEquivalence_28
v0)))
      ((AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
            T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40 (T_IsEquivalence_28 -> T_IsEquivalence_28
forall a b. a -> b
coe T_IsEquivalence_28
v0)))
-- Relation.Binary.Indexed.Heterogeneous.Construct.Trivial._.isIndexedPreorder
d_isIndexedPreorder_60 ::
  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 -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.T_IsIndexedPreorder_46
d_isIndexedPreorder_60 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsPreorder_76
-> T_IsIndexedPreorder_46
d_isIndexedPreorder_60 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> AgdaAny -> T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 T_IsPreorder_76
v8
  = T_IsPreorder_76 -> T_IsIndexedPreorder_46
du_isIndexedPreorder_60 T_IsPreorder_76
v8
du_isIndexedPreorder_60 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.T_IsIndexedPreorder_46
du_isIndexedPreorder_60 :: T_IsPreorder_76 -> T_IsIndexedPreorder_46
du_isIndexedPreorder_60 T_IsPreorder_76
v0
  = (T_IsIndexedEquivalence_22
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny
     -> AgdaAny
     -> AgdaAny
     -> AgdaAny
     -> AgdaAny
     -> AgdaAny
     -> AgdaAny
     -> AgdaAny
     -> AgdaAny)
 -> T_IsIndexedPreorder_46)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsIndexedPreorder_46
forall a b. a -> b
coe
      T_IsIndexedEquivalence_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny
    -> AgdaAny
    -> AgdaAny
    -> AgdaAny
    -> AgdaAny
    -> AgdaAny
    -> AgdaAny
    -> AgdaAny)
-> T_IsIndexedPreorder_46
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.C_constructor_84
      ((T_IsEquivalence_28 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28 -> T_IsIndexedEquivalence_22
du_isIndexedEquivalence_32
         ((T_IsPreorder_76 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_76 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_86
            (T_IsPreorder_76 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_76
v0)))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 ->
            T_IsPreorder_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_88 (T_IsPreorder_76 -> T_IsPreorder_76
forall a b. a -> b
coe T_IsPreorder_76
v0)))
      ((AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
            T_IsPreorder_76
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_90 (T_IsPreorder_76 -> T_IsPreorder_76
forall a b. a -> b
coe T_IsPreorder_76
v0)))
-- Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.indexedSetoid
d_indexedSetoid_106 ::
  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_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.T_IndexedSetoid_18
d_indexedSetoid_106 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_IndexedSetoid_18
d_indexedSetoid_106 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Setoid_46
v4 = T_Setoid_46 -> T_IndexedSetoid_18
du_indexedSetoid_106 T_Setoid_46
v4
du_indexedSetoid_106 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.T_IndexedSetoid_18
du_indexedSetoid_106 :: T_Setoid_46 -> T_IndexedSetoid_18
du_indexedSetoid_106 T_Setoid_46
v0
  = (T_IsIndexedEquivalence_22 -> T_IndexedSetoid_18)
-> AgdaAny -> T_IndexedSetoid_18
forall a b. a -> b
coe
      T_IsIndexedEquivalence_22 -> T_IndexedSetoid_18
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.C_constructor_50
      ((T_IsEquivalence_28 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28 -> T_IsIndexedEquivalence_22
du_isIndexedEquivalence_32
         ((T_Setoid_46 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_46 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_62 (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe T_Setoid_46
v0)))
-- Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.indexedPreorder
d_indexedPreorder_144 ::
  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.Relation.Binary.Bundles.T_Preorder_142 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.T_IndexedPreorder_62
d_indexedPreorder_144 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Preorder_142
-> T_IndexedPreorder_62
d_indexedPreorder_144 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 T_Preorder_142
v5
  = T_Preorder_142 -> T_IndexedPreorder_62
du_indexedPreorder_144 T_Preorder_142
v5
du_indexedPreorder_144 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.T_IndexedPreorder_62
du_indexedPreorder_144 :: T_Preorder_142 -> T_IndexedPreorder_62
du_indexedPreorder_144 T_Preorder_142
v0
  = (T_IsIndexedPreorder_46 -> T_IndexedPreorder_62)
-> AgdaAny -> T_IndexedPreorder_62
forall a b. a -> b
coe
      T_IsIndexedPreorder_46 -> T_IndexedPreorder_62
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.C_constructor_112
      ((T_IsPreorder_76 -> T_IsIndexedPreorder_46) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_76 -> T_IsIndexedPreorder_46
du_isIndexedPreorder_60
         ((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)))