Codewars라고 대충 코테 사이트 인데 지원 언어에 Agda가 있길래 좀 풀어봄

근데 증명 문제들은 대체로 개념적으로 어려운게 많고 증명 난이도가 높은건 없더라

Agda만 풀어봐서 PS문제 같은것도 이런지는 잘 모르겠음


https://www.codewars.com/kata/search/agda?q=&r[]=-1&beta=false

여기 있는 것들


재밌는게 1kyu에 cubical agda 쓰는 문제가 3개나 됨.

cubical agda는 agda에서 cubical type theory, HoTT를 구현해 놓은거임


1. Two paths in the forest

Bool 타입은 true와 false 두개의 원소를 가지기 때문에

isomorphism Bool -> Bool은 id, not 두개가 있음. (id ∘ id = not ∘ not = id)

한편 HoTT 에서는 "isomorphic하면 equal하다"는 말도 안되게 좋은 성질이 성립하기 때문에

위의 두 isomorphism으로부터 두개의 equality가 만들어짐.

결국 Bool = Bool 이라는 타입은 두개의 원소를 가져 (id로 같을 수 있고, not으로 같을 수 있으니까)

그럼 다시 Bool 과 Bool = Bool 사이의 isomorphism을 만들 수 있음.

isomorphic하면 equal하기 때문에 Bool = (Bool = Bool) 이라는 이상한 결과를 얻을 수 있다.

isomorphism을 만드는건 어렵지 않고, isomorphism이라는걸 증명하는게 쬐끔 까다롭긴 하다.


2. Maybe Injective

Maybe 타입생성자가 injective 하다는걸 증명하는 문제임. 즉 Maybe A = Maybe B -> A = B

이 문제도 1번 문제하고 비슷하게 A와 B사이의 isomorphism을 만들어서 풀면 됨.

1번 보다 isomorphism을 떠올리기 힘들긴 한데, "두 집합 A, B 각각에 원소를 1개씩 추가한 것이 isomorphic하다면 A, B도 isomorphic하다"로 classical하게 생각하면 할 수 있음. isomorphism임의 증명도 1번보다 더 길지만 그냥 케이스를 전부 쪼개면 단순한 증명의 반복일 뿐임.


3. Left, left! Right, right! Comp! Symmetric! Q!E!D!

이건 앞에 문제들이랑은 조금 다른데, HIT(Higher Inductive Type)이 나옴.

1,2번도 그렇지만 이건 특히 알면 손 안대고 코풀기 수준이고, 모르면 고생하는 그런 문제 같음.

그냥 패턴매칭하고 interval variable들을 잘 조작(∧,∨,~)해서 boundary를 만족하는 큐브를 만들면 되

나는 i∨~i ≠ 1, i∧~i≠0 인걸 생각 못해서 좀 헤맸는데 풀고나니까 답은 되게 간단하더라.