Skip to content

Instantly share code, notes, and snippets.

@mietek

mietek/Sigma.agda

Last active September 20, 2021 19:21
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save mietek/d53a0e3aa52078969d9f0d74e1aad462 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save mietek/d53a0e3aa52078969d9f0d74e1aad462 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Sigma.agda
-- To simplify defining ChurchSigma.
{-# OPTIONS --type-in-type #-}
module Sigma where
open import Axiom.Extensionality.Propositional using (Extensionality)
open import Level using (_βŠ”_)
open import Relation.Binary.PropositionalEquality using (_≑_ ; refl ; module ≑-Reasoning)
open ≑-Reasoning
-- Pointwise equality.
_≐_ : βˆ€ {a b} {A : Set a} {B : A β†’ Set b} (f g : βˆ€ (x : A) β†’ B x) β†’ Set (a βŠ” b)
f ≐ g = βˆ€ x β†’ f x ≑ g x
------------------------------------------------------------------------------
-- The negative view, as a record, to enjoy definitional eta.
record Sigma {a b} (A : Set a) (B : A β†’ Set b) : Set (a βŠ” b) where
constructor _,_
field
proj₁ : A
projβ‚‚ : B proj₁
open Sigma
-- Local soundness.
neg-beta₁ : βˆ€ {a b} {A : Set a} {B : A β†’ Set b}
(x : A) (y : B x) β†’
proj₁ {B = B} (x , y) ≑ x
neg-beta₁ x y = refl
neg-betaβ‚‚ : βˆ€ {a b} {A : Set a} {B : A β†’ Set b}
(x : A) (y : B x) β†’
projβ‚‚ {B = B} (x , y) ≑ y
neg-betaβ‚‚ x y = refl
-- Local completeness.
neg-eta : βˆ€ {a b} {A : Set a} {B : A β†’ Set b}
(s : Sigma A B) β†’
s ≑ proj₁ s , projβ‚‚ s
neg-eta s = refl
------------------------------------------------------------------------------
-- The positive view.
case : βˆ€ {a b c} {A : Set a} {B : A β†’ Set b} (C : Sigma A B β†’ Set c) β†’
(s : Sigma A B) β†’
(βˆ€ (x : A) (y : B x) β†’ C (x , y)) β†’
C s
case C (x , y) f = f x y
pos-proj₁ : βˆ€ {a b} {A : Set a} {B : A β†’ Set b} β†’
Sigma A B β†’ A
pos-proj₁ s = case _ s Ξ» x y β†’ x
pos-projβ‚‚ : βˆ€ {a b} {A : Set a} {B : A β†’ Set b} β†’
(s : Sigma A B) β†’ B (pos-proj₁ s)
pos-projβ‚‚ s = case _ s Ξ» x y β†’ y
-- Local soundness.
pos-beta : βˆ€ {a b c} {A : Set a} {B : A β†’ Set b} {C : Sigma A B β†’ Set c} β†’
(x : A) (y : B x) (f : βˆ€ (x : A) (y : B x) β†’ C (x , y)) β†’
case _ (x , y) f ≑ f x y
pos-beta x y f = refl
-- Local completeness.
pos-eta : βˆ€ {a b} {A : Set a} {B : A β†’ Set b} β†’
(s : Sigma A B) β†’
s ≑ case _ s (Ξ» x y β†’ x , y)
pos-eta s = refl
------------------------------------------------------------------------------
-- The non-dependent positive view.
caseβ€² : βˆ€ {a b c} {A : Set a} {B : A β†’ Set b} {C : Set c} β†’
(s : Sigma A B) β†’
(βˆ€ (x : A) (y : B x) β†’ C) β†’
C
caseβ€² = case _
pos-proj₁′ : βˆ€ {a b} {A : Set a} {B : A β†’ Set b} β†’
Sigma A B β†’ A
pos-proj₁′ s = caseβ€² s Ξ» x y β†’ x
-- NOTE: This is not provable, because the type of the continuation does not carry enough information.
pos-projβ‚‚β€² : βˆ€ {a b} {A : Set a} {B : A β†’ Set b} β†’
(s : Sigma A B) β†’ B (pos-proj₁′ s)
pos-projβ‚‚β€² s = caseβ€² s Ξ» x y β†’ {!y!}
-- Goal: B (pos-proj₁′ s)
-- Have: B x
------------------------------------------------------------------------------
-- The attempted Church encoding, using type-in-type for simplicity.
ChurchSigma : βˆ€ (A : Set) (B : A β†’ Set) β†’ Set
ChurchSigma A B = βˆ€ {C : Set} β†’
(βˆ€ (x : A) (y : B x) β†’ C) β†’
C
church-proj₁ : βˆ€ {A B} β†’ ChurchSigma A B β†’ A
church-proj₁ s = s (Ξ» x y β†’ x)
-- NOTE: This is likewise not provable.
church-projβ‚‚ : βˆ€ {A B} (s : ChurchSigma A B) β†’ B (church-proj₁ s)
church-projβ‚‚ s = s (Ξ» x y β†’ {!y!})
-- Goal: B (church-proj₁ s)
-- Have: B x
enchurch : βˆ€ {A B} β†’ Sigma A B β†’ ChurchSigma A B
enchurch s = Ξ» f β†’ caseβ€² s f
dechurch : βˆ€ {A B} β†’ ChurchSigma A B β†’ Sigma A B
dechurch s = s _,_
church-iso₁ : βˆ€ {A B} (s : Sigma A B) β†’
dechurch (enchurch s) ≑ s
church-iso₁ s = refl
-- NOTE: A similar problem appears here.
church-pre-isoβ‚‚ : βˆ€ {A B C} (s : ChurchSigma A B) β†’
enchurch (dechurch s) {C} ≐ s {C}
church-pre-isoβ‚‚ {C = C} s f =
begin
enchurch (dechurch s) f
β‰‘βŸ¨βŸ©
(Ξ» g β†’ g (proj₁ (dechurch s)) (projβ‚‚ (dechurch s))) f
β‰‘βŸ¨βŸ©
f (proj₁ (dechurch s)) (projβ‚‚ (dechurch s))
β‰‘βŸ¨ {!!} ⟩
s f
∎
-- Goal: f (proj₁ (dechurch s)) (projβ‚‚ (dechurch s)) ≑ s f
module _ (funext : Extensionality _ _) where
church-isoβ‚‚ : βˆ€ {A B C} (s : ChurchSigma A B) β†’
enchurch (dechurch s) {C} ≑ s {C}
church-isoβ‚‚ s = funext (church-pre-isoβ‚‚ s)
------------------------------------------------------------------------------
@Blaisorblade

Blaisorblade commented Sep 20, 2021

Copy link
Copy Markdown

I can't fill in the following. From this:

cfst : βˆ€ {A B} β†’ ChurchSigma A B β†’ A
cfst cs = cs (Ξ» x y β†’ x)

csnd : βˆ€ {A B} (s : ChurchSigma A B) β†’ B (cfst s)
csnd cs = cs (Ξ» x y β†’ {!y!})

I get:

Goal: B (cfst cs)
Have: B x
β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”
y  : B x
x  : A
cs : ChurchSigma A B
B  : A β†’ Set   (not in scope)
A  : Set   (not in scope)

@Blaisorblade

Blaisorblade commented Sep 20, 2021

Copy link
Copy Markdown

Ditto for:

sfst : βˆ€ {A B} (s : Sigma A B) β†’ A
sfst s = caseβ€² s Ξ» x y β†’ x

ssnd : βˆ€ {A B} (s : Sigma A B) β†’ B (sfst s)
-- ssnd (f , c) = c -- works
ssnd s = caseβ€² s Ξ» x y β†’ {!y!}
Goal: B (sfst s)
Have: B x
β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”
y : B x
x : A
s : Sigma A B
B : A β†’ Set   (not in scope)
A : Set   (not in scope)

I'm sure that's fixable by pattern-matching on s, but then we're not restricting ourselves to case'.

@mietek

mietek commented Sep 20, 2021

Copy link
Copy Markdown
Author

You’re right; updated to point out the problems.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment