Skip to content

Instantly share code, notes, and snippets.

@collares
Last active May 16, 2019 16:30
Show Gist options
  • Save collares/5afa808eef7f647190e0dea244e6eb50 to your computer and use it in GitHub Desktop.
Save collares/5afa808eef7f647190e0dea244e6eb50 to your computer and use it in GitHub Desktop.
module plfa.Minimized where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import Function using (_∘_)
data _×_ (A B : Set) : Set where
⟨_,_⟩ : A → B → A × B
proj₁ : ∀ {A B : Set} → A × B → A
proj₁ ⟨ x , y ⟩ = x
proj₂ : ∀ {A B : Set} → A × B → B
proj₂ ⟨ x , y ⟩ = y
postulate
extensionality : ∀ {A B : Set} {f g : A → B}
→ (∀ (x : A) → f x ≡ g x)
→ f ≡ g
{-
With the following version of extensionality, the code compiles:
postulate
extensionality : ∀ {A : Set} {B : A → Set} {f g : (x : A) → B x}
→ (∀ (x : A) → f x ≡ g x)
→ f ≡ g
-}
infix 0 _≃_
record _≃_ (A B : Set) : Set where
field
to : A → B
from : B → A
from∘to : ∀ (x : A) → from (to x) ≡ x
to∘from : ∀ (y : B) → to (from y) ≡ y
open _≃_
η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w
η-× ⟨ x , y ⟩ = refl
∀-distrib-× : ∀ {A : Set} {B C : A → Set} →
(∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x)
∀-distrib-× =
record
{ to = λ{ f → ⟨ proj₁ ∘ f , proj₂ ∘ f ⟩ }
; from = λ{ ⟨ f , g ⟩ → λ { a → ⟨ f a , g a ⟩ } }
; from∘to = λ{ f → extensionality (η-× ∘ f) }
; to∘from = λ{ ⟨ f , g ⟩ → refl }
}
{-
from∘to fails to typecheck with this error message:
Cannot instantiate the metavariable _96 to solution .B x × .C x
since it contains the variable x which is not in scope of the
metavariable or irrelevant in the metavariable but relevant in the
solution
when checking that the inferred type of an application
_f_97 f ≡ _g_98 f
matches the expected type
(λ { ⟨ f , g ⟩ → λ { a → ⟨ f a , g a ⟩ } })
((λ { f → ⟨ (λ x → proj₁ (f x)) , (λ x → proj₂ (f x)) ⟩ }) f)
≡ f
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment