fact: Definition rel `{Repr a} `{Repr b} (lam : a → b) (ccc : repr a ~{AST}~> repr b) : Type := ∀ x : a, convert (lam x) ≈ ccc ∘ convert x.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Structure.Terminal Category.Structure.Cartesian Category.Structure.Cartesian.Closed Category.Functor.Structure.Cartesian Category.Instance.Coq Category.Instance.AST Category.Tools.Represented