{-# 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 Data.Text qualified
import MAlonzo.Code.Agda.Primitive qualified
import MAlonzo.Code.Relation.Binary.Bundles qualified
import MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles qualified
import MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures 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.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_26 ->
  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_26
-> 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_26
v6
  = T_IsEquivalence_26 -> T_IsIndexedEquivalence_22
du_isIndexedEquivalence_32 T_IsEquivalence_26
v6
du_isIndexedEquivalence_32 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.T_IsIndexedEquivalence_22
du_isIndexedEquivalence_32 :: T_IsEquivalence_26 -> T_IsIndexedEquivalence_22
du_isIndexedEquivalence_32 T_IsEquivalence_26
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_IsIndexedEquivalence'46'constructor_1089
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 ->
            T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34 (T_IsEquivalence_26 -> T_IsEquivalence_26
forall a b. a -> b
coe T_IsEquivalence_26
v0)))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 ->
            T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36 (T_IsEquivalence_26 -> T_IsEquivalence_26
forall a b. a -> b
coe T_IsEquivalence_26
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_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38 (T_IsEquivalence_26 -> T_IsEquivalence_26
forall a b. a -> b
coe T_IsEquivalence_26
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_70 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.T_IsIndexedPreorder_44
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_70
-> T_IsIndexedPreorder_44
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_70
v8
  = T_IsPreorder_70 -> T_IsIndexedPreorder_44
du_isIndexedPreorder_60 T_IsPreorder_70
v8
du_isIndexedPreorder_60 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.T_IsIndexedPreorder_44
du_isIndexedPreorder_60 :: T_IsPreorder_70 -> T_IsIndexedPreorder_44
du_isIndexedPreorder_60 T_IsPreorder_70
v0
  = (T_IsIndexedEquivalence_22
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny
     -> AgdaAny
     -> AgdaAny
     -> AgdaAny
     -> AgdaAny
     -> AgdaAny
     -> AgdaAny
     -> AgdaAny
     -> AgdaAny)
 -> T_IsIndexedPreorder_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsIndexedPreorder_44
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_44
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.C_IsIndexedPreorder'46'constructor_5837
      ((T_IsEquivalence_26 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> T_IsIndexedEquivalence_22
du_isIndexedEquivalence_32
         ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
            (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0)))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 ->
            T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82 (T_IsPreorder_70 -> T_IsPreorder_70
forall a b. a -> b
coe T_IsPreorder_70
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_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84 (T_IsPreorder_70 -> T_IsPreorder_70
forall a b. a -> b
coe T_IsPreorder_70
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_44 ->
  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_44
-> T_IndexedSetoid_18
d_indexedSetoid_106 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Setoid_44
v4 = T_Setoid_44 -> T_IndexedSetoid_18
du_indexedSetoid_106 T_Setoid_44
v4
du_indexedSetoid_106 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.T_IndexedSetoid_18
du_indexedSetoid_106 :: T_Setoid_44 -> T_IndexedSetoid_18
du_indexedSetoid_106 T_Setoid_44
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_IndexedSetoid'46'constructor_445
      ((T_IsEquivalence_26 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> T_IsIndexedEquivalence_22
du_isIndexedEquivalence_32
         ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0)))
-- Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.indexedPreorder
d_indexedPreorder_142 ::
  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_132 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.T_IndexedPreorder_60
d_indexedPreorder_142 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Preorder_132
-> T_IndexedPreorder_60
d_indexedPreorder_142 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 T_Preorder_132
v5
  = T_Preorder_132 -> T_IndexedPreorder_60
du_indexedPreorder_142 T_Preorder_132
v5
du_indexedPreorder_142 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.T_IndexedPreorder_60
du_indexedPreorder_142 :: T_Preorder_132 -> T_IndexedPreorder_60
du_indexedPreorder_142 T_Preorder_132
v0
  = (T_IsIndexedPreorder_44 -> T_IndexedPreorder_60)
-> AgdaAny -> T_IndexedPreorder_60
forall a b. a -> b
coe
      T_IsIndexedPreorder_44 -> T_IndexedPreorder_60
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.C_IndexedPreorder'46'constructor_1987
      ((T_IsPreorder_70 -> T_IsIndexedPreorder_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> T_IsIndexedPreorder_44
du_isIndexedPreorder_60
         ((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)))