help.agda

module help where

open import univ
open import Base

-- Prelims
infixl 150 _#_

K : {A : S} -> S -> Fam A
K B = fam (\_ -> B) (\_ -> refS)

_#_ : {A : S}{F : Fam A} -> El (pi A F) -> (x : El A) -> El (F ! x)
el < f , _ > # x = f x

pFun : {A : S}{F : Fam A}(f : El (pi A F)){x y : El A}(x=y : x == y) ->
       f # x == pFam F x=y << f # y
pFun (el < f , pf >) x=y = pf x=y

p# : {A : S}{F : Fam A}{f g : El (pi A F)}{x : El A} -> f == g -> f # x == g # x
p# {A}{F}{el < f , _ >}{el < g , _ >} (eq f=g) = f=g _

eqDom : {A B : S}{F : Fam A}{G : Fam B} ->
        pi A F =S pi B G -> B =S A
eqDom (eqS < B=A , _ >) = B=A

eqCod : {A B : S}{F : Fam A}{G : Fam B} ->
        (AF=BG : pi A F =S pi B G)(x : El A) ->
        F ! x =S G ! (eqDom AF=BG << x)
eqCod (eqS < B=A , F=G >) = F=G

distr<<# : {A B : S}{F : Fam A}{G : Fam B}(f : El (pi A F)){x : El B}
            (BG=AF : pi B G =S pi A F) ->
            (BG=AF << f) # x == eqCod BG=AF x << f # (eqDom BG=AF << x)
distr<<# (el < f , pf >) {x} (eqS < A=B , G=F >) = ref

eqSnd : {A : S}{F : Fam A}{x : El A}{y z : El (F ! x)} ->
        y == z -> _==_ {sigma A F} (el < x , y >) (el < x , z >)
eqSnd {A}{F}{x}{y}{z} y=z = eq < ref , y=cz >
  where
    y=cz : y == pFam F ref << z
    y=cz = trans y=z (sym (castref _ _))

IsFun : {A : S}{F : Fam A}(f : (x : El A) -> El (F ! x)) -> Set
IsFun {A}{F} f = {x y : El A}(p : F ! x =S F ! y)(x=y : x == y) ->
                 f x == p << f y

mkFun : {A : S}{F : Fam A}(f : (x : El A) -> El (F ! x)) ->
        IsFun {A}{F} f -> El (pi A F)
mkFun {A}{F} f pf = el < f , (\{x}{y} x=y -> pf (pFam F x=y) x=y) >

curryFam : {A : S}{F : Fam A} -> Fam (sigma A F) -> (x : El A) -> Fam (F ! x)
curryFam {A}{F} G x = fam H pH
  where
    H : El (F ! x) -> S
    H y = G ! el < x , y >

    pH : Map _==_ _=S_ H
    pH y=z = pFam G (eq < ref , trans y=z (sym (castref _ _)) >)