{-# OPTIONS --without-K #-}
open import Agda.Primitive
open import 1-equality
open import 2-composition
open import 3-ap
open import 4-homotopy
open import 5-qip
open import 6-equivalence

data Bool : Set where
  true  : Bool
  false : Bool

isContr :
  { : Level} 
  (X : Set ) 
  Set 

isContr X = Σ X λ x  Π X λ y  x  y

isProp :
  { : Level} 
  (X : Set ) 
  Set 

isProp X = (x y : X)  isContr (x  y)

isSet :
  { : Level} 
  (X : Set ) 
  Set 

isSet X = (x y : X)  isProp (x  y)

-- monic and injective

is·monic :
  {ℓ₁ ℓ₂ : Level} 
  {A : Set ℓ₁}    
  {B : Set ℓ₂}    
  (f : A  B)     
  Set (ℓ₁  ℓ₂)

is·monic {A = A} {B = B} f =
  (g h : B  A)   
  (f  g  f  h) 
  g  h

monic·theorem :
  {ℓ₁ ℓ₂ ℓ₃ : Level}  
  {A : Set ℓ₁}        
  {B : Set ℓ₂}        
  {C : Set ℓ₃}        
  (f : A  B)         
  (is·monic f)        
  (g h : C  A)       
  ((f  g)  (f  h)) 
  g  h

monic·theorem f imf g h fg∼fh = -- auto-deduced!
    λ c  imf  _  g c)
               _  h c)
               _  fg∼fh c)
              ((f  h) c)

is·injective :
  {ℓ₁ ℓ₂ : Level} 
  {A : Set ℓ₁} 
  {B : Set ℓ₂} 
  (f : A  B) 
  Set (ℓ₁  ℓ₂)

is·injective {A = A} {B = B} f =
  (x y : A) 
  f x  f y 
  (x  y)

-- is·injective f ≃ is·monic f ?
-- I have everything but the last homotopy.

is·injective·to·is·monic :
  {ℓ₁ ℓ₂ : Level} 
  {A : Set ℓ₁} 
  {B : Set ℓ₂} 
  (f : A  B) 
  is·injective f  is·monic f

is·injective·to·is·monic f iif =
  λ g h f∘g∼f∘h z  iif (g z) (h z) (f∘g∼f∘h z)

is·monic·to·is·injective :
  {ℓ₁ ℓ₂ : Level} 
  {A : Set ℓ₁} 
  {B : Set ℓ₂} 
  (f : A  B) 
  is·monic f  is·injective f

is·monic·to·is·injective f imf =
  λ x y fx≡fy 
    imf  _  x)  _  y)  _  fx≡fy) (f x) -- (or f y)

monic·injective·homotopy·1 :
  {ℓ₁ ℓ₂ : Level} 
  {A : Set ℓ₁} 
  {B : Set ℓ₂} 
  (f : A  B) 
  is·monic·to·is·injective f  is·injective·to·is·monic f  id

monic·injective·homotopy·1 f = λ _  refl

-- monic·injective·homotopy·2 :
--   {ℓ₁ ℓ₂ : Level} →
--   {A : Set ℓ₁} →
--   {B : Set ℓ₂} →
--   (f : A → B) →
--   is·injective·to·is·monic f ∘ is·monic·to·is·injective f ∼ id
--
-- monic·injective·homotopy·2 f = {!   !}

-- epic and surjective

is·epic :
  {ℓ₁ ℓ₂ : Level} 
  {A : Set ℓ₁}    
  {B : Set ℓ₂}    
  (f : A  B)     
  Set (ℓ₁  ℓ₂)

is·epic {A = A} {B = B} f =
  (g h : B  A) 
  (g  f  h  f) 
  g  h

is·surjective :
  {ℓ₁ ℓ₂ : Level} 
  {A : Set ℓ₁}    
  {B : Set ℓ₂}    
  (f : A  B)     
  Set (ℓ₁  ℓ₂)

is·surjective {A = A} {B = B} f =
  (b : B)  Σ A λ a  f a  b

surjective·theorem :
  {ℓ₁ ℓ₂ ℓ₃ : Level}  
  {A : Set ℓ₁}        
  {B : Set ℓ₂}        
  {C : Set ℓ₃}        
  (f : A  B)         
  (is·surjective f)   
  (g h : B  C)       
  (g  f  h  f)     
  g  h

surjective·theorem f isf g h gf∼hf b =
  gb≡gfa  gfa≡hfa  hfa≡hb
  where
  a       = Σ.fst (isf b)
  fa≡b    = Σ.snd (isf b)
  gb≡gfa  = sym (ap g fa≡b)
  gfa≡hfa = gf∼hf a
  hfa≡hb  = ap h fa≡b



is·surjective·to·is·epic :
  {ℓ₁ ℓ₂ : Level} 
  {A : Set ℓ₁} 
  {B : Set ℓ₂} 
  (f : A  B) 
  is·surjective f  is·epic f

is·surjective·to·is·epic = surjective·theorem

-- is·epic·to·is·surjective :
--   {ℓ₁ ℓ₂ : Level} →
--   {A : Set ℓ₁} →
--   {B : Set ℓ₂} →
--   (f : A → B) →
--   is·epic f → is·surjective f

-- is·epic·to·is·surjective f = {!   !}
-- -- undoable? i seem unable to formalize the following:
-- -- https://mathoverflow.net/questions/178778/in-the-category-of-sets-epimorphisms-are-surjective-constructive-proof
--
-- epic·theorem :
--   {ℓ₁ ℓ₂ ℓ₃ : Level}  →
--   {A : Set ℓ₁}        →
--   {B : Set ℓ₂}        →
--   {C : Set ℓ₃}        →
--   (f : A → B)         →
--   (is·epic f)         →
--   (g h : B → C)       →
--   (g ∘ f ∼ h ∘ f) →
--   g ∼ h
--
-- epic·theorem = {!   !}


-- is·epic+·to·surjective {A = A} {B = B} h ief b =
--   {!   !}
--   where
--   f : B → Set _
--   f b' = Σ A (λ a → h a ≡ b)
--   g : B → Set _
--   g b' = Σ A (λ a → (h a ≡ b) × (b' ≡ b))
--   f∘h∼g∘h : f ∘ h ∼ g ∘ h
--   f∘h∼g∘h = λ a → {!   !}
--   f∼g : f ∼ g
--   f∼g = ief f g f∘h∼g∘h

-- Andrej Bauer gives the following.
--    im h = {b ∈ B | ∃ a ∈ A . h a ≡ b }
--    f g : B → 2ᴮ
--    f b = {b} ∩ im h
--    g b = {b}
--    ∀ (a ∈ A) . f (h a) ≡ {h a}
--    ∀ (a ∈ A) . g (h a) ≡ {h a}
--    f∼g
--    ∀ y ∈ B . f y ≡ g y
--    ∀ y ∈ B . {y} ∩ im(h) ≡ {y}
--    ∀ y ∈ B . y ∈ im(h)
-- The last line is surjectivity.
-- There are a number of things here I do not
-- know how to formalize constructively.
--    -- im h = {b ∈ B | ∃ a ∈ A . h a ≡ b }
--    im h = Σ B λ b → Σ A λ a → h a ≡ b
--    -- f g : B → 2ᴮ
--    f g : B → Σ B (Set _)
--    -- f b = {b} ∩ im h
--    -- g b = {b}
--    f b' = Σ B λ b → (b' ≡ b) × (Σ A λ a → h a ≡ b)
--    g b' = Σ B λ b → (b' ≡ b)
--    -- ∀ (a ∈ A) . f (h a) ≡ {h a}
--    (a : A) → f (h a) ≡ Σ B λ b → (h a ≡ b)
--    -- ∀ (a ∈ A) . g (h a) ≡ {h a}
--    (a : A) → g (h a) ≡ Σ B λ b → (h a ≡ b)
--    f ∼ g
--    -- ∀ y ∈ B . f y ≡ g y
--    (b : B) → f b ≡ g b
--    (b' : B) → (Σ B λ b → (b' ≡ b × Σ A λ a → h a ≡ b)) ≡
--               (Σ B λ b → (b' ≡ b))
--    ... can I get this far?
--    ∀ y ∈ B . {y} ∩ im(h) ≡ {y}
--    ∀ y ∈ B . y ∈ im(h)
-- is·surjective {A = A} {B = B} f =
--   (b : B) → Σ A λ a → f a ≡ b

-- full strength epi
is·epic+ :
  {ℓ₁ ℓ₂ : Level}     
  {A : Set ℓ₁}        
  {B : Set ℓ₂}        
  (f : A  B)         
  Set (lsuc (ℓ₁  ℓ₂))

is·epic+ {ℓ₁ = ℓ₁} {ℓ₂ = ℓ₂} {A = A} {B = B} f =
  (C : Set (ℓ₁  ℓ₂))      
  (g h : B  C)            
  (g  f  h  f)          
  g  h

-- is·epic+·to·surjective :
--   {ℓ₁ ℓ₂ : Level}  →
--   {A : Set ℓ₁}     →
--   {B : Set ℓ₂}     →
--   (f : A → B)      →
--   (is·epic+ f)     →
--   is·surjective f
--
-- is·epic+·to·surjective {A = A} {B = B} h ief b =
--   {!   !}
--   where
--   im = Σ B λ b → Σ A λ a → h a ≡ b
--   f : B → Σ B (Set _)
--   f b' = Σ B λ b → (b' ≡ b) × (Σ A λ a → h a ≡ b)
--   g : B → Σ B (B → Set _)
--   g b' = Σ B λ b → (b' ≡ b)
--   -- ∀ (a ∈ A) . f (h a) ≡ {h a}
--   [1] = (a : A) → f (h a) ≡ Σ B λ b → (h a ≡ b)
--   -- ∀ (a ∈ A) . g (h a) ≡ {h a}
--   [2] = (a : A) → g (h a) ≡ Σ B λ b → (h a ≡ b)
--   [3] = f ∼ g
--   [4] = (b' : B) → (Σ B λ b → (b' ≡ b × Σ A λ a → h a ≡ b)) ≡ (Σ B λ b → (b' ≡ b))
--   -- ... can I get this far?
--   -- ∀ y ∈ B . {y} ∩ im(h) ≡ {y}
--   -- ∀ y ∈ B . y ∈ im(h)
--   -- is·surjective {A = A} {B = B} f =
--   -- (b : B) → Σ A λ a → f a ≡ b

--- part 2

epi·monic·1 :
  {ℓ₁ ℓ₂ ℓ₃ : Level}       
  {A : Set ℓ₁}             
  {B : Set ℓ₂}             
  {C : Set ℓ₃}             
  (f : B  A)              
  (g : A  B)              
  (u v : C  A)            
  (f  g  id)             
  (g  u  g  v)          
  u  v

epi·monic·1 {A = A} {B = B} {C = C} f g u v fg∼id gu∼gv =
  λ x  g·monic (u x) (v x) (gu∼gv x)
  where
  g·monic : (a₁ a₂ : A)  g a₁  g a₂  a₁  a₂
  g·monic a₁ a₂ ga₁≡ga₂ =
    (sym (fg∼id a₁))  (ap f ga₁≡ga₂)  (fg∼id a₂)

epi·monic·2 :
  {ℓ₁ ℓ₂ ℓ₃ : Level}       
  {A : Set ℓ₁}             
  {B : Set ℓ₂}             
  {C : Set ℓ₃}             
  (f : B  A)              
  (g : A  B)              
  (u v : A  C)            
  (f  g  id)             
  (u  f  v  f)          
  u  v

epi·monic·2 {A = A} {B = B} {C = C} f g u v fg∼id uf∼vf a =
  (ap u (sym fb≡a))  (uf∼vf b)  (ap v fb≡a)
  where
  f·epi : (a : A)  Σ B  b  f b  a)
  f·epi a = [ g a , fg∼id a ]
  b = Σ.fst (f·epi a)
  fb≡a = Σ.snd (f·epi a)