{-# OPTIONS --cubical #-}

module jasontime where

open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence
open import Data.Product
open import Relation.Nullary
open import Function.LeftInverse hiding (id; _∘_)
open import Relation.Binary.PropositionalEquality hiding (_≡_)

-- Cribbed from https://stackoverflow.com/a/13441191
Surjective : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Set _
Surjective {A = A} {B = B} f = ∀ (y : B) → ∃ λ (x : A) → f x ≡ y

Injective : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Set _
Injective {A = A} {B = B} f = ∀ (x y : A) → f x ≡ f y → x ≡ y

-- contrapositive : {A B : Set} → (A → B) → (¬ B → ¬ A)
-- contrapositive f g = g ∘ f
-- 
-- Prove: f x ≡ f y → x ≡ y
-- Contra: x ≢ y → f x ≢ f y
-- contrapositive-statement : {S T : Set} → (f : S → T) → Surjective f → (x y : S) → x ≡ y → f x ≡ f y
-- 
-- wtf : {A : Set} {x y : A} → ¬ (x ≢ y) → x ≡ y
-- wtf s = ?

id : {A : Set} → A → A
id x = x

surjective-is-right-inverse : {S T : Set} → (f : S → T) → Surjective f → ∃ (λ g → f ∘ g ≡ id)
surjective-is-right-inverse f sj .fst t = Σ.fst (sj t)
surjective-is-right-inverse {S} {T} f sj .snd =
  let g = Σ.fst (surjective-is-right-inverse f sj) in
  ?
  -- funExt (λ s i → 
  --   let t = f s in
  --   let surjectivity = sj t in
  --   let sj-proof = Σ.snd surjectivity in
  --   let g∘f = g ∘ f in
  --   let Fuck! = transport {A = T} {B = T} ? ? in
  --   ?
  -- )
  -- funExt {A = S} {B = λ x i → ?} (λ x → ?) ? ?

left-inverse-is-injective : {S T : Set} → (g : T → S) → ∃ (λ f → f ∘ g ≡ id) → Injective g

jasontime-lemma : {S T : Set} → (f : S → T) → Surjective f → ∃ {A = T → S} (λ g → Injective g)
jasontime-lemma {S} {T} f sj .fst t = 
  let rinv = surjective-is-right-inverse f sj in
  let rinv-fn = Σ.fst rinv in
  rinv-fn t
jasontime-lemma f sj .snd x y p =
  ?
  where
    rinv = surjective-is-right-inverse f sj
    g = Σ.fst rinv

    TheLeftInverse : ∃ (λ f → f ∘ g ≡ id)
    TheLeftInverse .fst = ?
    TheLeftInverse .snd = ?

    Fuck! = left-inverse-is-injective ? TheLeftInverse
    rinv-prf = Σ.snd rinv
    left-inv = Σ.fst TheLeftInverse