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)

------------------------------------------------------------------------------

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)

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'.

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