h4iku

module plfa.ExerMini where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
open import plfa.Isomorphism using (_≃_; extensionality)
-- open import Level using (Level)

{-
-- Works with the version posted in the issue: