module Lib.Sigma where

open import Lib.Two
open import Lib.Hide

record Σ { l } (S : Set l) (T : S → Set l) : Set l where
  constructor _,_
  field  fst : S
         snd : T fst

open Σ public
infixr  _,_

p q r : { A : Set } { B : A → Set } → (a : A) → (b : (x : A) → B x) → Σ A B

p a b = record{ fst = a ; snd = b a }

q a b = a , (b a)

fst (r a b) = a
snd (r a b) = b a

_×_ : forall{ l } → Set l → Set l → Set l
S × T = Σ S λ _ → T
infixr  _×_

mapΣ : forall{k l}{S : Set k}{S' : Set l}{T : S → Set k}{T' : S' → Set l}
     → (f : S → S') → (g : {s : S} → T s → T' (f s))
     → Σ S T → Σ S' T'
mapΣ f g (s , t) = f s , g t

-- sums

_+_ : Set → Set → Set
A + B = Σ Two λ { ff → A ; tt → B }

pattern inl A = ff , A
pattern inr B = tt , B

hideΣ : {X Y : Set} → Hide X → Hide Y → Hide (X × Y)
hideΣ (hide x) (hide y) = hide (x , y)


hide→' : {X Y : Set} → Hide (X → Y) → (X → Hide Y)
hide→' (hide f) = λ x → hide (f x)


hideP : {X Y Z : Set} → Hide ((X × Y) × Z) → Hide X
hideP (hide xyz) = hide (fst (fst xyz))


assocΣr : {X : Set} {Y : X → Set} {Z : (x : X) → Y x → Set}
        → (Σ (Σ X Y) \ (x , y) → Z x y)
        → Σ X \ x → Σ (Y x) (Z x)
assocΣr  ((x , y) , z) = x , (y , z)

assocΣl : {X : Set} → {Y : X → Set} → {Z : (x : X) → Y x → Set}
          → (Σ X \ x → Σ (Y x) (Z x))
          → Σ (Σ X Y) \ (x , y) → Z x y
assocΣl (x , (y , z)) = ((x , y) , z)