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

-- Relation.Binary.Indexed.Heterogeneous.Bundles.IndexedSetoid
d_IndexedSetoid_18 :: p -> p -> p -> p -> ()
d_IndexedSetoid_18 p
a0 p
a1 p
a2 p
a3 = ()
newtype T_IndexedSetoid_18
  = C_IndexedSetoid'46'constructor_445 MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.T_IsIndexedEquivalence_22
-- Relation.Binary.Indexed.Heterogeneous.Bundles.IndexedSetoid.Carrier
d_Carrier_34 :: T_IndexedSetoid_18 -> AgdaAny -> ()
d_Carrier_34 :: T_IndexedSetoid_18 -> AgdaAny -> ()
d_Carrier_34 = T_IndexedSetoid_18 -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Indexed.Heterogeneous.Bundles.IndexedSetoid._≈_
d__'8776'__36 ::
  T_IndexedSetoid_18 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()
d__'8776'__36 :: T_IndexedSetoid_18
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()
d__'8776'__36 = T_IndexedSetoid_18
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Indexed.Heterogeneous.Bundles.IndexedSetoid.isEquivalence
d_isEquivalence_38 ::
  T_IndexedSetoid_18 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.T_IsIndexedEquivalence_22
d_isEquivalence_38 :: T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22
d_isEquivalence_38 T_IndexedSetoid_18
v0
  = case T_IndexedSetoid_18 -> T_IndexedSetoid_18
forall a b. a -> b
coe T_IndexedSetoid_18
v0 of
      C_IndexedSetoid'46'constructor_445 T_IsIndexedEquivalence_22
v3 -> T_IsIndexedEquivalence_22 -> T_IsIndexedEquivalence_22
forall a b. a -> b
coe T_IsIndexedEquivalence_22
v3
      T_IndexedSetoid_18
