Skip to content

Latest commit

 

History

History
13 lines (10 loc) · 391 Bytes

exercises-lecture2-1.md

File metadata and controls

13 lines (10 loc) · 391 Bytes

Give terms denoting proofs of

  • (A -> B -> C) -> (B -> A -> C)
  • (Πa:A.Πb:B.C(a,b)) -> (Πb:B.Πa:A.C(a,b))
  • (A -> B) -> (B -> C) -> (A -> C)
  • A ∧ (B ∧ C) -> B ∧ (A ∧ C)
  • (A ∧ B) ∧ C -> (B ∧ A) ∧ C
  • A ∧ (B ∧ C) -> (A ∧ B) ∧ C
  • Σa:A.Σb:B.C(a,b) -> Σb:B.Σa:A.C(a,b)
  • Σc:A×B.C(c) -> Σc:B×A.C(⟨c.2,c.1⟩)
  • Σb:A.Σa:B.C(a,b) -> Σc:A×B.C(c.1,c.2)