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

-- Function.Dependent.Bundles._._._≈_
d__'8776'__32 ::
  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_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.T_IndexedSetoid_18 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__32 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_IndexedSetoid_18
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8776'__32 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_IndexedSetoid_18
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Function.Dependent.Bundles._._.Carrier
d_Carrier_34 ::
  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_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.T_IndexedSetoid_18 ->
  ()
d_Carrier_34 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_IndexedSetoid_18
-> T_Level_18
d_Carrier_34 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_IndexedSetoid_18
-> T_Level_18
forall a. a
erased
-- Function.Dependent.Bundles._.Func
d_Func_42 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_Func_42 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_Func_42
  = C_Func'46'constructor_677 (AgdaAny -> AgdaAny)
                              (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-- Function.Dependent.Bundles._.Func.to
d_to_56 :: T_Func_42 -> AgdaAny -> AgdaAny
d_to_56 :: T_Func_42 -> AgdaAny -> AgdaAny
d_to_56 T_Func_42
v0
  = case T_Func_42 -> T_Func_42
forall a b. a -> b
coe T_Func_42
v0 of
      C_Func'46'constructor_677 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1
      T_Func_42
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Dependent.Bundles._.Func.cong
d_cong_62 :: T_Func_42 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_62 :: T_Func_42 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_62 T_Func_42
v0
  = case T_Func_42 -> T_Func_42
forall a b. a -> b
coe T_Func_42
v0 of
      C_Func'46'constructor_677 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2
      T_Func_42
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError