在Agda中，公理通常指一个已知的事实或原则。其中一个基本公理是底部（bottom）公理，它允许我们定义一些函数，即使在某些输入上它们不可定义也可以。具体来说，底部公理表示可以定义一个类型为“任何类型”的函数，它永远不会终止或产生正确的结果。例如，在Agda中，以下函数的类型为“Nat → Bool”，但对于输入为“0”的情况它会陷入无限循环：

loop : Nat → Bool
loop zero = loop zero
loop (suc x) = false

为了避免程序陷入无限循环，我们可以使用底部（bottom）公理定义一个函数，该函数在不可定义的输入上从不终止。例如：

impossible : ∀ {A : Set} → A
impossible = loop zero

在这个函数中，我们不需要定义任何情况，因为它永远不会被调用。当我们需要在一个函数中排除某些输入时，我们可以使用这个函数来表示那些不可能的输入。例如，以下函数定义了自然数加法：

_+_ : Nat → Nat → Nat
zero + n = n
suc m + n = suc (m + n)

如果我们希望排除“两个输入都为0”的情况，我们可以这样定义：

_+_ : Nat → Nat → Nat
zero + n = n
m + zero = m
suc m + n = suc (m + n)
zero +̸ zero = impossible

在这种情况下，我们使用底部公理作为哪些输入是不可能的表示。在这种情况下，我们定义了一个不会终止的函数，但它只在一个不可能的情况下被调用，因此不会影响程序的可维护性或可靠性。