How would one formulate a dependently-typed logic in Agda, but not "cheating" by re-using the Agda type system itself?
I can quite readily define an independently-typed logic:
infixr 5 _⇒_
data Type : Set where
_⇒_ : Type → Type → Type
infix 4 _⊢_
data _⊢_ : List Type → Type → Set where
var : {a : Type} → [ a ] ⊢ a
λ' : {a b : Type} {γ : _} → a ∷ γ ⊢ b → γ ⊢ a ⇒ b
ply : {a b : Type} {γ δ : _} → γ ⊢ a ⇒ b → δ ⊢ a → γ ++ δ ⊢ b
weak : {a b : Type} {γ : _} → γ ⊢ b → a ∷ γ ⊢ b
cntr : {a b : Type} {γ : _} → a ∷ a ∷ γ ⊢ b → a ∷ γ ⊢ b
xchg : {a : Type} {γ δ : _} → γ ↭ δ → γ ⊢ a → δ ⊢ a
I can also roughly follow the LambdaPi tutorial implementation of dependently-typed λ-calculus in Haskell. But it's implictly-typed, unlike my Agda code, and i'm not sure where to even begin to modify my code, as the path which came to mind so far led to infinite regress:
data _⊢_ : List (? ⊢ ?) → (? ⊢ ?) → Set where ...
Google searches for "embedding dependent types in Agda" and the like merely return hits for dependently-typed programming in Agda...
We have done this in our paper on Type Theory in Type Theory which is actually formalised in Agda. The basic idea is that you define Contexts, Types, Terms and Substitutions as a mutual inductive definition. We only define typed objects so we never have to define untyped things or a typing judgement. Typing is defined via dependency so for example types depend on contexts and terms on types and contexts. To formulate definitional equality we use ideas from Homotopy Type Theory and allow equality constructors. This meant that we had to axiomatise instances of higher inductive types or to be precise quotient inductive inductive types. This should be soon possible out of the box in cubical Agda.
http://www.cs.nott.ac.uk/~psztxa/publ/tt-in-tt.pdf
@article{altenkirch2016type,
title={Type theory in type theory using quotient inductive types},
author={Altenkirch, Thorsten and Kaposi, Ambrus},
journal={ACM SIGPLAN Notices},
volume={51},
number={1},
pages={18--29},
year={2016},
publisher={ACM}
}