open import 1Lab.Reflection.Subst
open import 1Lab.Reflection

open import Cat.Instances.Shape.Terminal
open import Cat.Functor.Naturality
open import Cat.Reasoning
open import Cat.Prelude

module Cat.Functor.Naturality.Reflection where

module _ {o ℓ o' ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'} where

  -- Tactic worker for filling in trivial natural isomorphisms F ≅ⁿ G.
  --
  -- The assumptions are:
  -- 1. ∀ x, F .F₀ x is definitionally equal to G .F₀ x
  -- 2. ∀ f, F .F₁ f is extensionally equal (by `trivial!`) to G .F₁ f
  --    OR C = ⊤Cat
  --
  -- The functor arguments are only used for type inference.
  trivial-isoⁿ : (F G : Functor C D) → Term → TC ⊤
  trivial-isoⁿ _ _ hole = do
    `C ← quoteTC C
    `D ← quoteTC D
    wait-just-a-bit `C >>= unify hole ⊙ λ where
      (def₀ (quote ⊤Cat)) → def₀ (quote !const-isoⁿ)
        ##ₙ (def₀ (quote id-iso) ##ₙ `D)
      _ → def₀ (quote iso→isoⁿ)
        ##ₙ vlam "" (def₀ (quote id-iso) ##ₙ raise 1 `D)
        ##ₙ vlam ""
          (def₀ (quote _··_··_)
            ##ₙ (def₀ (quote idr) ##ₙ raise 1 `D ##ₙ unknown)
            ##ₙ def₀ (quote trivial!)
            ##ₙ (def₀ (quote sym)
              ##ₙ (def₀ (quote idl) ##ₙ raise 1 `D ##ₙ unknown)))

  trivial-isoⁿ!
    : ∀ {F G : Functor C D}
    → {@(tactic trivial-isoⁿ F G) is : F ≅ⁿ G}
    → F ≅ⁿ G
  trivial-isoⁿ! {is = is} = is

-- Tests

module _ {o ℓ} {C : Precategory o ℓ} where

  _ : ∀ {F : Functor C C} → F ≅ⁿ F
  _ = trivial-isoⁿ!

  _ : ∀ {K : Functor ⊤Cat C} → !Const (K .Functor.F₀ _) ≅ⁿ K
  _ = trivial-isoⁿ!