如何在Agda中证明类型𝟚的等价关系要么是id要么是置换？

你的核心问题在于两点：一是没有利用等价关系的单射性排除不可能的函数行为（即两个元素映射到同一值的情况）；二是在with分支中没有正确绑定模式匹配带来的等式上下文，同时函数扩展性（funext）的调用方式有误。

前置定义补充 #

首先需要明确基础类型与等价关系的标准定义（如果你的代码中已有，可跳过）：

open import Data.Unit using (⊤; tt)
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_])
open import Data.Empty using (⊥; ⊥-elim)
open import Relation.Binary.PropositionalEquality
open import Function using (_∘_; id)
open import Axiom.Extensionality.Propositional using (Extensionality)

-- 双元素类型定义（你用的⊤⊎⊤版本）
𝟚-type : Set
𝟚-type = ⊤ ⊎ ⊤

-- 置换函数
permut-𝟚 : 𝟚-type → 𝟚-type
permut-𝟚 (inj₁ tt) = inj₂ tt
permut-𝟚 (inj₂ tt) = inj₁ tt

-- 等价关系记录类型
record _≃_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
    to-from : ∀ b → to (from b) ≡ b
    from-to : ∀ a → from (to a) ≡ a
open _≃_ public

-- 函数扩展性公理（需要显式声明）
postulate ext : ∀ {ℓ ℓ'} → Extensionality ℓ ℓ'

关键引理：等价关系的to函数是单射 #

因为等价关系是双射，所以to函数必然是单射——若to f x ≡ to f y，则x ≡ y。我们先证明这个引理：

to-injective : ∀ {f : 𝟚-type ≃ 𝟚-type} {x y : 𝟚-type} → to f x ≡ to f y → x ≡ y
to-injective {f} {x} {y} eq =
  begin
    x
      ≡⟨ sym (from-to f x) ⟩
    from f (to f x)
      ≡⟨ cong (from f) eq ⟩
    from f (to f y)
      ≡⟨ from-to f y ⟩
    y
  end
  where open ≡-Reasoning

主定理证明 #

利用with拆分to f在两个元素上的取值，结合单射性排除无效分支，最后用函数扩展性证明函数相等：

𝟚-equivalences-characterization : ∀ (f : 𝟚-type ≃ 𝟚-type) → to f ≡ id ⊎ to f ≡ permut-𝟚
𝟚-equivalences-characterization f with to f (inj₁ tt) | to f (inj₂ tt)
-- 情况1：函数是恒等映射
... | inj₁ tt | inj₂ tt = inj₁ (ext λ {
    (inj₁ tt) → refl;
    (inj₂ tt) → refl
  })
-- 情况2：函数是双元素置换
... | inj₂ tt | inj₁ tt = inj₂ (ext λ {
    (inj₁ tt) → refl;
    (inj₂ tt) → refl
  })
-- 情况3：两个元素映射到同一值，违反单射性，导出矛盾
... | inj₁ tt | inj₁ tt = ⊥-elim (to-injective {f} {inj₁ tt} {inj₂ tt} refl)
... | inj₂ tt | inj₂ tt = ⊥-elim (to-injective {f} {inj₁ tt} {inj₂ tt} refl)

解释 #

1. with分支的模式匹配：当你匹配到to f (inj₁ tt) ≡ inj₁ tt时，这个等式已经被纳入当前上下文，因此refl可以直接作为to f (inj₁ tt) ≡ id (inj₁ tt)的证明。
2. 函数扩展性：ext接受一个证明∀ x → to f x ≡ g x的函数，直接返回to f ≡ g，这是标准的函数扩展性使用方式。
3. 排除无效分支：利用to-injective，如果两个元素被映射到同一值，会导出inj₁ tt ≡ inj₂ tt的矛盾，用⊥-elim消除这些不可能的情况。

内容的提问来源于stack exchange，提问作者Werner Germán Busch