ExerMini.agda

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:
postulate
  extensionality : ∀ {a b : Level} {A : Set a} {B : A → Set b}
    {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g
-}


-- Exercise ∀-×:

data Tri : Set where
  aa : Tri
  bb : Tri
  cc : Tri

∀-× : {B : Tri → Set} → (∀ (x : Tri) → B x) ≃ B aa × B bb × B cc
∀-× =
  record
    { to      = λ{ f → ⟨ f aa , ⟨ f bb , f cc ⟩ ⟩ }
    ; from    = λ{ ⟨ a , ⟨ b , c ⟩ ⟩ → λ{ aa → a
                                      ; bb → b
                                      ; cc → c
                                      }}
    ; from∘to = λ{ f → extensionality λ{ aa → refl
                                       ; bb → refl
                                       ; cc → refl
                                       }}
    ; to∘from = λ{ ⟨ a , ⟨ b , c ⟩ ⟩ → refl }
    }