{-# 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.Structures 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

-- Relation.Binary.Indexed.Heterogeneous.Structures.IsIndexedEquivalence
d_IsIndexedEquivalence_22 :: p -> p -> p -> p -> p -> p -> ()
d_IsIndexedEquivalence_22 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_IsIndexedEquivalence_22
  = C_IsIndexedEquivalence'46'constructor_1089 (AgdaAny ->
                                                AgdaAny -> AgdaAny)
                                               (AgdaAny ->
                                                AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
                                               (AgdaAny ->
                                                AgdaAny ->
                                                AgdaAny ->
                                                AgdaAny ->
                                                AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-- Relation.Binary.Indexed.Heterogeneous.Structures.IsIndexedEquivalence.refl
d_refl_30 ::
  T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny
d_refl_30 :: T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny
d_refl_30 T_IsIndexedEquivalence_22
v0
  = case T_IsIndexedEquivalence_22 -> T_IsIndexedEquivalence_22
forall a b. a -> b
coe T_IsIndexedEquivalence_22
v0 of
      C_IsIndexedEquivalence'46'constructor_1089 AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
v3 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1
      T_IsIndexedEquivalence_22
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Indexed.Heterogeneous.Structures.IsIndexedEquivalence.sym
d_sym_32 ::
  T_IsIndexedEquivalence_22 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_32 :: T_IsIndexedEquivalence_22
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_32 T_IsIndexedEquivalence_22
v0
  = case T_IsIndexedEquivalence_22 -> T_IsIndexedEquivalence_22
forall a b. a -> b
coe T_IsIndexedEquivalence_22
v0 of
      C_IsIndexedEquivalence'46'constructor_1089 AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
v3 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2
      T_IsIndexedEquivalence_22
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Indexed.Heterogeneous.Structures.IsIndexedEquivalence.trans
d_trans_34 ::
  T_IsIndexedEquivalence_22 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_34 :: T_IsIndexedEquivalence_22
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_34 T_IsIndexedEquivalence_22
v0
  = case T_IsIndexedEquivalence_22 -> T_IsIndexedEquivalence_22
forall a b. a -> b
coe T_IsIndexedEquivalence_22
v0 of
      C_IsIndexedEquivalence'46'constructor_1089 AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
v3 -> (AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
v3
      T_IsIndexedEquivalence_22
_ -> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Indexed.Heterogeneous.Structures.IsIndexedEquivalence.reflexive
d_reflexive_38 ::
  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 -> AgdaAny -> ()) ->
  T_IsIndexedEquivalence_22 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_reflexive_38 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ())
-> T_IsIndexedEquivalence_22
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_reflexive_38 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()
v5 T_IsIndexedEquivalence_22
v6 AgdaAny
v7 AgdaAny
v8 ~AgdaAny
v9 ~T__'8801'__12
v10
  = T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_38 T_IsIndexedEquivalence_22
v6 AgdaAny
v7 AgdaAny
v8
du_reflexive_38 ::
  T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_38 :: T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_38 T_IsIndexedEquivalence_22
v0 AgdaAny
v1 AgdaAny
v2 = (T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny
d_refl_30 T_IsIndexedEquivalence_22
v0 AgdaAny
v1 AgdaAny
v2
-- Relation.Binary.Indexed.Heterogeneous.Structures.IsIndexedPreorder
d_IsIndexedPreorder_44 :: p -> p -> p -> p -> p -> p -> p -> p -> ()
d_IsIndexedPreorder_44 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 = ()
data T_IsIndexedPreorder_44
  = C_IsIndexedPreorder'46'constructor_5831 T_IsIndexedEquivalence_22
                                            (AgdaAny ->
                                             AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
                                            (AgdaAny ->
                                             AgdaAny ->
                                             AgdaAny ->
                                             AgdaAny ->
                                             AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-- Relation.Binary.Indexed.Heterogeneous.Structures.IsIndexedPreorder.isEquivalence
d_isEquivalence_60 ::
  T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22
d_isEquivalence_60 :: T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22
d_isEquivalence_60 T_IsIndexedPreorder_44
v0
  = case T_IsIndexedPreorder_44 -> T_IsIndexedPreorder_44
forall a b. a -> b
coe T_IsIndexedPreorder_44
v0 of
      C_IsIndexedPreorder'46'constructor_5831 T_IsIndexedEquivalence_22
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
v3 -> T_IsIndexedEquivalence_22 -> T_IsIndexedEquivalence_22
forall a b. a -> b
coe T_IsIndexedEquivalence_22
v1
      T_IsIndexedPreorder_44
_ -> T_IsIndexedEquivalence_22
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Indexed.Heterogeneous.Structures.IsIndexedPreorder.reflexive
d_reflexive_66 ::
  T_IsIndexedPreorder_44 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_66 :: T_IsIndexedPreorder_44
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_66 T_IsIndexedPreorder_44
v0
  = case T_IsIndexedPreorder_44 -> T_IsIndexedPreorder_44
forall a b. a -> b
coe T_IsIndexedPreorder_44
v0 of
      C_IsIndexedPreorder'46'constructor_5831 T_IsIndexedEquivalence_22
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
v3 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2
      T_IsIndexedPreorder_44
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Indexed.Heterogeneous.Structures.IsIndexedPreorder.trans
d_trans_68 ::
  T_IsIndexedPreorder_44 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_68 :: T_IsIndexedPreorder_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_68 T_IsIndexedPreorder_44
v0
  = case T_IsIndexedPreorder_44 -> T_IsIndexedPreorder_44
forall a b. a -> b
coe T_IsIndexedPreorder_44
v0 of
      C_IsIndexedPreorder'46'constructor_5831 T_IsIndexedEquivalence_22
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
v3 -> (AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
v3
      T_IsIndexedPreorder_44
_ -> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Indexed.Heterogeneous.Structures.IsIndexedPreorder.Eq.refl
d_refl_72 ::
  T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny
d_refl_72 :: T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny
d_refl_72 T_IsIndexedPreorder_44
v0 = (T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny
d_refl_30 ((T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22
d_isEquivalence_60 (T_IsIndexedPreorder_44 -> AgdaAny
forall a b. a -> b
coe T_IsIndexedPreorder_44
v0))
-- Relation.Binary.Indexed.Heterogeneous.Structures.IsIndexedPreorder.Eq.reflexive
d_reflexive_74 ::
  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 -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()) ->
  T_IsIndexedPreorder_44 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_reflexive_74 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ())
-> T_IsIndexedPreorder_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_reflexive_74 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()
v5 ~()
v6 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()
v7 T_IsIndexedPreorder_44
v8
  = T_IsIndexedPreorder_44
-> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_74 T_IsIndexedPreorder_44
v8
du_reflexive_74 ::
  T_IsIndexedPreorder_44 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
du_reflexive_74 :: T_IsIndexedPreorder_44
-> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_74 T_IsIndexedPreorder_44
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
du_reflexive_38 ((T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22
d_isEquivalence_60 (T_IsIndexedPreorder_44 -> AgdaAny
forall a b. a -> b
coe T_IsIndexedPreorder_44
v0)) AgdaAny
v1 AgdaAny
v2
-- Relation.Binary.Indexed.Heterogeneous.Structures.IsIndexedPreorder.Eq.sym
d_sym_76 ::
  T_IsIndexedPreorder_44 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_76 :: T_IsIndexedPreorder_44
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_76 T_IsIndexedPreorder_44
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
d_sym_32 ((T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22
d_isEquivalence_60 (T_IsIndexedPreorder_44 -> AgdaAny
forall a b. a -> b
coe T_IsIndexedPreorder_44
v0))
-- Relation.Binary.Indexed.Heterogeneous.Structures.IsIndexedPreorder.Eq.trans
d_trans_78 ::
  T_IsIndexedPreorder_44 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_78 :: T_IsIndexedPreorder_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_78 T_IsIndexedPreorder_44
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
d_trans_34 ((T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22
d_isEquivalence_60 (T_IsIndexedPreorder_44 -> AgdaAny
forall a b. a -> b
coe T_IsIndexedPreorder_44
v0))
-- Relation.Binary.Indexed.Heterogeneous.Structures.IsIndexedPreorder.refl
d_refl_80 ::
  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 -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()) ->
  T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny
d_refl_80 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ())
-> T_IsIndexedPreorder_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_refl_80 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()
v5 ~()
v6 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()
v7 T_IsIndexedPreorder_44
v8 AgdaAny
v9 AgdaAny
v10
  = T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny
du_refl_80 T_IsIndexedPreorder_44
v8 AgdaAny
v9 AgdaAny
v10
du_refl_80 ::
  T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny
du_refl_80 :: T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny
du_refl_80 T_IsIndexedPreorder_44
v0 AgdaAny
v1 AgdaAny
v2
  = (T_IsIndexedPreorder_44
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsIndexedPreorder_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsIndexedPreorder_44
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_66 T_IsIndexedPreorder_44
v0 AgdaAny
v1 AgdaAny
v1 AgdaAny
v2 AgdaAny
v2
      ((T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny
d_refl_30 (T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22
d_isEquivalence_60 (T_IsIndexedPreorder_44 -> T_IsIndexedPreorder_44
forall a b. a -> b
coe T_IsIndexedPreorder_44
v0)) AgdaAny
v1 AgdaAny
v2)