@@ -802,16 +802,6 @@ punchIn-injective (suc i) (suc j) (suc k) ↑j+1≡↑k+1 =
802
802
punchInᵢ≢i : ∀ i (j : Fin n) → punchIn i j ≢ i
803
803
punchInᵢ≢i (suc i) (suc j) = punchInᵢ≢i i j ∘ suc-injective
804
804
805
- punchIn-mono-≤ : ∀ i (j k : Fin n) → j ≤ k → punchIn i j ≤ punchIn i k
806
- punchIn-mono-≤ zero _ _ j≤k = s≤s j≤k
807
- punchIn-mono-≤ (suc _) zero _ z≤n = z≤n
808
- punchIn-mono-≤ (suc i) (suc j) (suc k) (s≤s j≤k) = s≤s (punchIn-mono-≤ i j k j≤k)
809
-
810
- punchIn-cancel-≤ : ∀ i (j k : Fin n) → punchIn i j ≤ punchIn i k → j ≤ k
811
- punchIn-cancel-≤ zero _ _ (s≤s j≤k) = j≤k
812
- punchIn-cancel-≤ (suc _) zero _ z≤n = z≤n
813
- punchIn-cancel-≤ (suc i) (suc j) (suc k) (s≤s ↑j≤↑k) = s≤s (punchIn-cancel-≤ i j k ↑j≤↑k)
814
-
815
805
------------------------------------------------------------------------
816
806
-- punchOut
817
807
------------------------------------------------------------------------
@@ -845,22 +835,6 @@ punchOut-injective {suc n} {suc i} {zero} {zero} _ _ _ = refl
845
835
punchOut-injective {suc n} {suc i} {suc j} {suc k} i≢j i≢k pⱼ≡pₖ =
846
836
cong suc (punchOut-injective (i≢j ∘ cong suc) (i≢k ∘ cong suc) (suc-injective pⱼ≡pₖ))
847
837
848
- punchOut-mono-≤ : ∀ {i j k : Fin (suc n)} (i≢j : i ≢ j) (i≢k : i ≢ k) →
849
- j ≤ k → punchOut i≢j ≤ punchOut i≢k
850
- punchOut-mono-≤ {_ } {zero } {zero } {_ } 0≢0 _ z≤n = contradiction refl 0≢0
851
- punchOut-mono-≤ {_ } {zero } {suc _} {suc _} _ _ (s≤s j≤k) = j≤k
852
- punchOut-mono-≤ {suc _} {suc _} {zero } {_ } _ _ z≤n = z≤n
853
- punchOut-mono-≤ {suc _} {suc _} {suc _} {suc _} i≢j i≢k (s≤s j≤k) = s≤s (punchOut-mono-≤ (i≢j ∘ cong suc) (i≢k ∘ cong suc) j≤k)
854
-
855
- punchOut-cancel-≤ : ∀ {i j k : Fin (suc n)} (i≢j : i ≢ j) (i≢k : i ≢ k) →
856
- punchOut i≢j ≤ punchOut i≢k → j ≤ k
857
- punchOut-cancel-≤ {_ } {zero } {zero } {_ } 0≢0 _ _ = contradiction refl 0≢0
858
- punchOut-cancel-≤ {_ } {zero } {suc _} {zero } _ 0≢0 _ = contradiction refl 0≢0
859
- punchOut-cancel-≤ {suc _} {zero } {suc _} {suc _} _ _ pⱼ≤pₖ = s≤s pⱼ≤pₖ
860
- punchOut-cancel-≤ {_ } {suc _} {zero } {_ } _ _ _ = z≤n
861
- punchOut-cancel-≤ {suc _} {suc _} {suc _} {zero } _ _ ()
862
- punchOut-cancel-≤ {suc _} {suc _} {suc _} {suc _} i≢j i≢k (s≤s pⱼ≤pₖ) = s≤s (punchOut-cancel-≤ (i≢j ∘ cong suc) (i≢k ∘ cong suc) pⱼ≤pₖ)
863
-
864
838
punchIn-punchOut : ∀ {i j : Fin (suc n)} (i≢j : i ≢ j) →
865
839
punchIn i (punchOut i≢j) ≡ j
866
840
punchIn-punchOut {_} {zero} {zero} 0≢0 = contradiction refl 0≢0
0 commit comments