-- This file:
--   http://angg.twu.net/AGDA/ha.agda.html
--   http://angg.twu.net/AGDA/ha.agda
--           (find-angg "AGDA/ha.agda")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>

-- (find-es "agda" "heyting-algebra")
-- (find-es "agda" "module-system")

-- (find-agdaprimfile "Agda/Builtin/Equality.agda")
-- (find-agdaprimfile "Agda/Builtin/Strict.agda")
-- (find-agdaprimfile "Agda/Builtin/Unit.agda")
-- (find-agdaprimfile "Agda/Builtin/Sigma.agda")
-- (find-agdaprimfile "Agda/Builtin/Bool.agda")
-- (find-agdastdlibsrcfile "Level.agda")
-- (find-agdastdlibsrcfile "Strict.agda")
-- (find-agdastdlibsrcfile "Function/Base.agda")
-- (find-agdastdlibsrcfile "Data/Empty.agda")
-- (find-agdastdlibsrcfile "Data/Empty/Irrelevant.agda")
-- (find-agdastdlibsrcfile "Relation/Nullary.agda")
-- (find-agdastdlibsrcfile "Data/Unit/Base.agda")
-- (find-agdastdlibsrcfile "Data/Bool/Base.agda")
-- (find-agdastdlibsrcfile "Relation/Nullary/Reflects.agda")
-- (find-agdastdlibsrcfile "Data/Sum/Base.agda")
-- (find-agdastdlibsrcfile "Algebra/Core.agda")
-- (find-agdastdlibsrcfile "Data/Product.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Core.agda")
-- (find-agdastdlibsrcfile "Algebra/Definitions.agda")
-- (find-agdastdlibsrcfile "Data/These/Base.agda")
-- (find-agdastdlibsrcfile "Data/Maybe/Base.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Definitions.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/PropositionalEquality/Core.agda")
-- (find-agdastdlibsrcfile "Relation/Nullary/Decidable/Core.agda")
-- (find-agdastdlibsrcfile "Relation/Unary.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Consequences.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Structures.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Bundles.agda")
-- (find-agdastdlibsrcfile "Relation/Binary.agda")
-- (find-agdastdlibsrcfile "Function/Definitions/Core1.agda")
-- (find-agdastdlibsrcfile "Function/Definitions/Core2.agda")
-- (find-agdastdlibsrcfile "Function/Definitions.agda")
-- (find-agdastdlibsrcfile "Function/Structures.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Indexed/Heterogeneous/Core.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Indexed/Heterogeneous/Definitions.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Indexed/Heterogeneous/Structures.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Indexed/Heterogeneous/Bundles.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Indexed/Heterogeneous.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Reasoning/Base/Single.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Reasoning/Setoid.agda")
-- (find-agdastdlibsrcfile "Algebra/Consequences/Base.agda")
-- (find-agdastdlibsrcfile "Algebra/Consequences/Setoid.agda")
-- (find-agdastdlibsrcfile "Algebra/Structures.agda")
-- (find-agdastdlibsrcfile "Algebra/Bundles.agda")
-- (find-agdastdlibsrcfile "Algebra.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/PropositionalEquality/Properties.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/PropositionalEquality/Algebra.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Indexed/Heterogeneous/Construct/Trivial.agda")
-- (find-agdastdlibsrcfile "Function/Equality.agda")
-- (find-agdastdlibsrcfile "Axiom/UniquenessOfIdentityProofs.agda")
-- (find-agdastdlibsrcfile "Axiom/Extensionality/Propositional.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/PropositionalEquality.agda")
-- (find-agdastdlibsrcfile "Function/Bundles.agda")
-- (find-agdastdlibsrcfile "Function/Core.agda")
-- (find-agdastdlibsrcfile "Function.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Properties/Preorder.agda")
-- (find-agdastdlibsrcfile "Relation/Nullary/Product.agda")
-- (find-agdastdlibsrcfile "Function/Equivalence.agda")
-- (find-agdastdlibsrcfile "Function/Injection.agda")
-- (find-agdastdlibsrcfile "Relation/Nullary/Decidable.agda")
-- (find-agdastdlibsrcfile "Data/Unit/Properties.agda")
-- (find-agdastdlibsrcfile "Data/Unit.agda")
-- (find-agdastdlibsrcfile "Category/Functor.agda")
-- (find-agdastdlibsrcfile "Category/Applicative/Indexed.agda")
-- (find-agdastdlibsrcfile "Category/Monad/Indexed.agda")
-- (find-agdastdlibsrcfile "Category/Monad.agda")
-- (find-agdastdlibsrcfile "Relation/Nullary/Negation/Core.agda")
-- (find-agdastdlibsrcfile "Relation/Nullary/Negation.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Construct/NonStrictToStrict.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Properties/Poset.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Lattice.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Properties/BoundedJoinSemilattice.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Properties/BoundedMeetSemilattice.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Reasoning/Base/Triple.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Reasoning/PartialOrder.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Properties/JoinSemilattice.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Properties/MeetSemilattice.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Properties/Lattice.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Properties/BoundedLattice.agda")
-- (find-agdastdlibsrcfile "Relation/Binary/Properties/HeytingAlgebra.agda")

-- (eek "M-h M-k  C-c C-o  ;; agda2-module-contents-maybe-toplevel")
-- (find-efunctiondescr 'agda2-module-contents-maybe-toplevel)
-- (find-efunction      'agda2-module-contents-maybe-toplevel)
-- (find-efunctionpp    'agda2-module-contents-maybe-toplevel)
-- (find-efunctiond     'agda2-module-contents-maybe-toplevel)
-- (find-efunctiondescr 'agda2-module-contents)
-- (find-efunction      'agda2-module-contents)
-- (find-efunctionpp    'agda2-module-contents)
-- (agda2-module-contents nil "HA")

-- (agda2-module-contents "HA")

-- module Ha where

open import Function.Base
open import Level

import Relation.Binary.Properties.HeytingAlgebra as HA
-- import Relation.Binary.Lattice.HeytingAlgebra as HA

variable
  c �� �� : Level
  -- L : HA c �� ��


-- variable
--   a b c � �� �� �� : Level
--   A : Set a
--   B : Set b
--   C : Set c
--   D : Set
--   E : Set (suc zero)

-- PQ�Q�R : B� B� B�




{-
-- (find-es "agda" "agda-user-manual")
-- (find-efunctiondescr 'agda2-mode)

* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
export LC_ALL=en_GB.UTF-8
agda -v 2 ha.agda  | tee /tmp/o

# (find-es "agda" "loading-process")

stack exec --       agda --compile ha.agda
./ha
                    agda --compile ha.agda
agda --ghc-dont-call-ghc --compile ha.agda

agda  --help
stack --help
# agda -i. -i/usr/share/agda-stdlib --interactive ha.agda
# :load ha.agda
# :?

-}