--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
--Module       : Type.Function
--Author       : Daniel Schüssler
--License      : BSD3
--Copyright    : Daniel Schüssler
--
--Maintainer   : Daniel Schüssler
--Stability    : Experimental
--Portability  : Uses various GHC extensions
--
--------------------------------------------------------------------------------
--Description  : 
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------

{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE IncoherentInstances #-}



-- | Notes
--
-- * Functions are coded as functional relations (in particular, functions are sets)
--
-- * Extensional equality of functions coincedes with extensional equality of sets.
module Type.Function where
    
import Type.Logic
import Type.Set
import Data.Type.Equality
import Control.Arrow
import Helper
import Type.Dummies

    

#include "../Defs.hs"

    
-- * Preliminary
    
            
-- | Existential quantification over the first component of a pair
data ExSnd (f :: SET) (a :: *) :: * where
    ExSnd :: (a, ex) :∈: f -> ExSnd f a
            
-- | Totality
type Total dom f =
  (forall (a :: *). a :∈: dom -> ExSnd f a)            

-- | Single-valuedness (CPS)
type Sval f =
          (forall a b1 b2 r.

                   (a, b1) :∈: f -> 
                   (a, b2) :∈: f -> 
                   ((b1 ~ b2) => r) ->
                   r)

    
-- * Functions
            
-- | Functions are encoded as functional relations; the three arguments to the construcor are:
--
-- * Is a relation
--
-- * Totality
--
-- * Single-valuedness (CPS-encoded; using ':=:' would work just as well. I hope that the CPS variant makes the optimizer more happy, but this is pure speculation)
data ((dom :: SET) :~>: (cod :: SET)) :: SET1 where
    IsFun ::
           -- Is a relation
           (f :⊆: (dom :×: cod)) 

           -- Totality
       ->  Total dom f
              
       ->  Sval f
            
       ->  (dom :~>: cod) f
           
infixr 6 :~>:, :~~>:

-- | Functions are relations
                              
relation :: (dom :~>: cod) f -> f :⊆: (dom :×: cod)
relation (IsFun p _ _) = p
                         

-- | Functions are total
total :: (dom :~>: cod) f -> a :∈: dom -> ExSnd f a
total (IsFun _ p _) = p
                      

-- | /The detailed type variable names help debugging proofs/
totalCPS :: (dom :~>: cod) f -> a :∈: dom -> 
           (forall totalCPS_y. (a,totalCPS_y) :∈: f -> totalCPS_return) ->
               totalCPS_return
totalCPS f a k = case total f a of
                   ExSnd fab -> k fab


                      
-- | Functions are single-valued (reified equality version)
sval :: forall dom cod a b1 b2 f.
                (dom :~>: cod) f ->
                   (a, b1) :∈: f -> 
                   (a, b2) :∈: f -> 
                   b1 :=: b2
                      
sval f fab1 fab2 = svalCPS f fab1 fab2 (Refl :: b1 ~ b2 => b1 :=: b2)
-- | Perform coercion using the single-valuedness
svalCoerce :: forall dom cod a b1 b2 f.
                (dom :~>: cod) f ->
                   (a, b1) :∈: f -> 
                   (a, b2) :∈: f -> 
                       b1 -> b2
svalCoerce f p1 p2 x = svalCPS f p1 p2 (x :: b1 ~ b2 => b2)
                     
-- | Functions are single-valued (CPS version)
svalCPS :: (dom :~>: cod) f ->
                   (a, b1) :∈: f -> 
                   (a, b2) :∈: f -> 
                       
                   ((b1 ~ b2) => r) ->

                   r
svalCPS (IsFun _ _ p) fab1 fab2 k = p fab1 fab2 k 
                                    
svalCPS' :: (dom :~>: cod) f ->
                   (a, b1) :∈: f -> 
                   (a, b2) :∈: f -> 
                       
                   (b1 :=: b2 -> r) ->

                   r
svalCPS' (IsFun _ _ p) fab1 fab2 k = p fab1 fab2 (k Refl) 
                                    
                     
-- | Shortcut for unpacking 'relation'
rel :: (dom :~>: cod) f -> pair :∈: f -> pair :∈: (dom :×: cod)
rel f fp = relation f `scoerce` fp
           

relCPS :: (dom :~>: cod) f -> pair :∈: f -> 
         (forall relCPS_x relCPS_y. (pair ~ (relCPS_x,relCPS_y)) => dom relCPS_x -> cod relCPS_y -> relCPS_return)
         -> relCPS_return
relCPS f fxy k = case rel f fxy of
                   x :×: y -> k x y
                             

-- | If @f a = b@, then @a@ is in the domain of @f@
inDom :: (dom :~>: cod) f -> (a, b) :∈: f -> a :∈: dom
inDom f p = fstPrf (relation f `scoerce` p) 

-- | If @f a = b@, then @b@ is in the codomain of @f@
inCod :: (dom :~>: cod) f -> (a, b) :∈: f -> b :∈: cod
inCod f p = sndPrf (relation f `scoerce` p)
            
-- | The domain of a function is uniquely determined
domUniq :: (dom :~>: cod) f -> (dom2 :~>: cod) f -> dom :==: dom2
domUniq f f' = SetEq (domUniq0 f f') (domUniq0 f' f)
    where
      domUniq0 :: (dom :~>: cod) f -> (dom2 :~>: cod) f -> dom :⊆: dom2
      domUniq0 f f' = Subset (\a -> case total f a of
                                     ExSnd fa -> inDom f' fa)
                                                  
-- ** Set of functions

-- | Kind-casted variant (function space as a set)
--
-- Convention: Instances of 'Fact' should always prove ':~>:' rather than this type.
type (dom :~~>: cod) = Lower1 (dom :~>: cod)

-- data ((dom :: SET) :~~>: (cod :: SET)) :: SET where
--      IsFun' :: (dom :~>: cod) f -> (dom :~~>: cod) (Lower f)
              
instance (Fact ((dom :~>: cod) f), Lower f ~ lf) => (Fact ((dom :~~>: cod) lf))
    where
      auto = LowerElement auto

lowerFun :: (dom :~>: cod) f -> (dom :~~>: cod) (Lower f)
lowerFun = LowerElement
           
raiseFun :: (dom :~~>: cod) (Lower f) -> (dom :~>: cod) f
raiseFun (LowerElement x) = x
                     
-- | This is stronger than 'raiseFun' since it introduces the knowledge that @lf@ is of the form @Lower f@, rather than assuming it.
raiseFunCPS :: (dom :~~>: cod) lf -> 
              (forall f. (lf ~ Lower f) => (dom :~>: cod) f -> r) -> r
raiseFunCPS (LowerElement x) k = k x
                     
-- * Images

-- | Image of a set under the function
data Image (f :: SET) (s :: SET) :: SET where
    Image :: a :∈: s -> 
            (a, b) :∈: f -> 
            Image f s b
            
-- | Every image is a subset of every possible codomain
imageCod :: (dom :~>: cod) f -> Image f s :⊆: cod
imageCod f = Subset (\(Image _ p) -> inCod f p)
             
-- | The full image is a codomain
setCodToImage :: (dom :~>: cod) f -> (dom :~>: Image f dom) f
setCodToImage f = adjustCod f subsetRefl
                               
                     
-- | Change the codomain by proving that the full image is included in the new codomain
adjustCod :: (dom :~>: cod) f -> 
            (Image f dom :⊆: cod') 
          -> (dom :~>: cod') f
            
adjustCod f p = 
    IsFun (Subset (\fab -> case relation f `scoerce` fab of
                            p1 :×: _ -> p1 :×: p `scoerce` 
                                               (Image p1 fab )))

          (total f) (\p1 p2 k -> svalCPS f p1 p2 k)
                    

-- | Enlargen the codomain
extendCod :: (dom :~>: cod) f -> 
            (cod :⊆: cod')
          -> (dom :~>: cod') f
            
extendCod f q = adjustCod f (Subset (\(Image _ fab) -> q `scoerce` inCod f fab))
                
                
imageMonotonic :: (s1 :⊆: s2) -> Image f s1  :⊆: Image f s2 
imageMonotonic p = Subset( \(Image x fxy) -> Image (p `scoerce` x) fxy)
                   
imageEmpty :: Image f Empty :==: Empty
imageEmpty = SetEq (Subset (\(Image (Empty e) _) -> Empty e)) emptySubset
             

imageOfInclusion :: Image (Incl dom cod) s :==: (s :∩: dom)
imageOfInclusion = SetEq (Subset (\(Image s (Incl dom)) -> Inter s dom))
                         (Subset (\(Inter s dom) -> Image s (Incl dom)))
                         
fullImageOfInclusion :: dom :⊆: cod -> Image (Incl dom cod) dom :==: dom
fullImageOfInclusion s = imageOfInclusion `setEqTrans` interIdempotent

             
-- | Image distributes over union (in general not over intersection)
imageUnion :: forall dom cod s1 s2 f.
               (dom :~>: cod) f -> 
              
              (Image f (s1 :∪: s2)  )
              :==:
              (Image f s1 :∪: Image f s2)

imageUnion f = SetEq
               (Subset 
                (\(Image x fxy) -> case elimUnion x of
                                    Left x1 -> (Union . Left) (Image x1 fxy)
                                    Right x1 -> (Union . Right) (Image x1 fxy)))
               
               (unionMinimal
                (imageMonotonic auto)
                (imageMonotonic auto)
               )
                
                
                
instance (cod' ~ cod'_copy, Fact ((dom :~>: cod) f)) => 
    Fact (
            (cod :⊆: cod'_copy)
                -> (dom :~>: cod') f
         )
    where
      auto x = extendCod auto x
           
                               
                    
-- -- | This is a helper type for bringing the knowledge into scope that if @f pair@, and @f@ is a function, then @pair@ must be a tuple
-- data Rel (dom,cod) f pair where
--     Rel :: dom a -> cod b -> Rel (dom,cod) f (PAIR a b)
              
               
                               
-- * Equality

                                   
-- | Very useful lemma for proving equality of functions.
--
-- Given the properties of functions, it is enough to show that @f@ is a subset of @f'@ to prove @f = f'@.
funEq :: forall dom cod cod' f f'.
               (dom :~>: cod) f 
             -> (dom :~>: cod') f' 
             -> f :⊆: f' 
             -> f :==: f'

-- guardSameType :: a -> a -> b -> b
-- guardSameType _ _ = id

funEq f f' pSub = 
        SetEq pSub
           (Subset (\(f'ab :: ab :∈: f') -> 
                        relCPS f' f'ab
                          (\(a :: dom a) _ ->
                              totalCPS f a (\ (fab' :: (a,b') :∈: f) ->
                                    case pSub `scoerce` fab' of
                                      (f'ab' :: (a,b') :∈: f') -> 
                                                svalCPS f' f'ab' f'ab 
                                                        (fab' :: ab :∈: f))
                                           )))
                                                    

-- | 'funEq' with the inclusion argument flipped
funEq' ::
               (dom :~>: cod) f 
             -> (dom :~>: cod') f' 
             -> f' :⊆: f 
             -> f :==: f'

funEq' f f' pSub = setEqSym (funEq f' f pSub) 
                   

-- | Expresses the fact that /f = f' ==> f x = f' x/
equal_f :: (d :~>: c) f' -> 
          f :==: f' -> 
              (x,y) :∈: f -> 
              (x,y') :∈: f' -> 
                  y :=: y'
equal_f f' eq fxy fxy' = sval f' (eq `ecoerce` fxy) fxy'
                         
-- | Perform coercion using a function equality
equal_f_coerce :: (d :~>: c) f' -> 
             f :==: f' -> 
              (x,y) :∈: f -> 
              (x,y') :∈: f' -> 
                  y -> y'
equal_f_coerce f' eq fxy fxy' = coerce (equal_f f' eq fxy fxy')

isFun_congruence :: (d :~>: c) f ->
                   f :==: f' ->
                   (d :~>: c) f'

isFun_congruence f eq = IsFun
                        (Subset (\p -> rel f (eq `ecoerceFlip` p)))
                        (\p -> totalCPS f p (\fxy -> ExSnd (eq `ecoerce` fxy)))
                        (\p1 p2 k -> svalCPS f 
                                    (eq `ecoerceFlip` p1) 
                                    (eq `ecoerceFlip` p2)
                                    k)


-- * Inclusion functions, identity, composition
                     
-- | Inclusion function of a subset
--
-- Inclusions /do/ know their codomain (somewhat arbitrary design decision)
data Incl (dom :: SET) (cod :: SET) :: SET where
    Incl :: dom a -> Incl dom cod (a,a)
           
           
-- inclCoerce :: (pair1 EQUAL pair2) ->
--              Incl dc pair1 ->
--              Incl dc pair2
-- inclCoerce 
           

-- elimIncl :: pair ELEMENT Incl domcod -> 
--            (forall a b dom cod r. ((PAIR0 a b) :∈: Incl domcod) -> r (PAIR0 a b))
--            -> r pair
           
-- | Identity function on @dom@
type Id dom = Incl dom dom

-- | Inclusion is a function
inclusionIsFun :: dom :⊆: cod -> (dom :~>: cod) (Incl dom cod)
inclusionIsFun q = IsFun
                       (Subset (\(Incl p1) -> p1 :×: (q `scoerce` p1)))
                       (\p -> ExSnd (Incl p))
                       (\(Incl _) (Incl _) k -> k)
                       

instance (Fact (dom :⊆: cod))
    => Fact ((dom :~>: cod) (Incl dom cod))

        where
          auto = inclusionIsFun auto


                   
-- | Id is a function
idIsFun :: (dom :~>: dom) (Id dom)
idIsFun = inclusionIsFun subsetRefl
                              

-- | Composition
data ((g :: SET) :○: (f :: SET)) :: SET where
    Compo ::
            (b, c) :∈: g -> 
            (a, b) :∈: f -> 
            (g :○: f) (a, c)
            
infixr 5 :○:
                  
                       
-- | The composition is a function
compoIsFun :: (s2 :~>: s3) g -> 
             (s1 :~>: s2) f -> 
             (s1 :~>: s3) (g :○: f)
compoIsFun g f = 
            IsFun 
            (Subset (\(Compo gbc fab) -> case (rel g gbc, rel f fab) of
                                  (  _  :×: pc
                                   , pa :×: _  ) ->
                                                    pa :×: pc))

            (\p -> case total f p of
                    ExSnd fab ->
                        case total g (inCod f fab) of
                          ExSnd gbc -> 
                              ExSnd (Compo gbc fab))

            (\(Compo gbc fab) (Compo gbc' fab') k -> svalCPS f fab fab'
                                                    (svalCPS g gbc gbc' k)) 
                 -- case sval f fab fab' of
                 --   Refl -> case sval g gbc gbc' of
                 --            Refl -> Refl)
        
        
instance 
 ( Fact ( (s2 :~>: s3) g )
 , Fact ( (s1 :~>: s2) f ) 
 )

 =>
             Fact ((s1 :~>: s3) (g :○: f))
                  
                   where
                     auto = compoIsFun (auto :: (s2 :~>: s3) g) auto

-- | 'Id' is a left identity for composition                            
compo_idl :: (d :~>: c) f -> (Id c :○: f) :==: f
compo_idl f = funEq (compoIsFun idIsFun f) f
              (Subset (\(Compo (Incl y) fxy) -> fxy)) 
              
-- | 'Id' is a right identity for composition                       
compo_idr :: (d :~>: c) f -> (f :○: Id d) :==: f
compo_idr f = funEq (compoIsFun f idIsFun) f
              (Subset (\(Compo fxy (Incl x)) -> fxy)) 

              

compo_assoc
  ::
       (:~>:) s2 cod g
     -> (:~>:) s21 s2 f
     -> (:~>:) dom s21 f1
     -> ((g :○: f) :○: f1) :==: (g :○: (f :○: f1))

compo_assoc h g f = funEq ((compoIsFun h g) `compoIsFun` f)
                          (h `compoIsFun` (g `compoIsFun` f))
                          (Subset (\(Compo (Compo vh vg) vf) ->
                                       Compo vh (Compo vg vf)))
-- * Equalisers

-- | Equalisers :D
--
-- In our category, the equaliser of two parallel functions @f1@ and @f2@ is the set of types on which @f1@ and @f2@ agree; that is:
--
--     /Equaliser f1 f2 = { x | f1 x = f2 x }/
data Equaliser (f1 :: SET) (f2 :: SET) :: SET where
    Equaliser :: (a, b) :∈: f1 -> (a, b) :∈: f2 -> Equaliser f1 f2 a
                
-- | Inclusion of the equaliser into the domain of the parallel functions
type EqualiserIncl s f1 f2 = Incl (Equaliser f1 f2) s
    
    
-- | The equaliser is a subset of the domain of the parallel functions 
equaliserSubset :: (s :~>: t) f1 
                  ->  (Equaliser f1 f2) :⊆: s 
  
equaliserSubset f = Subset (\(Equaliser p _) -> inDom f p)
                     



     
-- | The equaliser inclusion is a function
equaliserIsFun ::  (s :~>: t) f1 
                   -> ((Equaliser f1 f2) :~>: s) 
                     (EqualiserIncl s f1 f2)
                     
equaliserIsFun f = inclusionIsFun (equaliserSubset f)
                    
    
-- The mediator is the same as the original function...

-- data EqualiserMed f1 f2 g :: (* -> * -> *) where
--     EqualiserMed :: Compo f1 g d a
--                  -> Compo f2 g d a
--                  -> EqualiserMed f1 f2 g d a

-- restrictDom :: IsFun (dom,cod) f -> (Subset dom' dom) -> IsFun dom' cod f
-- restrictDom (IsFun t s d c) (Subset p) = IsFun t s d (p . c)


                       
-- | Universal property of equalisers:
--
-- @f1 . g = f2 . g@ ==> @g@ factors uniquely through @Equaliser f1 f2@
--
-- Uniqueness is trivial in our case because the function into the equaliser is
-- identical to @g@ (our functions don't know their codomain)
equaliserUni ::      (s0 :~>: s) g
                  -> (s  :~>: t) f1
                  -> (f1 :○: g) :==: (f2 :○: g)
                  -> (s0 :~>: (Equaliser f1 f2)) g 

equaliserUni g f1 pEq = 

          adjustCod g
           (Subset (\(Image _ gab) -> 
                case total f1 (inCod g gab) of
                  ExSnd f1bc -> 
                      case pEq `ecoerce` (Compo f1bc gab) of
                        Compo f2b'c gab' ->
                            case sval g gab gab' of
                              Refl -> Equaliser f1bc f2b'c))


-- * Injectivity

-- | Injective functions
--
-- (NB: Surjectivity is meaningless here because our functions don't know their codomain, but we have 'Image')
data Injective (f :: SET) :: * where
    Injective :: (forall a1 a2 b r.
                       ( a1, b) :∈: f -> 
                       ( a2, b) :∈: f -> 
                           (a1 ~ a2 => r) ->
                               r)
                
                -> Injective f
              
                  
injective :: forall f a1 a2 b . 
            Injective f -> ((a1, b) :∈: f) -> ((a2, b) :∈: f) -> 
            a1 :=: a2
               
injective (Injective p) p1 p2 = p p1 p2 (Refl :: (a1 ~ a2) => a1 :=: a2)
                                

inclusion_Injective :: Injective (Incl dom cod)
inclusion_Injective = Injective (\(Incl _) (Incl _) k -> k) 

                          
-- data Surjective (f :: SET) :: PROP where 
--     Surjective :: (forall b. Image f b) -> Surjective f
               


-- * Preimages

                  
data Preimage (f :: SET) (s :: SET) :: SET where
                    Preimage :: (a, b) :∈: f -> b :∈: s -> Preimage f s a
              
                               
preimage_Image :: 
    (dom :~>: cod) f ->
    set :⊆: dom -> 
    set :⊆: Preimage f (Image f set)
        
preimage_Image f s = Subset 
                     (\x -> 
                          let
                              dom_x = s `scoerce` x
                          in
                            totalCPS f dom_x
                             (\fxy -> Preimage fxy (Image x fxy)))

image_Preimage ::
    (dom :~>: cod) f ->
    Image f (Preimage f set) :⊆: set
        
image_Preimage f = Subset 
                     (\(Image (Preimage fxy y) fxy') -> case sval f fxy fxy' of
                                                         Refl -> y)
                        

-- * Binary product projections, target tupling

data Fst (s1 :: SET) (s2 :: SET) :: SET where 
                 Fst :: a :∈: s1 -> b :∈: s2 -> Fst s1 s2 ((,) ((,) a b) a)
data Snd (s1 :: SET) (s2 :: SET) :: SET where 
                 Snd :: a :∈: s1 -> b :∈: s2 -> Snd s1 s2 ((,) ((,) a b) b)
                                     
-- | Analogous to '***'
data ((f1 :: SET) :***: (f2 :: SET)) :: SET where
                     (:***:) :: ((,) a b1) :∈: f1 -> 
                               ((,) a b2) :∈: f2 -> 
                               (f1 :***: f2) (a,((,) b1 b2))
                         
infixr 3 :***:
        
                       
fstIsFun :: ((s1 :×: s2) :~>: s1) (Fst s1 s2)
fstIsFun = IsFun 
           (Subset (\(Fst p q) -> (p :×: q) :×: p))
           (\(p :×: q) -> ExSnd (Fst p q))
           (\(Fst _ _) (Fst _ _) k -> k)
           



     
sndIsFun :: ( (s1 :×: s2) :~>: s2) (Snd s1 s2)
sndIsFun = IsFun 
               (Subset (\(Snd p q) -> (p :×: q) :×: q))
               (\(p :×: q) -> ExSnd (Snd p q))
               (\(Snd _ _) (Snd _ _) k -> k)
               
               

               
targetTuplingIsFun :: (dom :~>: cod1) f1
                  -> (dom :~>: cod2) f2 
                  -> (dom :~>: (cod1 :×: cod2)) (f1 :***: f2)
targetTuplingIsFun f1 f2 = IsFun
                       (Subset (\(p1 :***: p2) -> inDom f1 p1
                                                 :×:
                                                 (inCod f1 p1 :×: inCod f2 p2)))

                       (\p -> case (total f1 p , total f2 p) of 
                               (ExSnd p1, ExSnd p2) -> ExSnd (p1 :***: p2))
                       
                       (\(p1 :***: p2)
                         (q1 :***: q2) k 
                             -> svalCPS f1 p1 q1 
                               (svalCPS f2 p2 q2 k))
                       

instance (
               Fact ((dom :~>: cod1) f1)
             , Fact ((dom :~>: cod2) f2)
         )
          => Fact (
                      (dom :~>: (cod1 :×: cod2)) 
                        (f1 :***: f2)
                     )
          
                      where
                        auto = targetTuplingIsFun auto auto
                               


fst_tupling :: 
               (dom :~>: cod1) f1 ->
               (dom :~>: cod2) f2 ->
               
               Fst cod1 cod2 :○: (f1 :***: f2) :==: f1
                   
fst_tupling f1 f2 = funEq (compoIsFun fstIsFun (targetTuplingIsFun f1 f2)) f1
                    (Subset (\(Compo (Fst _ _) (vf1 :***: _)) -> vf1))
                    
snd_tupling :: 
               (dom :~>: cod1) f1 ->
               (dom :~>: cod2) f2 ->
               
               Snd cod1 cod2 :○: (f1 :***: f2) :==: f2
                   
snd_tupling f1 f2 = funEq (compoIsFun sndIsFun (targetTuplingIsFun f1 f2)) f2
                    (Subset (\(Compo (Snd _ _) (_ :***: vf2)) -> vf2))
                    

tupling_eta :: 
               (dom :~>: (cod1 :×: cod2)) f ->

               ((Fst cod1 cod2 :○: f)
                        :***: 
                (Snd cod1 cod2 :○: f))

                :==: f
                                                       
tupling_eta f = funEq (targetTuplingIsFun (fstIsFun `compoIsFun` f) 
                                          (sndIsFun `compoIsFun` f)) f

                (Subset (\((Compo (Fst _ _) vf) :***: (Compo (Snd _ _) vf')) ->
                             case sval f vf vf' of
                               Refl -> vf))

-- * Particular functions
                       
-- | The type-level function:
--
-- /HaskFun(a,b) = (a -> b)/
data HaskFun :: SET where
               HaskFun :: HaskFun ((,) ((,) a b) (a -> b))
                         
instance (a_copy~a, b_copy~b) => Fact (((a_copy, b_copy), a -> b) :∈: HaskFun) where
    auto = HaskFun

haskFunIsFun :: ((Univ :×: Univ) :~>: FunctionType) HaskFun
haskFunIsFun = IsFun
               (Subset (\HaskFun -> ((Univ :×: Univ) :×: FunctionType)))
               (\(_ :×: _) -> ExSnd HaskFun)
               (\HaskFun HaskFun k -> k)

               
haskFunInjective :: Injective HaskFun
haskFunInjective = Injective (\HaskFun HaskFun k -> k)
                   

                   
-- | The type-level function:
--
-- /KleisliHom(a,b) = (a -> m b)/
data KleisliHom (m :: * -> *) :: SET where
               KleisliHom :: KleisliHom m ((,) ((,) a b) (a -> m b))

kleisliHomIsFun :: ((Univ :×: Univ) :~>: (KleisliType m)) (KleisliHom m)
kleisliHomIsFun = IsFun
               (Subset (\KleisliHom -> ((Univ :×: Univ) :×: KleisliType)))
               (\(_ :×: _) -> ExSnd KleisliHom)
               (\KleisliHom KleisliHom k -> k)
               
               
kleisliHomInjective :: Injective (KleisliHom m)
kleisliHomInjective = Injective (\KleisliHom KleisliHom k -> k)
                      
instance (a1~a, b1~b, m1~m) => Fact (((a1, b1), a -> m1 b) :∈: KleisliHom m) where
    auto = KleisliHom
           


-- * Conversions type constructors \<-\> type-level functions
                      
-- | Graph of a @SET@ type constructor
data Graph f :: SET where
               Graph :: Graph f (a, (f a))
                       
graphIsFun :: (Univ :~>: Univ) (Graph f)
graphIsFun = IsFun
             (Subset (\Graph -> Univ :×: Univ))
             (\_ -> ExSnd Graph)
             (\Graph Graph k -> k)
             
             
graphCPS :: pair :∈: Graph f ->
           (forall a. (pair ~ (a,f a)) => r) ->
               r
graphCPS Graph k = k 
           
             

-- | Type constructors are injective
graphInjective :: Injective (Graph f)
graphInjective = Injective (\Graph Graph k -> k)
                 

imageGraphList ::
                 [a] :∈: Image (Graph []) Univ
                     
                     
imageGraphList = Image Univ Graph

                 
instance (a~a_copy) => Fact ((a_copy, f a) :∈: Graph f) where
    auto = Graph



data ToTyCon (f::SET) x = forall y. ToTyCon ((x,y) :∈: f) y
                       
introToTyCon :: ((x, y) :∈: f) -> y -> ToTyCon f x
introToTyCon = ToTyCon            
               

-- | NB: this is stronger than the straightforward unpacking function -- we can use the single-valuedness
elimToTyCon :: (dom :~>: cod) f -> ToTyCon f x -> ((x,z) :∈: f) -> z
elimToTyCon f (ToTyCon fxy y) fxz = svalCoerce f fxy fxz y 
    
-- this is actually false; the two functions are just isomorphic
-- graph_TyCon :: Injective f -> (Univ :~>: cod) f -> Graph (TyCon f) :==: f

toTCG :: f x -> ToTyCon (Graph f) x
toTCG fx = ToTyCon Graph fx
                    
fromTCG :: ToTyCon (Graph f) x -> f x
fromTCG (ToTyCon Graph fx) = fx
                             

-- | Graph of a @(* -> * -> *)@ type constructor
data BiGraph f :: SET where
               BiGraph :: BiGraph f ((a,b) , (f a b))
                       
biGraphIsFun :: ((Univ :×: Univ) :~>: Univ) (BiGraph f)
biGraphIsFun = IsFun
             (Subset (\BiGraph -> (Univ :×: Univ) :×: Univ))
             (\(_ :×: _) -> ExSnd BiGraph)
             (\BiGraph BiGraph k -> k)
             

-- | Type constructors are injective
biGraphInjective :: Injective (BiGraph f)
biGraphInjective = Injective (\BiGraph BiGraph k -> k)
                   
instance (a~a_copy, b~b_copy) => Fact (((a_copy,b_copy), f a b) :∈: BiGraph f) where
    auto = BiGraph
                   

-- | Example of an extensional equation between functions
biGraph_eq_HaskFun :: BiGraph (->) :==: HaskFun
biGraph_eq_HaskFun = funEq biGraphIsFun haskFunIsFun
       (Subset (\BiGraph -> HaskFun))
       
-- * Constant functions

data Const dom x :: SET where
               Const :: a :∈: dom -> Const dom x (a,x)
                       
constIsFun :: x :∈: cod -> (dom :~>: cod) (Const dom x)
constIsFun x = IsFun 
               (Subset (\(Const a) -> a :×: x))
               (\a -> ExSnd (Const a))
               (\(Const a) (Const a') k -> k)
               

constEq :: Ex dom -> Const dom x :==: Const dom' x' -> x :=: x'
constEq (Ex a) eq = case eq `ecoerce` (Const a) of
                      Const _ -> Refl

       

-- * Dependent product

-- | NB: @fam@ must be a function mapping some set to a set of sets, or the second condition in the constructor is vacuous
data (Π (fam :: SET)) (f :: SET) where
                        Π ::
                          (base :~>: Unions fam) f
                          ->
                          (forall x y s. (x,y) :∈: f ->
                                    (x,Lower s) :∈: fam ->
                                  
                                    x :∈: s)
                          ->
                          Π fam f
                            

-- -- | We represent dependent products as spaces of sections.
-- --
-- -- Let /bundleMap : total -> base/ 
-- -- 
-- -- Then our @(Pi) bundleMap@, in more common notation, represents:
-- --
-- -- /(Pi) (x : base). { y : total | bundleMap y = x }/
-- --

-- * Sections

-- | Expresses that @f@ is a section of @bundleMap@
data (Section (bundleMap :: SET)) (f::SET) where
    Section ::
        (forall x y. (x,y) :∈: f -> (y,x) :∈: bundleMap)
            ->
        Section bundleMap f

-- | Lemma for proving a function equal to the identity
idLemma :: ((dom :~>: dom) f) -> 
            (forall x y. (x,y) :∈: f -> x :=: y) ->
            (Id dom :==: f)

idLemma f p = funEq idIsFun f
                 (Subset (\(Incl x) -> case total f x of
                                        ExSnd fxy -> case p fxy of
                                                      Refl -> fxy))

-- | Is section ==> composition is /id/
section_CompoId ::
    
    (total :~>: base) bun ->
    (base :~>: total) f ->
    ( Section bun f ) ->

       (bun :○: f :==: Id base) 
       
section_CompoId bun f (Section s) =
    setEqSym (idLemma (compoIsFun bun f)
             
              (\(Compo bun_yx f_xy) -> case sval bun bun_yx (s f_xy) of
                                        Refl -> Refl)
                                      
             )

-- | Composition is /id/ ==> is section
compoId_Section ::
    ( (total :~>: base) bun ) ->
    ( (base :~>: total) f ) ->
        (bun :○: f :==: Id base) 
       
    -> ( Section bun f )

       
compoId_Section bun f eq =
    Section (\f_xy -> case rel f f_xy of
                       (x :×: y) -> 
                           case total bun y of
                             ExSnd bun_yx' -> 
                                 case equal_f 
                                      idIsFun 
                                      eq 
                                      (Compo bun_yx' f_xy) 
                                      (Incl x) of

                                   Refl -> bun_yx')

      
-- * Inverses

data Inv (f :: SET) :: SET where
    Inv :: (a,b) :∈: f -> Inv f (b,a)
          
invInv0 :: Inv (Inv f) :⊆: f
invInv0 = Subset (\(Inv (Inv p)) -> p)
          

invInv :: (dom :~>: cod) f -> (Inv (Inv f)) :==: f
invInv f = SetEq invInv0
           (Subset (\fxy -> case rel f fxy of
                             _ :×: _ -> Inv (Inv fxy)))


-- | An injective function has an inverse, with domain the image
injective_Inv :: (dom :~>: cod) f -> Injective f -> 
                (Image f dom :~>: dom) (Inv f)
                                       
injective_Inv f (Injective inj) = 
    IsFun
    (Subset (\(Inv fxy) -> case rel f fxy of
                            x :×: _ -> Image x fxy :×: x)) 
    (\(Image _ fxy) -> ExSnd (Inv fxy))
    (\(Inv fxy) (Inv fx'y) k -> inj fxy fx'y k)
    
invId :: Inv (Id dom) :==: Id dom
invId = SetEq (Subset (\(Inv (Incl xx)) -> Incl xx))
              (Subset (\(Incl xx) -> (Inv (Incl xx))))


              

    
-- TODO: inverse of composition


$(lemmata ''Fact ['targetTuplingIsFun,'fstIsFun,'sndIsFun
                 ,'haskFunIsFun, 'haskFunInjective
                 ,'kleisliHomIsFun, 'kleisliHomInjective
                 ,'compoIsFun, 'idIsFun, 'inclusionIsFun 
                 ,'sval,'relation,'rel,'total 
                 , 'graphInjective, 'graphIsFun
                 , 'biGraphInjective, 'biGraphIsFun
                 , 'funEq
                 , 'extendCod
                 , 'equaliserSubset, 'equaliserUni, 'equaliserIsFun
                 , 'equal_f
                 ,'inDom,'inCod,'domUniq
                 ,'imageUnion
                 ,'compo_idl,'compo_idr
                 ,'lowerFun, 'raiseFun
                 ,'constIsFun, 'constEq
                             

                 ,'section_CompoId,'compoId_Section
                                  
                 ,'injective_Inv, 'inclusion_Injective, 'invId
                 ,'preimage_Image, 'image_Preimage
                 ,'compo_assoc


                  ,'fst_tupling, 'snd_tupling, 'tupling_eta
                     ])