module Prelude
  (C : Set1)
  (HomC : C -> C -> Set)
  (idC : (c : C) -> HomC c c)
  (_∘C_ : {a b c : C} -> HomC b c -> HomC a b -> HomC a c)
  where

-- This file contains some basic definitions missing (or well-hidden)
-- in the standard library, and then defines the category Fam C,
-- parameterised by the category C, together with its coproducts.


open import Data.Product
open import Data.Bool
open import Function

-- Dependent elimination for Bool

Bool-elim : ∀ {a} (P : Bool -> Set a) -> P true -> P false -> (x : Bool) -> P x
Bool-elim P Pt Pf true = Pt
Bool-elim P Pt Pf false = Pf


-- Fam C and Fam C morphisms, plus coproduct stuff for Fam C -----

record FamC : Set1 where
  constructor _,_
  field
    index : Set
    fam : index -> C
open FamC public

record HomFamC  (A B : FamC) : Set1 where
  constructor _,_
  field
    indfun : index A -> index B
    famfun : (x : index A) -> HomC (fam A x) (fam B (indfun x))
open HomFamC

idFamC : {A : FamC} -> HomFamC A A
idFamC {A} = id , (λ x → idC (fam A x))

_∘FamC_ : ∀ {a b c} -> HomFamC b c -> HomFamC a b -> HomFamC a c
(h , k) ∘FamC (h' , k') = (h ∘ h') , (λ x → k (h' x) ∘C k' x)

-- Fam C has coproducts

ΣFamC : (A : Set) -> (A -> FamC) -> FamC
ΣFamC A B = (Σ A (index ∘ B)) , (λ { (a , b) → fam (B a) b })


inA : ∀ {A B} -> (a : A) -> HomFamC (B a) (ΣFamC A B)
inA a = (λ b → (a , b)) , (λ b → idC _)

outΣ : ∀ A {B C} -> ((a : A) -> HomFamC (B a) C) -> HomFamC (ΣFamC A B) C
outΣ A p = (λ { (a , b) → indfun (p a) b }) , (λ { (a , b) → famfun (p a) b })

syntax outΣ A (λ a → p) = [ p ][ a ∈ A ]

ΣFamCmor : {I J : Set} → {X : I -> FamC}{Y : J -> FamC} ->
          (f : I -> J) ->
          (g : (i : I) -> HomFamC (X i) (Y (f i))) ->
          HomFamC (ΣFamC I X) (ΣFamC J Y)
ΣFamCmor {I} f g = [ inA (f i) ∘FamC (g i) ][ i ∈ I ]