_ -> T_IsIndexedEquivalence_22
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Indexed.Heterogeneous.Bundles.IndexedSetoid._.refl
d_refl_42 :: T_IndexedSetoid_18 -> AgdaAny -> AgdaAny -> AgdaAny
d_refl_42 :: T_IndexedSetoid_18 -> AgdaAny -> AgdaAny -> AgdaAny
d_refl_42 T_IndexedSetoid_18
v0
  = (T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_refl_30
      ((T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22
d_isEquivalence_38 (T_IndexedSetoid_18 -> AgdaAny
forall a b. a -> b
coe T_IndexedSetoid_18
v0))
-- Relation.Binary.Indexed.Heterogeneous.Bundles.IndexedSetoid._.reflexive
d_reflexive_44 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_IndexedSetoid_18 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_reflexive_44 :: ()
-> ()
-> ()
-> ()
-> T_IndexedSetoid_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_reflexive_44 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_IndexedSetoid_18
v4 = T_IndexedSetoid_18
-> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_44 T_IndexedSetoid_18
v4
du_reflexive_44 ::
  T_IndexedSetoid_18 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
du_reflexive_44 :: T_IndexedSetoid_18
-> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_44 T_IndexedSetoid_18
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 T__'8801'__12
v4
  = (T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.du_reflexive_38
      ((T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22
d_isEquivalence_38 (T_IndexedSetoid_18 -> AgdaAny
forall a b. a -> b
coe T_IndexedSetoid_18
v0)) AgdaAny
v1 AgdaAny
v2
-- Relation.Binary.Indexed.Heterogeneous.Bundles.IndexedSetoid._.sym
d_sym_46 ::
  T_IndexedSetoid_18 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_46 :: T_IndexedSetoid_18
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_46 T_IndexedSetoid_18
v0
  = (T_IsIndexedEquivalence_22
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsIndexedEquivalence_22
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_sym_32
      ((T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22
d_isEquivalence_38 (T_IndexedSetoid_18 -> AgdaAny
forall a b. a -> b
coe T_IndexedSetoid_18
v0))
-- Relation.Binary.Indexed.Heterogeneous.Bundles.IndexedSetoid._.trans
d_trans_48 ::
  T_IndexedSetoid_18 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_48 :: T_IndexedSetoid_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_48 T_IndexedSetoid_18
v0
  = (T_IsIndexedEquivalence_22
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsIndexedEquivalence_22
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_trans_34
      ((T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22
d_isEquivalence_38 (T_IndexedSetoid_18 -> AgdaAny
forall a b. a -> b
coe T_IndexedSetoid_18
v0))
-- Relation.Binary.Indexed.Heterogeneous.Bundles.IndexedPreorder
d_IndexedPreorder_60 :: p -> p -> p -> p -> p -> ()
d_IndexedPreorder_60 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
newtype T_IndexedPreorder_60
  = C_IndexedPreorder'46'constructor_1981 MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.T_IsIndexedPreorder_44
-- Relation.Binary.Indexed.Heterogeneous.Bundles.IndexedPreorder.Carrier
d_Carrier_80 :: T_IndexedPreorder_60 -> AgdaAny -> ()
d_Carrier_80 :: T_IndexedPreorder_60 -> AgdaAny -> ()
d_Carrier_80 = T_IndexedPreorder_60 -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Indexed.Heterogeneous.Bundles.IndexedPreorder._≈_
d__'8776'__82 ::
  T_IndexedPreorder_60 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()
d__'8776'__82 :: T_IndexedPreorder_60
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()
d__'8776'__82 = T_IndexedPreorder_60
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Indexed.Heterogeneous.Bundles.IndexedPreorder._∼_
d__'8764'__84 ::
  T_IndexedPreorder_60 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()
d__'8764'__84 :: T_IndexedPreorder_60
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()
d__'8764'__84 = T_IndexedPreorder_60
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Indexed.Heterogeneous.Bundles.IndexedPreorder.isPreorder
d_isPreorder_86 ::
  T_IndexedPreorder_60 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.T_IsIndexedPreorder_44
d_isPreorder_86 :: T_IndexedPreorder_60 -> T_IsIndexedPreorder_44
d_isPreorder_86 T_IndexedPreorder_60
v0
  = case T_IndexedPreorder_60 -> T_IndexedPreorder_60
forall a b. a -> b
coe T_IndexedPreorder_60
v0 of
      C_IndexedPreorder'46'constructor_1981 T_IsIndexedPreorder_44
v4 -> T_IsIndexedPreorder_44 -> T_IsIndexedPreorder_44
forall a b. a -> b
coe T_IsIndexedPreorder_44
v4
      T_IndexedPreorder_60
_ -> T_IsIndexedPreorder_44
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Indexed.Heterogeneous.Bundles.IndexedPreorder._.isEquivalence
d_isEquivalence_90 ::
  T_IndexedPreorder_60 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.T_IsIndexedEquivalence_22
d_isEquivalence_90 :: T_IndexedPreorder_60 -> T_IsIndexedEquivalence_22
d_isEquivalence_90 T_IndexedPreorder_60
v0
  = (T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> T_IsIndexedEquivalence_22
forall a b. a -> b
coe
      T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_isEquivalence_60
      ((T_IndexedPreorder_60 -> T_IsIndexedPreorder_44)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60 -> T_IsIndexedPreorder_44
d_isPreorder_86 (T_IndexedPreorder_60 -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60
v0))
-- Relation.Binary.Indexed.Heterogeneous.Bundles.IndexedPreorder._.refl
d_refl_92 ::
  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 ->
  T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny
d_refl_92 :: ()
-> ()
-> ()
-> ()
-> ()
-> T_IndexedPreorder_60
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_refl_92 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 T_IndexedPreorder_60
v5 = T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny
du_refl_92 T_IndexedPreorder_60
v5
du_refl_92 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny
du_refl_92 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny
du_refl_92 T_IndexedPreorder_60
v0
  = (T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.du_refl_80
      ((T_IndexedPreorder_60 -> T_IsIndexedPreorder_44)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60 -> T_IsIndexedPreorder_44
d_isPreorder_86 (T_IndexedPreorder_60 -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60
v0))
-- Relation.Binary.Indexed.Heterogeneous.Bundles.IndexedPreorder._.reflexive
d_reflexive_94 ::
  T_IndexedPreorder_60 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_94 :: T_IndexedPreorder_60
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_94 T_IndexedPreorder_60
v0
  = (T_IsIndexedPreorder_44
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsIndexedPreorder_44
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_reflexive_66
      ((T_IndexedPreorder_60 -> T_IsIndexedPreorder_44)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60 -> T_IsIndexedPreorder_44
d_isPreorder_86 (T_IndexedPreorder_60 -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60
v0))
-- Relation.Binary.Indexed.Heterogeneous.Bundles.IndexedPreorder._.trans
d_trans_96 ::
  T_IndexedPreorder_60 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_96 :: T_IndexedPreorder_60
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_96 T_IndexedPreorder_60
v0
  = (T_IsIndexedPreorder_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsIndexedPreorder_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_trans_68
      ((T_IndexedPreorder_60 -> T_IsIndexedPreorder_44)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60 -> T_IsIndexedPreorder_44
d_isPreorder_86 (T_IndexedPreorder_60 -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60
v0))
-- Relation.Binary.Indexed.Heterogeneous.Bundles.IndexedPreorder._.Eq.refl
d_refl_100 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny
d_refl_100 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny
d_refl_100 T_IndexedPreorder_60
v0
  = (T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_refl_30
      ((T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_isEquivalence_60
         ((T_IndexedPreorder_60 -> T_IsIndexedPreorder_44)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60 -> T_IsIndexedPreorder_44
d_isPreorder_86 (T_IndexedPreorder_60 -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60
v0)))
-- Relation.Binary.Indexed.Heterogeneous.Bundles.IndexedPreorder._.Eq.reflexive
d_reflexive_102 ::
  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 ->
  T_IndexedPreorder_60 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_reflexive_102 :: ()
-> ()
-> ()
-> ()
-> ()
-> T_IndexedPreorder_60
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_reflexive_102 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 T_IndexedPreorder_60
v5 = T_IndexedPreorder_60
-> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_102 T_IndexedPreorder_60
v5
du_reflexive_102 ::
  T_IndexedPreorder_60 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
du_reflexive_102 :: T_IndexedPreorder_60
-> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_102 T_IndexedPreorder_60
v0
  = let v1 :: T_IsIndexedPreorder_44
v1 = T_IndexedPreorder_60 -> T_IsIndexedPreorder_44
d_isPreorder_86 (T_IndexedPreorder_60 -> T_IndexedPreorder_60
forall a b. a -> b
coe T_IndexedPreorder_60
v0) in
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
forall a b. a -> b
coe
      (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 ->
         (T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.du_reflexive_38
           ((T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_isEquivalence_60
              (T_IsIndexedPreorder_44 -> AgdaAny
forall a b. a -> b
coe T_IsIndexedPreorder_44
v1))
           AgdaAny
v2 AgdaAny
v3)
-- Relation.Binary.Indexed.Heterogeneous.Bundles.IndexedPreorder._.Eq.sym
d_sym_104 ::
  T_IndexedPreorder_60 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_104 :: T_IndexedPreorder_60
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_104 T_IndexedPreorder_60
v0
  = (T_IsIndexedEquivalence_22
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsIndexedEquivalence_22
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_sym_32
      ((T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_isEquivalence_60
         ((T_IndexedPreorder_60 -> T_IsIndexedPreorder_44)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60 -> T_IsIndexedPreorder_44
d_isPreorder_86 (T_IndexedPreorder_60 -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60
v0)))
-- Relation.Binary.Indexed.Heterogeneous.Bundles.IndexedPreorder._.Eq.trans
d_trans_106 ::
  T_IndexedPreorder_60 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_106 :: T_IndexedPreorder_60
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_106 T_IndexedPreorder_60
v0
  = (T_IsIndexedEquivalence_22
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsIndexedEquivalence_22
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_trans_34
      ((T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_isEquivalence_60
         ((T_IndexedPreorder_60 -> T_IsIndexedPreorder_44)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60 -> T_IsIndexedPreorder_44
d_isPreorder_86 (T_IndexedPreorder_60 -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60
v0)))