{-# 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.Equivalence 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.Function.Equality
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Function.Equivalence.Equivalence
d_Equivalence_16 :: p -> p -> p -> p -> p -> p -> ()
d_Equivalence_16 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_Equivalence_16
  = C_Equivalence'46'constructor_433 MAlonzo.Code.Function.Equality.T_Π_16
                                     MAlonzo.Code.Function.Equality.T_Π_16
-- Function.Equivalence.Equivalence.to
d_to_34 ::
  T_Equivalence_16 -> MAlonzo.Code.Function.Equality.T_Π_16
d_to_34 :: T_Equivalence_16 -> T_Π_16
d_to_34 T_Equivalence_16
v0
  = case T_Equivalence_16 -> T_Equivalence_16
forall a b. a -> b
coe T_Equivalence_16
v0 of
      C_Equivalence'46'constructor_433 T_Π_16
v1 T_Π_16
v2 -> T_Π_16 -> T_Π_16
forall a b. a -> b
coe T_Π_16
v1
      T_Equivalence_16
_ -> T_Π_16
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Equivalence.Equivalence.from
d_from_36 ::
  T_Equivalence_16 -> MAlonzo.Code.Function.Equality.T_Π_16
d_from_36 :: T_Equivalence_16 -> T_Π_16
d_from_36 T_Equivalence_16
v0
  = case T_Equivalence_16 -> T_Equivalence_16
forall a b. a -> b
coe T_Equivalence_16
v0 of
      C_Equivalence'46'constructor_433 T_Π_16
v1 T_Π_16
v2 -> T_Π_16 -> T_Π_16
forall a b. a -> b
coe T_Π_16
v2
      T_Equivalence_16
_ -> T_Π_16
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Equivalence._⇔_
d__'8660'__42 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> () -> ()
d__'8660'__42 :: () -> () -> () -> () -> ()
d__'8660'__42 = () -> () -> () -> () -> ()
forall a. a
erased
-- Function.Equivalence.equivalence
d_equivalence_56 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_16
d_equivalence_56 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Equivalence_16
d_equivalence_56 ~()
v0 ~()
v1 ~()
v2 ~()
v3 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 = (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_16
du_equivalence_56 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5
du_equivalence_56 ::
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_16
du_equivalence_56 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_16
du_equivalence_56 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny
v1
  = (T_Π_16 -> T_Π_16 -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
      T_Π_16 -> T_Π_16 -> T_Equivalence_16
C_Equivalence'46'constructor_433
      ((T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Π_16)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Π_16
MAlonzo.Code.Relation.Binary.PropositionalEquality.du_'8594''45'to'45''10230'_68
         ((T_IsEquivalence_26 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_727
            (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_743
               AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased))
         AgdaAny -> AgdaAny
v0)
      ((T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Π_16)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Π_16
MAlonzo.Code.Relation.Binary.PropositionalEquality.du_'8594''45'to'45''10230'_68
         ((T_IsEquivalence_26 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_727
            (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_743
               AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased))
         AgdaAny -> AgdaAny
v1)
-- Function.Equivalence.id
d_id_66 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_Equivalence_16
d_id_66 :: () -> () -> T_Setoid_44 -> T_Equivalence_16
d_id_66 ~()
v0 ~()
v1 ~T_Setoid_44
v2 = T_Equivalence_16
du_id_66
du_id_66 :: T_Equivalence_16
du_id_66 :: T_Equivalence_16
du_id_66
  = (T_Π_16 -> T_Π_16 -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
      T_Π_16 -> T_Π_16 -> T_Equivalence_16
C_Equivalence'46'constructor_433
      (T_Π_16 -> AgdaAny
forall a b. a -> b
coe T_Π_16
MAlonzo.Code.Function.Equality.du_id_62)
      (T_Π_16 -> AgdaAny
forall a b. a -> b
coe T_Π_16
MAlonzo.Code.Function.Equality.du_id_62)
-- Function.Equivalence._∘_
d__'8728'__82 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16
d__'8728'__82 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Equivalence_16
-> T_Equivalence_16
-> T_Equivalence_16
d__'8728'__82 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~T_Setoid_44
v6 ~T_Setoid_44
v7 ~T_Setoid_44
v8 T_Equivalence_16
v9 T_Equivalence_16
v10
  = T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16
du__'8728'__82 T_Equivalence_16
v9 T_Equivalence_16
v10
du__'8728'__82 ::
  T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16
du__'8728'__82 :: T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16
du__'8728'__82 T_Equivalence_16
v0 T_Equivalence_16
v1
  = (T_Π_16 -> T_Π_16 -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
      T_Π_16 -> T_Π_16 -> T_Equivalence_16
C_Equivalence'46'constructor_433
      ((T_Π_16 -> T_Π_16 -> T_Π_16) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Π_16 -> T_Π_16 -> T_Π_16
MAlonzo.Code.Function.Equality.du__'8728'__82
         ((T_Equivalence_16 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16 -> T_Π_16
d_to_34 (T_Equivalence_16 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16
v0)) ((T_Equivalence_16 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16 -> T_Π_16
d_to_34 (T_Equivalence_16 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16
v1)))
      ((T_Π_16 -> T_Π_16 -> T_Π_16) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Π_16 -> T_Π_16 -> T_Π_16
MAlonzo.Code.Function.Equality.du__'8728'__82
         ((T_Equivalence_16 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16 -> T_Π_16
d_from_36 (T_Equivalence_16 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16
v1)) ((T_Equivalence_16 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16 -> T_Π_16
d_from_36 (T_Equivalence_16 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16
v0)))
-- Function.Equivalence.sym
d_sym_100 ::
  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.Bundles.T_Setoid_44 ->
  T_Equivalence_16 -> T_Equivalence_16
d_sym_100 :: ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> T_Equivalence_16
-> T_Equivalence_16
d_sym_100 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 T_Equivalence_16
v6 = T_Equivalence_16 -> T_Equivalence_16
du_sym_100 T_Equivalence_16
v6
du_sym_100 :: T_Equivalence_16 -> T_Equivalence_16
du_sym_100 :: T_Equivalence_16 -> T_Equivalence_16
du_sym_100 T_Equivalence_16
v0
  = (T_Π_16 -> T_Π_16 -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
      T_Π_16 -> T_Π_16 -> T_Equivalence_16
C_Equivalence'46'constructor_433 ((T_Equivalence_16 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16 -> T_Π_16
d_from_36 (T_Equivalence_16 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16
v0))
      ((T_Equivalence_16 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16 -> T_Π_16
d_to_34 (T_Equivalence_16 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16
v0))
-- Function.Equivalence._._.from
d_from_110 ::
  T_Equivalence_16 -> MAlonzo.Code.Function.Equality.T_Π_16
d_from_110 :: T_Equivalence_16 -> T_Π_16
d_from_110 T_Equivalence_16
v0 = (T_Equivalence_16 -> T_Π_16) -> AgdaAny -> T_Π_16
forall a b. a -> b
coe T_Equivalence_16 -> T_Π_16
d_from_36 (T_Equivalence_16 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16
v0)
-- Function.Equivalence._._.to
d_to_112 ::
  T_Equivalence_16 -> MAlonzo.Code.Function.Equality.T_Π_16
d_to_112 :: T_Equivalence_16 -> T_Π_16
d_to_112 T_Equivalence_16
v0 = (T_Equivalence_16 -> T_Π_16) -> AgdaAny -> T_Π_16
forall a b. a -> b
coe T_Equivalence_16 -> T_Π_16
d_to_34 (T_Equivalence_16 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16
v0)
-- Function.Equivalence.setoid
d_setoid_118 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_setoid_118 :: () -> () -> T_Setoid_44
d_setoid_118 ~()
v0 ~()
v1 = T_Setoid_44
du_setoid_118
du_setoid_118 :: MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_setoid_118 :: T_Setoid_44
du_setoid_118
  = (T_IsEquivalence_26 -> T_Setoid_44) -> AgdaAny -> T_Setoid_44
forall a b. a -> b
coe
      T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_727
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_743
         (\ AgdaAny
v0 -> T_Equivalence_16 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16
du_id_66) (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> (T_Equivalence_16 -> T_Equivalence_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16 -> T_Equivalence_16
du_sym_100 AgdaAny
v2)
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> (T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16
du__'8728'__82 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))))
-- Function.Equivalence.⇔-setoid
d_'8660''45'setoid_126 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_'8660''45'setoid_126 :: () -> T_Setoid_44
d_'8660''45'setoid_126 ~()
v0 = T_Setoid_44
du_'8660''45'setoid_126
du_'8660''45'setoid_126 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_'8660''45'setoid_126 :: T_Setoid_44
du_'8660''45'setoid_126
  = (T_IsEquivalence_26 -> T_Setoid_44) -> AgdaAny -> T_Setoid_44
forall a b. a -> b
coe
      T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_727
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_743
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> T_Equivalence_16 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16
du_id_66)) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 -> (T_Equivalence_16 -> T_Equivalence_16) -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16 -> T_Equivalence_16
du_sym_100))
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> (T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16
du__'8728'__82 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))))
-- Function.Equivalence.map
d_map_154 ::
  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.Bundles.T_Setoid_44 ->
  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.Bundles.T_Setoid_44 ->
  (MAlonzo.Code.Function.Equality.T_Π_16 ->
   MAlonzo.Code.Function.Equality.T_Π_16) ->
  (MAlonzo.Code.Function.Equality.T_Π_16 ->
   MAlonzo.Code.Function.Equality.T_Π_16) ->
  T_Equivalence_16 -> T_Equivalence_16
d_map_154 :: ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> (T_Π_16 -> T_Π_16)
-> (T_Π_16 -> T_Π_16)
-> T_Equivalence_16
-> T_Equivalence_16
d_map_154 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 ~()
v6 ~()
v7 ~()
v8 ~()
v9 ~T_Setoid_44
v10 ~T_Setoid_44
v11 T_Π_16 -> T_Π_16
v12 T_Π_16 -> T_Π_16
v13
          T_Equivalence_16
v14
  = (T_Π_16 -> T_Π_16)
-> (T_Π_16 -> T_Π_16) -> T_Equivalence_16 -> T_Equivalence_16
du_map_154 T_Π_16 -> T_Π_16
v12 T_Π_16 -> T_Π_16
v13 T_Equivalence_16
v14
du_map_154 ::
  (MAlonzo.Code.Function.Equality.T_Π_16 ->
   MAlonzo.Code.Function.Equality.T_Π_16) ->
  (MAlonzo.Code.Function.Equality.T_Π_16 ->
   MAlonzo.Code.Function.Equality.T_Π_16) ->
  T_Equivalence_16 -> T_Equivalence_16
du_map_154 :: (T_Π_16 -> T_Π_16)
-> (T_Π_16 -> T_Π_16) -> T_Equivalence_16 -> T_Equivalence_16
du_map_154 T_Π_16 -> T_Π_16
v0 T_Π_16 -> T_Π_16
v1 T_Equivalence_16
v2
  = (T_Π_16 -> T_Π_16 -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
      T_Π_16 -> T_Π_16 -> T_Equivalence_16
C_Equivalence'46'constructor_433 ((T_Π_16 -> T_Π_16) -> T_Π_16 -> AgdaAny
forall a b. a -> b
coe T_Π_16 -> T_Π_16
v0 (T_Equivalence_16 -> T_Π_16
d_to_34 (T_Equivalence_16 -> T_Equivalence_16
forall a b. a -> b
coe T_Equivalence_16
v2)))
      ((T_Π_16 -> T_Π_16) -> T_Π_16 -> AgdaAny
forall a b. a -> b
coe T_Π_16 -> T_Π_16
v1 (T_Equivalence_16 -> T_Π_16
d_from_36 (T_Equivalence_16 -> T_Equivalence_16
forall a b. a -> b
coe T_Equivalence_16
v2)))
-- Function.Equivalence._._.from
d_from_168 ::
  T_Equivalence_16 -> MAlonzo.Code.Function.Equality.T_Π_16
d_from_168 :: T_Equivalence_16 -> T_Π_16
d_from_168 T_Equivalence_16
v0 = (T_Equivalence_16 -> T_Π_16) -> AgdaAny -> T_Π_16
forall a b. a -> b
coe T_Equivalence_16 -> T_Π_16
d_from_36 (T_Equivalence_16 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16
v0)
-- Function.Equivalence._._.to
d_to_170 ::
  T_Equivalence_16 -> MAlonzo.Code.Function.Equality.T_Π_16
d_to_170 :: T_Equivalence_16 -> T_Π_16
d_to_170 T_Equivalence_16
v0 = (T_Equivalence_16 -> T_Π_16) -> AgdaAny -> T_Π_16
forall a b. a -> b
coe T_Equivalence_16 -> T_Π_16
d_to_34 (T_Equivalence_16 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16
v0)
-- Function.Equivalence.zip
d_zip_208 ::
  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.Bundles.T_Setoid_44 ->
  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.Bundles.T_Setoid_44 ->
  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.Bundles.T_Setoid_44 ->
  (MAlonzo.Code.Function.Equality.T_Π_16 ->
   MAlonzo.Code.Function.Equality.T_Π_16 ->
   MAlonzo.Code.Function.Equality.T_Π_16) ->
  (MAlonzo.Code.Function.Equality.T_Π_16 ->
   MAlonzo.Code.Function.Equality.T_Π_16 ->
   MAlonzo.Code.Function.Equality.T_Π_16) ->
  T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16
d_zip_208 :: ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_Setoid_44
-> (T_Π_16 -> T_Π_16 -> T_Π_16)
-> (T_Π_16 -> T_Π_16 -> T_Π_16)
-> T_Equivalence_16
-> T_Equivalence_16
-> T_Equivalence_16
d_zip_208 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 ~()
v6 ~()
v7 ~()
v8 ~()
v9 ~T_Setoid_44
v10 ~T_Setoid_44
v11 ~()
v12
          ~()
v13 ~()
v14 ~()
v15 ~T_Setoid_44
v16 ~T_Setoid_44
v17 T_Π_16 -> T_Π_16 -> T_Π_16
v18 T_Π_16 -> T_Π_16 -> T_Π_16
v19 T_Equivalence_16
v20 T_Equivalence_16
v21
  = (T_Π_16 -> T_Π_16 -> T_Π_16)
-> (T_Π_16 -> T_Π_16 -> T_Π_16)
-> T_Equivalence_16
-> T_Equivalence_16
-> T_Equivalence_16
du_zip_208 T_Π_16 -> T_Π_16 -> T_Π_16
v18 T_Π_16 -> T_Π_16 -> T_Π_16
v19 T_Equivalence_16
v20 T_Equivalence_16
v21
du_zip_208 ::
  (MAlonzo.Code.Function.Equality.T_Π_16 ->
   MAlonzo.Code.Function.Equality.T_Π_16 ->
   MAlonzo.Code.Function.Equality.T_Π_16) ->
  (MAlonzo.Code.Function.Equality.T_Π_16 ->
   MAlonzo.Code.Function.Equality.T_Π_16 ->
   MAlonzo.Code.Function.Equality.T_Π_16) ->
  T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16
du_zip_208 :: (T_Π_16 -> T_Π_16 -> T_Π_16)
-> (T_Π_16 -> T_Π_16 -> T_Π_16)
-> T_Equivalence_16
-> T_Equivalence_16
-> T_Equivalence_16
du_zip_208 T_Π_16 -> T_Π_16 -> T_Π_16
v0 T_Π_16 -> T_Π_16 -> T_Π_16
v1 T_Equivalence_16
v2 T_Equivalence_16
v3
  = (T_Π_16 -> T_Π_16 -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
      T_Π_16 -> T_Π_16 -> T_Equivalence_16
C_Equivalence'46'constructor_433
      ((T_Π_16 -> T_Π_16 -> T_Π_16) -> T_Π_16 -> T_Π_16 -> AgdaAny
forall a b. a -> b
coe T_Π_16 -> T_Π_16 -> T_Π_16
v0 (T_Equivalence_16 -> T_Π_16
d_to_34 (T_Equivalence_16 -> T_Equivalence_16
forall a b. a -> b
coe T_Equivalence_16
v2)) (T_Equivalence_16 -> T_Π_16
d_to_34 (T_Equivalence_16 -> T_Equivalence_16
forall a b. a -> b
coe T_Equivalence_16
v3)))
      ((T_Π_16 -> T_Π_16 -> T_Π_16) -> T_Π_16 -> T_Π_16 -> AgdaAny
forall a b. a -> b
coe T_Π_16 -> T_Π_16 -> T_Π_16
v1 (T_Equivalence_16 -> T_Π_16
d_from_36 (T_Equivalence_16 -> T_Equivalence_16
forall a b. a -> b
coe T_Equivalence_16
v2)) (T_Equivalence_16 -> T_Π_16
d_from_36 (T_Equivalence_16 -> T_Equivalence_16
forall a b. a -> b
coe T_Equivalence_16
v3)))