-- This file:
--   http://angg.twu.net/AGDA/Variable1.agda.html
--   http://angg.twu.net/AGDA/Variable1.agda
--           (find-angg "AGDA/Variable1.agda")
--     See:  (find-angg "AGDA/Postulate1.agda")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
-- Version: 2021dec28
-- Public domain.
--
-- Long story short: if we want to build telescopes for tests the
-- right tool to use is "postulate", not "variable". See:
--   https://lists.chalmers.se/pipermail/agda/2021/012832.html my question
--   https://lists.chalmers.se/pipermail/agda/2021/012834.html Jesper's answer =)
--
-- ;; (find-angg "AGDA/find-agdatype.el")
-- (load       "~/AGDA/find-agdatype.el")


variable B₁ :                                              Set
variable B₂ : (y₁ : B₁) →                                  Set
variable A₁ : (y₁ : B₁) → (y₂ : B₂ y₁) →                   Set
variable A₂ : (y₁ : B₁) → (y₂ : B₂ y₁) → (x₁ : A₁ y₁ y₂) → Set
variable y₁ : B₁
variable y₂ : B₂ y₁
-- variable x₁ : A₁ y₁ y₂
-- variable x₂ : A₂ y₁ y₂ x₁
-- foo : ?
-- foo = B₁

-- (find-agdatype "B₁")
-- (find-agdatype "B₂")
-- (find-agdatype "A₁")

-- (find-agdatype "B₁")
-- (find-agdatype "B₂")
-- (find-agdatype "A₁")



-- Local Variables:
-- coding:  utf-8-unix
-- End: