-- open import Cat.Functor.Adjoint.Monadic
-- open import Cat.Functor.Adjoint.Monad
-- open import Cat.Functor.Equivalence
-- open import Cat.Diagram.Initial
-- open import Cat.Functor.Adjoint
-- open import Cat.Instances.Comma
-- open import Cat.Diagram.Monad hiding ( Free ; Forget ; Free⊣Forget )
-- open import Cat.Functor.Base
-- open import Cat.Univalent
-- open import Cat.Prelude

module wip.test3 where

-- Props : ∀ ℓ → Precategory (lsuc ℓ) ℓ
-- Props ℓ = c where
--   open Precategory
--   c : Precategory _ _
--   c .Ob = n-Type ℓ 1
--   c .Hom A B = ∣ A ∣ → B
--   c .Hom-set _ (_ , bp) = is-prop→is-set (Π-is-hlevel 1 λ _ → bp)
--   c .id = λ x → x
--   c ._∘_ f g = λ x → f (g x)
--   c .idr f = refl
--   c .idl f = refl
--   c .assoc f g h = refl

-- private variable ℓ : Level

-- open Functor

-- Forget : Functor (Props ℓ) (Sets ℓ)
-- Forget .F₀ (A , ap) = A , is-prop→is-set ap
-- Forget .F₁ = λ x → x
-- Forget .F-id = refl
-- Forget .F-∘ f g = refl

-- open Initial
-- open ↓Obj
-- open ↓Hom

-- Forget-has-univ : ∀ c → Universal-morphism c (Forget {ℓ})
-- Forget-has-univ (C , _) = um where
--   it : ↓Obj _ _
--   it .x = tt
--   it .y = ∥ C ∥ , squash
--   it .map = inc

--   um : Universal-morphism (C , _) _
--   um .bot = it
--   um .has⊥ arr = contr dh pull where
--     codomain : Prop _
--     codomain = arr .y

--     dh : ↓Hom _ _ _ _
--     dh .α = tt
--     dh .β = ∥-∥-elim (λ _ → arr .y .snd) (arr .map)
--     dh .sq i x = arr .map x

--     pull : ∀ x → dh ≡ x
--     pull x = ↓Hom-path _ _ refl (funext (λ _ → arr .y .snd _ _))

-- Free : Functor (Sets ℓ) (Props ℓ)
-- Free = universal-maps→L _ Forget-has-univ

-- Free⊣Forget : Free {ℓ} ⊣ Forget
-- Free⊣Forget = universal-maps→L⊣R _ Forget-has-univ

-- test : is-monadic (Free⊣Forget {ℓ})
-- test {ℓ} = ff+split-eso→is-equivalence ff seso where
--   ff : is-fully-faithful (Comparison Free⊣Forget)
--   ff = is-iso→is-equiv (iso alg rinv linv) where
--     alg : Algebra-hom _ _ _ → _ → _
--     alg = Algebra-hom.morphism

--     rinv : is-right-inverse alg (F₁ (Comparison Free⊣Forget))
--     rinv x = Algebra-hom-path refl

--     linv : is-left-inverse alg (F₁ (Comparison Free⊣Forget))
--     linv x = refl

--   seso : is-split-eso (Comparison Free⊣Forget)
--   seso ((T , tset) , alg) = (∥ T ∥ , squash) , c where
--     module alg = Algebra-on alg
--     import Cat.Reasoning (Eilenberg-Moore (L∘R (Free⊣Forget {ℓ}))) as R

--     abstract
--       T-prop : is-prop T
--       T-prop x y =
--           sym (happly alg.ν-unit _)
--         ·· ap alg.ν (squash (inc x) (inc y))
--         ·· happly alg.ν-unit _

--     f : Algebra-hom _ _ _
--     f .Algebra-hom.morphism = alg.ν
--     f .Algebra-hom.commutes = funext (λ _ → T-prop _ _)

--     g : Algebra-hom _ _ _
--     g .Algebra-hom.morphism = inc
--     g .Algebra-hom.commutes = funext (λ _ → squash _ _)

--     c : _ R.≅ _
--     c = R.make-iso f g (Algebra-hom-path (funext (λ _ → T-prop _ _)))
--                        (Algebra-hom-path (funext (λ _ → squash _ _)))

-- module
--   _ {o o₁ ℓ ℓ₁}
--     {A : Precategory o ℓ} {B : Precategory o₁ ℓ₁}
--     {F : Functor A B}
--   where

--   private module F = Functor F
--   import Cat.Reasoning A as A
--   import Cat.Reasoning B as B

--   faithful-reflects-monic
--     : ∀ {a b} {f : A.Hom a b}
--     → is-faithful F → B.is-monic (F.₁ f) → A.is-monic f
--   faithful-reflects-monic {f = f} faith mon g h p = faith (mon _ _ l) where
--     l =
--       F.₁ f B.∘ F.₁ g ≡˘⟨ F.F-∘ _ _ ⟩
--       F.₁ (f A.∘ g)   ≡⟨ ap F.₁ p ⟩
--       F.₁ (f A.∘ h)   ≡⟨ F.F-∘ _ _ ⟩
--       F.₁ f B.∘ F.₁ h ∎

--   faithful-reflects-epic
--     : ∀ {a b} {f : A.Hom a b}
--     → is-faithful F → B.is-epic (F.₁ f) → A.is-epic f
--   faithful-reflects-epic {f = f} faith epi g h p = faith (epi _ _ l) where
--     l =
--       F.₁ g B.∘ F.₁ f ≡˘⟨ F.F-∘ _ _ ⟩
--       F.₁ (g A.∘ f)   ≡⟨ ap F.₁ p ⟩
--       F.₁ (h A.∘ f)   ≡⟨ F.F-∘ _ _ ⟩
--       F.₁ h B.∘ F.₁ f ∎