{-# 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_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_5831
      ((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_100 ::
  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_100 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_IndexedSetoid_18
d_indexedSetoid_100 ~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_100 T_Setoid_44
v4
du_indexedSetoid_100 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.T_IndexedSetoid_18
du_indexedSetoid_100 :: T_Setoid_44 -> T_IndexedSetoid_18
du_indexedSetoid_100 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_136 ::
  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_136 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Preorder_132
-> T_IndexedPreorder_60
d_indexedPreorder_136 ~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_136 T_Preorder_132
v5
du_indexedPreorder_136 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.T_IndexedPreorder_60
du_indexedPreorder_136 :: T_Preorder_132 -> T_IndexedPreorder_60
du_indexedPreorder_136 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_1981
      ((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)))