text:
{-# OPTIONS --without-K #-}

open import HoTT
open import homotopy.JoinFunc

-- Associativity of the join (work in progress)

module homotopy.JoinAssoc3 where

 import homotopy.JoinAssoc as Assoc

 module JoinAssoc3 {i} (A : Type i) (B : Type i) (C : Type i) where

  module A31 = Assoc A B C
  postulate
--    from : ((A * B) * C) → (A * (B * C))
--    to : (A * (B * C)) → ((A * B) * C)
    to-from : (z : (A * (B * C))) → (A31.to (A31.from z)) == z

  from = A31.from
  to = A31.to

  idc : C → C
  idc c = c
  ida : A → A
  ida a = a

--  import homotopy.JoinComm as JoinComm
--  open JoinComm

--  from' : ((A * B) * C) → (A * (B * C))
--  from' z =  {! swap $  swap ** ida [ to $ swap $ swap ** idc [ z ] ] !}

 module _  {i} {A : Type i} {B : Type i} {C : Type i} where

  import homotopy.JoinComm as JoinComm
  open JoinComm

  module JA31 = JoinAssoc3 A B C
  module JA32 = JoinAssoc3 C B A
  module JA33 = JoinAssoc3 B A C
  idc : C → C
  idc c = c
  ida : A → A
  ida a = a

  -- need A * (B * C)
  from-to : (z : ((A * B) * C)) -> (JA31.from (JA31.to z)) == z
  from-to z with  JA31.to z -- idc ** swap [ {! swap $ swap ** idc [ z ]!} ] --JA32.to $ swap $ swap ** idc [ z ] ]
  ... | p = {!JA31.to-from p!} -- JA31.from-to p

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: UlrikBuchholtz/HoTT-Agda

max_forks_repo_name: UlrikBuchholtz/HoTT-Agda


text:
{- Formal verification of authenticated append-only skiplists in Agda, version 1.0.

   Copyright (c) 2020 Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import Data.Unit.NonEta
open import Data.Empty
open import Data.Fin using (Fin; fromℕ≤) renaming (zero to fz; suc to fs)
import      Data.Fin.Properties renaming (_≟_ to _≟Fin_)
open import Data.Sum
open import Data.Product
open import Data.Product.Properties
open import Data.Nat renaming (_≟_ to _≟ℕ_; _≤?_ to _≤?ℕ_)
open import Data.Nat.Properties
open import Data.List renaming (map to List-map)
open import Data.List.Properties using (∷-injective; length-++)
open import Data.List.Relation.Binary.Pointwise using (decidable-≡)
open import Data.List.Relation.Unary.All as List-All
open import Data.List.Relation.Unary.Any renaming (map to Any-map)
open import Data.List.Relation.Unary.Any.Properties renaming (gmap to Any-gmap)
open import Data.Bool hiding (_≤_ ; _<_)
open import Data.Maybe renaming (map to Maybe-map)

open import Function using (_∘_)

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open import Relation.Binary.Core
open import Relation.Nullary

-- This module contains various useful lemmas

module AAOSL.Lemmas where

 -----------------------------
 -- Properties about functions

 postulate  -- valid assumption, functional extensionality
   fun-ext : ∀{a b}{A : Set a}{B : Set b}
           → {f g : A → B}
           → (∀ x → f x ≡ g x)
           → f ≡ g

 ------------------------------
 -- Properties about inequality

 ≢-pi : ∀{a}{A : Set a}{m n : A}(p q : m ≢ n) → p ≡ q
 ≢-pi p q = fun-ext {f = p} {q} (λ x → ⊥-elim (p x))

 suc-≢ : ∀ {m n} → (suc m ≢ suc n) → m ≢ n
 suc-≢ sm≢sn m≡n = sm≢sn (cong suc m≡n)

 *-cong-≢ : ∀ p {m n} → 0 < p → m ≢ n → p * m ≢ p * n
 *-cong-≢ (suc p) 0<p m≢n p*m≡p*n = m≢n (*-cancelˡ-≡ p p*m≡p*n)

 ⊥-1≡m*2 : ∀ m → 1 ≢ m * 2
 ⊥-1≡m*2 zero = λ x → <⇒≢ (s≤s z≤n) (sym x)
 ⊥-1≡m*2 (suc m) = λ x → <⇒≢ (s≤s z≤n) (suc-injective x)

 ∸-≢ : ∀{m} n → 1 ≤ n → n ≤ suc m → suc m ∸ n ≢ suc m
 ∸-≢ {m} (suc n) 1≤n (s≤s n≤sm)
   rewrite sym (+-identityʳ (suc m))
         | sym (n∸n≡0 n)
         | sym (+-∸-assoc m {n} {n} ≤-refl)
         | +-∸-comm {m} n {n} n≤sm = m≢1+m+n (m ∸ n)

 1≢a+b : ∀{a b} → 1 ≤ a → 1 ≤ b → 1 ≢ a + b
 1≢a+b (s≤s {n = a} 1≤a) (s≤s {n = b} 1≤b) abs
   rewrite +-comm a (suc b) = 1+n≢0 (sym (suc-injective abs))

 0≢a*b-magic : ∀{a b} → 0 < a → 0 < b → 0 ≢ a * b
 0≢a*b-magic {a} {b} 0<a 0<b hip
   with m*n≡0⇒m≡0∨n≡0 a (sym hip)
 ... | inj₁ x = <⇒≢ 0<a (sym x)
 ... | inj₂ y = <⇒≢ 0<b (sym y)

 -----------------------------------
 -- Injectivty of ℕ ranged functions

 *2-injective : ∀ n m → n * 2 ≡ m * 2 → m ≡ n
 *2-injective zero    zero    x = refl
 *2-injective (suc n) (suc m) x
    = cong suc (*2-injective n m (suc-injective (suc-injective x)))

 2^-injective : ∀ {n m : ℕ}
   → 2 ^ n ≡ 2 ^ m
   → n ≡ m
 2^-injective {n} {zero} 2^n≡2^0
     with (m^n≡1⇒n≡0∨m≡1 2 n 2^n≡2^0)
 ...| inj₁ m≡0 = m≡0
 2^-injective {zero} {suc m} 2^0≡2^sm
     with (m^n≡1⇒n≡0∨m≡1 2 (suc m) (sym 2^0≡2^sm))
 ...| inj₁ sm≡0 = sym sm≡0
 2^-injective {suc n} {suc m} 2^n≡2^m = cong suc (2^-injective (*-cancelˡ-≡ {2 ^ n} {2 ^ m} 1 2^n≡2^m))

 +-inj : ∀ {m n p : ℕ} → m + n ≡ m + p → n ≡ p
 +-inj {0}     {n} {p} prf = prf
 +-inj {suc m} {n} {p} prf =  +-inj (suc-injective prf)

 ∸-inj : ∀{m} o n → o ≤ m → n ≤ m → m ∸ o ≡ m ∸ n → o ≡ n
 ∸-inj {m} o n o≤m n≤m m∸o≡m∸n =
       begin
         o
       ≡⟨ sym (m∸[m∸n]≡n o≤m) ⟩
         m ∸ (m ∸ o)
       ≡⟨ cong (m ∸_) m∸o≡m∸n ⟩
         m ∸ (m ∸ n)
       ≡⟨ m∸[m∸n]≡n n≤m ⟩
         n
       ∎

 -------------------------------
 -- Properties about _≤_ and _<_

 <-≤-trans : ∀{m n o} → m < n → n ≤ o → m < o
 <-≤-trans p q = ≤-trans p q

 ≤-<-trans : ∀{m n o} → m ≤ n → n < o → m < o
 ≤-<-trans p q = ≤-trans (s≤s p) q

 ≤-unstep2 : ∀{m n} → suc m ≤ suc n → m ≤ n
 ≤-unstep2 (s≤s p) = p

 ≤-unstep : ∀{m n} → suc m ≤ n → m ≤ n
 ≤-unstep (s≤s p) = ≤-step p

 0<-suc : ∀{m} → 0 < m → ∃[ n ] (m ≡ suc n)
 0<-suc (s≤s p) = _ , refl

 1≤0-⊥ : 1 ≤ 0 → ⊥
 1≤0-⊥ ()

 -------------------------------
 -- Properties of Multiplication

 a*2-lemma : ∀ a → (a + (a + zero)) ≡ a * 2
 a*2-lemma a rewrite *-comm a 2 = refl

 *2< : ∀ (m n : ℕ)
   → m * 2 < n * 2
   → m < n
 *2< 0       0       ()
 *2< 0       (suc n) _             = s≤s z≤n
 *2< (suc m) (suc n) (s≤s (s≤s x)) = s≤s (*2< m n x)

 a*b*2-lemma : ∀ a b → a * b * 2 ≡ (a + (a + zero)) * b
 a*b*2-lemma a b rewrite *-comm (a * b) 2
                       | *-assoc 2 a b = refl

 +-*-suc' : ∀ m n → m * suc n ≡ m + n * m
 +-*-suc' m n with *-suc m n
 ...| xx rewrite *-comm n m = xx

 ----------------------------------
 -- Properties of divisibility by 2

 1+n=m*2⇒m<1+n : ∀ m n → 1 + n ≡ m * 2 → m < 1 + n
 1+n=m*2⇒m<1+n (suc zero) (suc n) eq = s≤s (s≤s z≤n)
 1+n=m*2⇒m<1+n (suc (suc m)) (suc (suc n)) eq = s≤s (<-trans ih (n<1+n (1 + n)))
   where
   eq' : 1 + n ≡ (1 + m) * 2
   eq' = +-cancelˡ-≡ 2 eq

   ih : (1 + m) < 1 + n
   ih = 1+n=m*2⇒m<1+n (1 + m) n eq'

 -------------------------------
 -- Properties of exponentiation

 1≤2^n : ∀ n → 1 ≤ (2 ^ n)
 1≤2^n 0       = s≤s z≤n
 1≤2^n (suc n) = ≤-trans (1≤2^n n) (m≤m+n (2 ^ n) ((2 ^ n) + zero))

 1<2^sucn : ∀ n → 1 < (2 ^ suc n)
 1<2^sucn n = ≤∧≢⇒< (1≤2^n (suc n))
                    (subst (λ P → 1 ≢ (2 ^ n) + P)
                      (+-comm 0 (2 ^ n))
                      (1≢a+b (1≤2^n n) (1≤2^n n)))

 pow*d>1 : ∀ k d → 0 < k → 0 < d → 1 < 2 ^ k * d
 pow*d>1 (suc k) d 0<k 0<d = *-mono-≤ (1<2^sucn k) 0<d

 2^ld-2l : ∀ l₀ l₁ d → l₁ ≤ l₀
              → (2 ^ l₀) * d ∸ 2 ^ l₁ ≡ 2 ^ l₁ * (2 ^ (l₀ ∸ l₁) * d ∸ 1)
 2^ld-2l l₀ l₁ d x rewrite *-distribˡ-∸ (2 ^ l₁) (2 ^ (l₀ ∸ l₁) * d) 1
                         | sym (*-assoc (2 ^ l₁) (2 ^ (l₀ ∸ l₁)) d)
                         | sym (^-distribˡ-+-* 2 l₁ (l₀ ∸ l₁))
                         | sym (+-∸-assoc l₁ {l₀} {l₁} x)
                         | m+n∸m≡n l₁ l₀
                         | *-identityʳ (2 ^ l₁) = refl

 -------------------------------------
 -- Monotonicity of ℕ ranged functions

 2^-mono : ∀{m n} → m < n → 2 ^ m < 2 ^ n
 2^-mono {zero} {suc zero}    x  = s≤s (s≤s z≤n)
 2^-mono {zero} {suc (suc n)} x  = +-mono-<-≤ (2^-mono {zero} {suc n} (s≤s z≤n))
                                              (m≤n+m zero (2 * 2 ^ n))
 2^-mono {suc m} {suc n} (s≤s x) = +-mono-<   (2^-mono x)
                                              (+-mono-<-≤ (2^-mono x) z≤n)

 log-mono : ∀ (l n : ℕ)
   → 2 ^ l < 2 ^ n
   → l < n
 log-mono l 0 x = ⊥-elim (<⇒≱ x (1≤2^n l))
 log-mono 0 (suc n) x = s≤s z≤n
 log-mono (suc l) (suc n) x
   rewrite a*2-lemma (2 ^ l) | a*2-lemma (2 ^ n)
   =  s≤s ((log-mono l n (*2< (2 ^ l) (2 ^ n) x)))

 ^-mono : ∀ (l n : ℕ) → l ≤ n → 2 ^ l ≤ 2 ^ n
 ^-mono zero    n    _  = 1≤2^n n
 ^-mono (suc l) zero ()
 ^-mono (suc l) (suc n) (s≤s xx)
   rewrite +-identityʳ (2 ^ l)
         | +-identityʳ (2 ^ n)
         = +-mono-≤ (^-mono l n xx)  (^-mono l n xx)

 2^kd-mono : ∀{m n d} → m ≤ n → 0 < d → 2 ^ m ≤ 2 ^ n * d
 2^kd-mono {m} {n} {d} m≤n 0<d = ≤-trans (^-mono m n m≤n) (m≤m*n (2 ^ n) 0<d)

 1≤m*n⇒0<n : ∀{m n} → 1 ≤ m * n → 0 < n
 1≤m*n⇒0<n {m} {n} 1≤m*n rewrite *-comm m n = 1≤n*m⇒0<n n m 1≤m*n
     where 1≤n*m⇒0<n : ∀ m n →  1 ≤ m * n → 0 < m
           1≤n*m⇒0<n (suc m) n 1≤m*n = s≤s z≤n

 n+p≡m+q∧n<m⇒q<p : ∀ {n p m q} → n < m → n + p ≡ m + q → q < p
 n+p≡m+q∧n<m⇒q<p {n} {p} {m} {q} n<m n+p≡m+q = +-cancelˡ-< n (subst ((n + q) <_) (sym n+p≡m+q) (+-monoˡ-< q n<m))

 -------------------
 -- Misc. Properties

 ss≰1 : ∀{n} → suc (suc n) ≰ 1
 ss≰1 (s≤s ())

 ∸-split : ∀{a b c} → c < b → b < a → a ∸ c ≡ (a ∸ b) + (b ∸ c)
 ∸-split {a} {b} {c} c<b b<a
   rewrite sym (+-∸-comm {a} (b ∸ c) {b} (<⇒≤ b<a))
         | sym (+-∸-assoc a {b} {c} (<⇒≤ c<b))
         | +-∸-comm {a} b {c} (<⇒≤ (<-trans c<b b<a))
         | m+n∸n≡m (a ∸ c) b = refl

 0<m-n : ∀{m n} → n < m → 0 < m ∸ n
 0<m-n {n = zero} (s≤s x) = s≤s x
 0<m-n {n = suc n} (s≤s x) = 0<m-n x

 2^k-is-suc : ∀ n → ∃ (λ r → 2 ^ n ≡ suc r)
 2^k-is-suc zero = 0 , refl
 2^k-is-suc (suc n) with 2^k-is-suc n
 ...| fst , snd rewrite snd
                      | +-identityʳ fst
                      | +-comm fst (suc fst) = (suc (fst + fst)) , refl

 -------------------------
 -- Properties about lists

 ∷≡[]-⊥ : ∀{a}{A : Set a}{x : A}{xs : List A}
        → _≡_ {a} {List A} (x ∷ xs) [] → ⊥
 ∷≡[]-⊥ ()

 All-pi : ∀{a}{A : Set a}{P : A → Set}
        → (∀ {x}(p₁ p₂ : P x) → p₁ ≡ p₂)
        → {xs : List A}
        → (a₁ a₂ : All P xs)
        → a₁ ≡ a₂
 All-pi P-pi [] [] = refl
 All-pi P-pi (a ∷ as) (b ∷ bs) = cong₂ _∷_ (P-pi a b) (All-pi P-pi as bs)

 _∈_ : {A : Set} → A → List A → Set
 x ∈ xs = Any (_≡_ x) xs

 witness : {A : Set}{P : A → Set}{x : A}{xs : List A}
         → x ∈ xs → All P xs → P x
 witness {x = x} {xs = []} ()
 witness {P = P } {x = x} {xh ∷ xt} (here px) all = subst P (sym px) (List-All.head all)
 witness {x = x} {xh ∷ xt} (there x∈xt) all = witness x∈xt (List-All.tail all)

 List-map-≡ : {A B : Set}
            → (f g : A → B)
            → (xs : List A)
            → (∀ x → x ∈ xs → f x ≡ g x)
            → List-map f xs ≡ List-map g xs
 List-map-≡ f g [] prf = refl
 List-map-≡ f g (x ∷ xs) prf
   = cong₂ _∷_ (prf x (here refl)) (List-map-≡ f g xs
                                     (λ x₁ prf' → prf x₁ (there prf')))

 List-map-≡-All : {A B : Set}
                → (f g : A → B)
                → (xs : List A)
                → All (λ x → f x ≡ g x) xs
                → List-map f xs ≡ List-map g xs
 List-map-≡-All f g xs hyp
   = List-map-≡ f g xs (λ x x∈xs → witness x∈xs hyp)

 nats : (n : ℕ) → List (Fin n)
 nats 0       = []
 nats (suc n) = fz ∷ List-map fs (nats n)

 nats-correct : ∀{m}(x : Fin m) → x ∈ nats m
 nats-correct {suc m} fz     = here refl
 nats-correct {suc m} (fs x) = there (Any-gmap (cong fs) (nats-correct x))

 nats-length : ∀{m} → 0 < m → 1 ≤ length (nats m)
 nats-length (s≤s prf) = s≤s z≤n

 ++-inj : ∀{a}{A : Set a}{m n o p : List A}
        → length m ≡ length n → m ++ o ≡ n ++ p
        → m ≡ n × o ≡ p
 ++-inj {m = []}     {x ∷ n} () hip
 ++-inj {m = x ∷ m}  {[]}    () hip
 ++-inj {m = []}     {[]}     lhip hip
   = refl , hip
 ++-inj {m = m ∷ ms} {n ∷ ns} lhip hip
   with ++-inj {m = ms} {ns} (suc-injective lhip) (proj₂ (∷-injective hip))
 ...| (mn , op) rewrite proj₁ (∷-injective hip)
    = cong (n ∷_) mn , op

 ++-abs : ∀{a}{A : Set a}{n : List A}(m : List A)
        → 1 ≤ length m → [] ≡ m ++ n → ⊥
 ++-abs [] ()
 ++-abs (x ∷ m) imp ()

 ++-injₕ : ∀{a}{A : Set a}{m o p : List A}
         → m ++ o ≡ m ++ p
         → o ≡ p
 ++-injₕ {m = m} {o} {p} r = proj₂ (++-inj {m = m} {m} {o} {p} refl r)

ext: agda

max_stars_repo_name: cwjnkins/aaosl-agda

max_issues_repo_name: cwjnkins/aaosl-agda

max_forks_repo_name: cwjnkins/aaosl-agda


text:
module Algebra.Module.Morphism.Module where

open import Assume using (assume)
open import Algebra.Core using (Op₁; Op₂)
open import Algebra.Bundles using (CommutativeRing)
open import Algebra.Module.Bundles using (Module)
open import Algebra.Module.Structures using (IsModule)
open import Algebra.Module.Normed using (IsNormedModule; NormedModule)
open import Relation.Binary.Core using (Rel)
open import Data.Product using (Σ-syntax; ∃-syntax; _×_; _,_; proj₁)

open import Algebra.Module.Morphism.Structures
  using (IsModuleHomomorphism; IsModuleMonomorphism; IsModuleIsomorphism)

open import Level using (_⊔_; suc)

private
  module toModule
    {a} (A : Set a)
    {r ℓr} {CR : CommutativeRing r ℓr}
    {mb ℓmb} (MB : Module CR mb ℓmb)
    where

    private
      module CR = CommutativeRing CR
      module MB = Module MB

      Carrierᴹ : Set _
      Carrierᴹ = A → MB.Carrierᴹ

      _≈ᴹ_ : Rel Carrierᴹ _
      f ≈ᴹ g = ∀ a → f a MB.≈ᴹ g a

      _+ᴹ_ : Op₂ Carrierᴹ
      f +ᴹ g = λ a → f a MB.+ᴹ g a

      _*ₗ_ : CR.Carrier → Carrierᴹ → Carrierᴹ
      s *ₗ f = λ a → s MB.*ₗ f a

      _*ᵣ_ : Carrierᴹ → CR.Carrier → Carrierᴹ
      f *ᵣ s = λ a → f a MB.*ᵣ s

      0ᴹ : Carrierᴹ
      0ᴹ _ = MB.0ᴹ

      -ᴹ_ : Op₁ Carrierᴹ
      -ᴹ_ f = λ a → MB.-ᴹ f a

    isModule : IsModule CR _≈ᴹ_ _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_
    isModule = assume

→-module
  : ∀ {a} (A : Set a)
    {r ℓr} {CR : CommutativeRing r ℓr}
    {mb ℓmb} (MB : Module CR mb ℓmb)
  → Module CR (a ⊔ mb) (a ⊔ ℓmb)
→-module A MB = record { toModule A MB }

→-module'
  : ∀ {r ℓr} {CR : CommutativeRing r ℓr}
    {ma ℓma} (MA : Module CR ma ℓma)
    {mb ℓmb} (MB : Module CR mb ℓmb)
  → Module CR (ma ⊔ mb) (ma ⊔ ℓmb)
→-module' MA MB = →-module (Carrierᴹ MA) MB
  where open Module

module _
  {r ℓr} {CR : CommutativeRing r ℓr}
  {ma ℓma} (MA : Module CR ma ℓma)
  {mb ℓmb} (MB : Module CR mb ℓmb)
  where

  private
    module MA = Module MA
    module MB = Module MB

  _⊸_ : Set _
  _⊸_ = ∃[ f ] IsModuleHomomorphism MA MB f

  ⊸-module : Module CR (r ⊔ ma ⊔ ℓma ⊔ mb ⊔ ℓmb) (ma ⊔ ℓmb)
  ⊸-module =
    record
    { Carrierᴹ = _⊸_
    ; _≈ᴹ_ = λ f g → ∀ x → proj₁ f x MB.≈ᴹ proj₁ g x
    ; _+ᴹ_ = λ f g → (λ x → proj₁ f x MB.+ᴹ proj₁ g x) , assume
    ; _*ₗ_ = λ s f → (λ x → s MB.*ₗ proj₁ f x) , assume
    ; _*ᵣ_ = λ f s → (λ x → proj₁ f x MB.*ᵣ s) , assume
    ; 0ᴹ = (λ x → MB.0ᴹ) , assume
    ; -ᴹ_ = λ f → (λ x → MB.-ᴹ proj₁ f x) , assume
    ; isModule = assume
    }

module _
  {r ℓr} {CR : CommutativeRing r ℓr}
  (open CommutativeRing CR using () renaming (Carrier to S))
  {rel} {_≤_ : Rel S rel}
  {ma ℓma} (MA : NormedModule CR _≤_ ma ℓma)
  {mb ℓmb} (MB : NormedModule CR _≤_ mb ℓmb)
  where

  private
    module MB = NormedModule MB
    module MA = NormedModule MA

  ⊸-normed : NormedModule CR _≤_ _ _
  ⊸-normed =
    record
    { M = ⊸-module MA.M MB.M
    ; ∥_∥ = λ f → MB.∥ proj₁ f MA.0ᴹ ∥
    ; isNormedModule = assume
    }

max_stars_repo_name: cspollard/reals

max_issues_repo_name: cspollard/reals

max_forks_repo_name: cspollard/reals


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category where

open import Level

-- The main definitions are in:
open import Categories.Category.Core public

private
  variable
    o ℓ e : Level

-- Convenience functions for working over mupliple categories at once:
-- C [ x , y ] (for x y objects of C) - Hom_C(x , y)
-- C [ f ≈ g ] (for f g arrows of C)  - that f and g are equivalent arrows
-- C [ f ∘ g ] (for f g composables arrows of C) - composition in C
infix 10  _[_,_] _[_≈_] _[_∘_]

_[_,_] : (C : Category o ℓ e) → (X : Category.Obj C) → (Y : Category.Obj C) → Set ℓ
_[_,_] = Category._⇒_

_[_≈_] : (C : Category o ℓ e) → ∀ {X Y} (f g : C [ X , Y ]) → Set e
_[_≈_] = Category._≈_

_[_∘_] : (C : Category o ℓ e) → ∀ {X Y Z} (f : C [ Y , Z ]) → (g : C [ X , Y ]) → C [ X , Z ]
_[_∘_] = Category._∘_

module Definitions (𝓒 : Category o ℓ e) where
  open Category 𝓒

  CommutativeSquare : {A B C D : Obj} → (f : A ⇒ B) (g : A ⇒ C) (h : B ⇒ D) (i : C ⇒ D) → Set _
  CommutativeSquare f g h i = h ∘ f ≈ i ∘ g

-- Combinators for commutative diagram
-- The idea is to use the combinators to write commutations in a more readable way.
-- It starts with [_⇒_]⟨_≈_⟩, and within the third and fourth places, use _⇒⟨_⟩_ to
-- connect morphisms with the intermediate object specified.
module Commutation (𝓒 : Category o ℓ e) where
  open Category 𝓒

  infix 1 [_⇒_]⟨_≈_⟩
  [_⇒_]⟨_≈_⟩ : ∀ (A B : Obj) → A ⇒ B → A ⇒ B → Set _
  [ A ⇒ B ]⟨ f ≈ g ⟩ = f ≈ g

  infixl 2 connect
  connect : ∀ {A C : Obj} (B : Obj) → A ⇒ B → B ⇒ C → A ⇒ C
  connect B f g = g ∘ f

  syntax connect B f g = f ⇒⟨ B ⟩ g

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS -v treeless.opt:20 #-}

open import Agda.Builtin.Nat
open import Common.IO using (return)
open import Agda.Builtin.Unit

data List {a} (A : Set a) : Set a where
  []  : List A
  _∷_ : A → List A → List A

data Vec {a} (A : Set a) : ..(_ : Nat) → Set a where
  [] : Vec A 0
  _∷_ : ∀ ..{n} → A → Vec A n → Vec A (suc n)

-- We can't handle smashing this yet. Different backends might compile
-- datatypes differently so we can't guarantee representational
-- compatibility. Possible solution: handle datatype compilation in
-- treeless as well and be explicit about which datatypes compile to the
-- same representation.
vecToList : ∀ {a} {A : Set a} ..{n} → Vec A n → List A
vecToList []       = []
vecToList (x ∷ xs) = x ∷ vecToList xs

data Fin : ..(_ : Nat) → Set where
  zero : ∀ ..{n} → Fin (suc n)
  suc  : ∀ ..{n} → Fin n → Fin (suc n)

-- These should all compile to identity functions:

wk : ∀ ..{n} → Fin n → Fin (suc n)
wk  zero   = zero
wk (suc i) = suc (wk i)

wkN : ∀ ..{n m} → Fin n → Fin (n + m)
wkN  zero   = zero
wkN (suc i) = suc (wkN i)

wkN′ : ∀ m ..{n} → Fin n → Fin (m + n)
wkN′ zero i = i
wkN′ (suc m) i = wk (wkN′ m i)

vecPlusZero : ∀ {a} {A : Set a} ..{n} → Vec A n → Vec A (n + 0)
vecPlusZero [] = []
vecPlusZero (x ∷ xs) = x ∷ vecPlusZero xs

main = return tt

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Pr where

data FF : Set where

magic : {X : Set} -> FF -> X
magic ()

record TT : Set where

data Id {S : Set}(s : S) : S -> Set where
  refl : Id s s

data Pr : Set1 where
  tt : Pr
  ff : Pr
  _/\_ : Pr -> Pr -> Pr
  all : (S : Set) -> (S -> Pr) -> Pr
  _eq_ : {S : Set} -> S -> S -> Pr

record Sig (S : Set)(T : S -> Set) : Set where
  field
    fst : S
    snd : T fst

open module Sig' {S : Set}{T : S -> Set} = Sig {S}{T} public

_,_ : {S : Set}{T : S -> Set}(s : S) -> T s -> Sig S T
s , t = record {fst = s ; snd = t}

[|_|] : Pr -> Set
[| tt |] = TT
[| ff |] = FF
[| P /\ Q |] = Sig [| P |] \_ -> [| Q |]
[| all S P |] = (x : S) -> [| P x |]
[| a eq b |] = Id a b

_=>_ : Pr -> Pr -> Pr
P => Q = all [| P |] \_ -> Q

∼ : Pr -> Pr
∼ P = P => ff

data Decision (P : Pr) : Set where
  yes  : [| P |]   -> Decision P
  no   : [| ∼ P |] -> Decision P

data Bool : Set where
  true : Bool
  false : Bool

So : Bool -> Pr
So true = tt
So false = ff

not : Bool -> Bool
not true = false
not false = true

so : (b : Bool) -> Decision (So b)
so true = yes _
so false = no magic

potahto : (b : Bool) -> [| So (not b) => ∼ (So b) |]
potahto true () _
potahto false _ ()

PEx : (P : Pr) -> ([| P |] -> Pr) -> Pr
PEx P Q = P /\ all [| P |] Q

Pow : Set -> Set1
Pow X = X -> Pr

_==>_ : {X : Set} -> Pow X -> Pow X -> Pr
_==>_ {X} P Q = all X \x -> P x => Q x

Decidable : {X : Set}(P : Pow X) -> Set
Decidable {X} P = (x : X) -> Decision (P x)

data _:-_ (S : Set)(P : Pow S) : Set where
  [_/_] : (s : S) -> [| P s |] -> S :- P

wit : {S : Set}{P : S -> Pr} -> S :- P -> S
wit [ s / p ] = s

cert : {S : Set}{P : S -> Pr}(sp : S :- P) -> [| P (wit sp) |]
cert [ s / p ] = p

_??_ : {S : Set}{P : S -> Pr}
      (sp : S :- P){M : Set} ->
      ((s : S)(p : [| P s |]) -> M) ->
      M
sp ?? m = m (wit sp) (cert sp)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Data.InfNat where

open import Cubical.Data.InfNat.Base public
open import Cubical.Data.InfNat.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
{-# OPTIONS --sized-types #-}

module Lang.Size where

-- Some stuff about sizes that seems to :
-- • Types:
--   • SizeU   : TYPE
--   • Size    : TYPE
--   • <ˢⁱᶻᵉ_  : Size → TYPE
--   • 𝐒ˢⁱᶻᵉ   : Size → Size
--   • ∞ˢⁱᶻᵉ   : Size
--   • _⊔ˢⁱᶻᵉ_ : Size → Size → Size
-- • Subtyping           : ∀s₁∀s₂. (s₁: <ˢⁱᶻᵉ s₂) → (s₁: Size)
-- • Almost irreflexivity: ∀(s: Size). (s ≠ ∞ˢⁱᶻᵉ) → ¬(s: <ˢⁱᶻᵉ s)
-- • Transitivity        : ∀s₁∀s₂∀s₃. (s₁: <ˢⁱᶻᵉ s₂) → (s₂: <ˢⁱᶻᵉ s₃) → (s₁: <ˢⁱᶻᵉ s₃)
-- • Successor           : ∀(s: Size). s: <ˢⁱᶻᵉ 𝐒ˢⁱᶻᵉ(s)
-- • Maximum             : ∀(s: Size). s: <ˢⁱᶻᵉ ∞ˢⁱᶻᵉ
-- • Successor of maximum: 𝐒ˢⁱᶻᵉ(∞ˢⁱᶻᵉ) = ∞ˢⁱᶻᵉ
-- • Max function left   : ∀(s₁: Size)∀(s₂: Size)∀(s₃: Size). ((s₁: <ˢⁱᶻᵉ s₃) ∧ (s₂: <ˢⁱᶻᵉ s₃)) → (((s₁ ⊔ˢⁱᶻᵉ s₂)): <ˢⁱᶻᵉ s₃)
-- • Max function right  : ∀(s₁: Size)∀(s₂: Size)∀(s₃: Size). ((s₁: <ˢⁱᶻᵉ s₂) ∨ (s₁: <ˢⁱᶻᵉ s₃)) → (s₁: <ˢⁱᶻᵉ (s₂ ⊔ˢⁱᶻᵉ s₃))
-- • Max of maximum left : ∀(s: Size). s ⊔ˢⁱᶻᵉ ∞ˢⁱᶻᵉ = ∞ˢⁱᶻᵉ
-- • Max of maximum right: ∀(s: Size). ∞ˢⁱᶻᵉ ⊔ˢⁱᶻᵉ s = ∞ˢⁱᶻᵉ
-- TODO: What is SizeU? See https://github.com/agda/agda/blob/cabe234d3c784e20646636ad082cc1e04ddf007b/src/full/Agda/TypeChecking/Rules/Builtin.hs#L294 , https://github.com/agda/agda/blob/1eec63b1c5566b252c0a4a815ce1df99a772c475/src/full/Agda/TypeChecking/Primitive/Base.hs#L134

{-# BUILTIN SIZEUNIV SizeU #-}
{-# BUILTIN SIZE     Size    #-}
{-# BUILTIN SIZELT   <ˢⁱᶻᵉ_  #-}
{-# BUILTIN SIZESUC  𝐒ˢⁱᶻᵉ   #-}
{-# BUILTIN SIZEINF  ∞ˢⁱᶻᵉ   #-}
{-# BUILTIN SIZEMAX  _⊔ˢⁱᶻᵉ_ #-}

{-
private
  module Test where
    open import Relator.Equals

    types-SizeU : TYPE
    types-SizeU = SizeU

    types-Size : TYPE
    types-Size = Size

    types-<ˢⁱᶻᵉ : Size → TYPE
    types-<ˢⁱᶻᵉ = <ˢⁱᶻᵉ_

    types-𝐒ˢⁱᶻᵉ : Size → Size
    types-𝐒ˢⁱᶻᵉ = 𝐒ˢⁱᶻᵉ

    types-∞ˢⁱᶻᵉ : Size
    types-∞ˢⁱᶻᵉ = ∞ˢⁱᶻᵉ

    types-_⊔ˢⁱᶻᵉ_ : Size → Size → Size
    types-_⊔ˢⁱᶻᵉ_ = _⊔ˢⁱᶻᵉ_

    subtyping : ∀{s₂ : Size}{s₁ : <ˢⁱᶻᵉ s₂} → Size
    subtyping {s₁ = s₁} = s₁

    reflexivity-of-maximum : <ˢⁱᶻᵉ ∞ˢⁱᶻᵉ
    reflexivity-of-maximum = ∞ˢⁱᶻᵉ

    transitivity : ∀{s₃ : Size}{s₂ : <ˢⁱᶻᵉ s₃}{s₁ : <ˢⁱᶻᵉ s₂} → (<ˢⁱᶻᵉ s₃)
    transitivity {s₁ = s₁} = s₁

    maximum : ∀{s : Size} → <ˢⁱᶻᵉ ∞ˢⁱᶻᵉ
    maximum{s} = s

    successor-of-maximum : 𝐒ˢⁱᶻᵉ ∞ˢⁱᶻᵉ ≡ ∞ˢⁱᶻᵉ
    successor-of-maximum = [≡]-intro

    max-of-maximumₗ : ∀{s : Size} → (∞ˢⁱᶻᵉ ⊔ˢⁱᶻᵉ s ≡ ∞ˢⁱᶻᵉ)
    max-of-maximumₗ = [≡]-intro

    max-of-maximumᵣ : ∀{s : Size} → (s ⊔ˢⁱᶻᵉ ∞ˢⁱᶻᵉ ≡ ∞ˢⁱᶻᵉ)
    max-of-maximumᵣ = [≡]-intro

    max-function-left : ∀{s₃ : Size}{s₁ : <ˢⁱᶻᵉ s₃}{s₂ : <ˢⁱᶻᵉ s₃} → (<ˢⁱᶻᵉ s₃)
    max-function-left {s₁ = s₁}{s₂ = s₂} = s₁ ⊔ˢⁱᶻᵉ s₂

    max-function-rightₗ : ∀{s₂ s₃ : Size}{s₁ : <ˢⁱᶻᵉ s₂} → (<ˢⁱᶻᵉ (s₂ ⊔ˢⁱᶻᵉ s₃))
    max-function-rightₗ {s₁ = s₁} = s₁

    max-function-rightᵣ : ∀{s₂ s₃ : Size}{s₁ : <ˢⁱᶻᵉ s₃} → (<ˢⁱᶻᵉ (s₂ ⊔ˢⁱᶻᵉ s₃))
    max-function-rightᵣ {s₁ = s₁} = s₁

    -- TODO: Is this supposed to not work? This is: ∀(sₗ₁ : Size)∀(sₗ₂ : Size)∀(sᵣ : Size) → (sₗ₁ <ˢⁱᶻᵉ sₗ₂) → ((sₗ₁ ⊔ˢⁱᶻᵉ sᵣ) <ˢⁱᶻᵉ (sₗ₂ ⊔ˢⁱᶻᵉ sᵣ))
    max-should-work? : ∀{sₗ₂ sᵣ : Size}{sₗ₁ : <ˢⁱᶻᵉ sₗ₂} → (<ˢⁱᶻᵉ (sₗ₂ ⊔ˢⁱᶻᵉ sᵣ))
    max-should-work? {sᵣ = sᵣ}{sₗ₁ = sₗ₁} = sₗ₁ ⊔ˢⁱᶻᵉ sᵣ
-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Variables and contexts
--
-- This module defines the syntax of contexts and subcontexts,
-- together with variables and properties of these notions.
--
-- This module is parametric in the syntax of types, so it
-- can be reused for different calculi.
------------------------------------------------------------------------

module Base.Syntax.Context
    (Type : Set)
  where

open import Relation.Binary
open import Relation.Binary.PropositionalEquality

-- Typing Contexts
-- ===============

import Data.List as List
open import Base.Data.ContextList public

Context : Set
Context = List.List Type

-- Variables
-- =========
--
-- Here it is clear that we are using de Bruijn indices,
-- encoded as natural numbers, more or less.
data Var : Context → Type → Set where
  this : ∀ {Γ τ} → Var (τ • Γ) τ
  that : ∀ {Γ σ τ} → (x : Var Γ τ) → Var (σ • Γ) τ

-- Weakening
-- =========
--
-- We define weakening based on subcontext relationship.

-- Subcontexts
-- -----------
--
-- Useful as a reified weakening operation,
-- and for making theorems strong enough to prove by induction.
--
-- The contents of this module are currently exported at the end
-- of this file.

-- This handling of contexts is recommended by [this
-- email](https://lists.chalmers.se/pipermail/agda/2011/003423.html) and
-- attributed to Conor McBride.
--
-- The associated thread discusses a few alternatives solutions, including one
-- where beta-reduction can handle associativity of ++.

module Subcontexts where
  infix 4 _≼_

  data _≼_ : (Γ₁ Γ₂ : Context) → Set where
    ∅ : ∅ ≼ ∅
    keep_•_ : ∀ {Γ₁ Γ₂} →
      (τ : Type) →
      Γ₁ ≼ Γ₂ →
      τ • Γ₁ ≼ τ • Γ₂
    drop_•_ : ∀ {Γ₁ Γ₂} →
      (τ : Type) →
      Γ₁ ≼ Γ₂ →
      Γ₁ ≼ τ • Γ₂

  -- Properties

  ∅≼Γ : ∀ {Γ} → ∅ ≼ Γ
  ∅≼Γ {∅} = ∅
  ∅≼Γ {τ • Γ} = drop τ • ∅≼Γ

  ≼-refl : Reflexive _≼_
  ≼-refl {∅} = ∅
  ≼-refl {τ • Γ} = keep τ • ≼-refl

  ≼-reflexive : ∀ {Γ₁ Γ₂} → Γ₁ ≡ Γ₂ → Γ₁ ≼ Γ₂
  ≼-reflexive refl = ≼-refl

  ≼-trans : Transitive _≼_
  ≼-trans ≼₁ ∅ = ≼₁
  ≼-trans (keep .τ • ≼₁) (keep τ • ≼₂) = keep τ • ≼-trans ≼₁ ≼₂
  ≼-trans (drop .τ • ≼₁) (keep τ • ≼₂) = drop τ • ≼-trans ≼₁ ≼₂
  ≼-trans ≼₁ (drop τ • ≼₂) = drop τ • ≼-trans ≼₁ ≼₂

  ≼-isPreorder : IsPreorder _≡_ _≼_
  ≼-isPreorder = record
    { isEquivalence = isEquivalence
    ; reflexive = ≼-reflexive
    ; trans = ≼-trans
    }

  ≼-preorder : Preorder _ _ _
  ≼-preorder = record
    { Carrier = Context
    ; _≈_ = _≡_
    ; _∼_ = _≼_
    ; isPreorder = ≼-isPreorder
    }

  module ≼-Reasoning where
    open import Relation.Binary.PreorderReasoning ≼-preorder public
      renaming
        ( _≈⟨_⟩_ to _≡⟨_⟩_
        ; _∼⟨_⟩_ to _≼⟨_⟩_
        ; _≈⟨⟩_ to _≡⟨⟩_
        )

  -- Lift a variable to a super context

  weaken-var : ∀ {Γ₁ Γ₂ τ} → Γ₁ ≼ Γ₂ → Var Γ₁ τ → Var Γ₂ τ
  weaken-var (keep τ • ≼₁) this = this
  weaken-var (keep τ • ≼₁) (that x) = that (weaken-var ≼₁ x)
  weaken-var (drop τ • ≼₁) x = that (weaken-var ≼₁ x)

-- Currently, we export the subcontext relation.

open Subcontexts public

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Sublist.Propositional directly.
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.List.Relation.Sublist.Propositional where

open import Data.List.Relation.Binary.Sublist.Propositional public

{-# WARNING_ON_IMPORT
"Data.List.Relation.Sublist.Propositional was deprecated in v1.0.
Use Data.List.Relation.Binary.Sublist.Propositional instead."
#-}


text:
-- Andreas, 2012-01-10
-- {-# OPTIONS -v tc.constr.findInScope:50 #-}
module InstanceGuessesMeta where

data Bool : Set where
  true false : Bool

postulate
  D : Bool -> Set
  E : Bool -> Set
  d : {x : Bool} -> D x
  f : {x : Bool}{{ dx : D x }} -> E x

b : E true
b = f  -- should succeed
-- Agda is now allowed to solve hidden x in type of d by unification,
-- when searching for inhabitant of D x

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
-- Andreas, 2011-04-14
-- {-# OPTIONS -v tc.cover:20 -v tc.lhs.unify:20 #-}
module Issue291a where

open import Common.Coinduction
open import Common.Equality

data RUnit : Set where
  runit : ∞ RUnit -> RUnit

j : (u : ∞ RUnit) -> ♭ u ≡ runit u -> Set
j u ()
-- needs to fail (reports a Bad split!)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module SystemF.Syntax where

open import SystemF.Syntax.Type public
open import SystemF.Syntax.Term public
open import SystemF.Syntax.Context public


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.Filler where

open import Cubical.Foundations.Prelude

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ

cube-cong : {a b : A}
            {p p' q q' : a ≡ b}
            (P : p ≡ p') (Q : q ≡ q')
            → (p ≡ q) ≡ (p' ≡ q')
cube-cong {p = p} {p' = p'} {q = q} {q' = q'} P Q =
  p ≡ q
    ≡⟨ cong (_≡ q) P ⟩
  p' ≡ q
    ≡⟨ cong (p' ≡_) Q ⟩
  p' ≡ q' ∎

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
{-# OPTIONS --syntactic-equality=2 --allow-unsolved-metas #-}

-- Limited testing suggests that --syntactic-equality=2 is a little
-- faster than --syntactic-equality=0 and --syntactic-equality=1 for
-- this file.

-- The option --allow-unsolved-metas and the open goal at the end of
-- the file ensure that time is not wasted on serialising things.

open import Agda.Builtin.Equality

data D : Set where
  c : D

data Delay-D : Set where
  now   : D → Delay-D
  later : Delay-D → Delay-D

-- The result of f x is 5000 applications of later to now x.

f : D → Delay-D
f x =
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  later (later (later (later (later (later (later (later (later (later (
  now x
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))))))))))))))))))))))))))))))

mutual

  α : D
  α = _

  _ : f α ≡ f c
  _ = refl

_ : Set
_ = {!!}


text:
open import Nat
open import Prelude
open import List
open import statics-core

-- erasure of cursor in the types and expressions is defined in the paper,
-- and in the core file, as a function on zexpressions. because of the
-- particular encoding of all the judgments as datatypes and the agda
-- semantics for pattern matching, it is sometimes also convenient to have
-- a judgemental form of erasure.
--
-- this file describes the obvious encoding of the view this function as a
-- jugement relating input and output as a datatype, and argues that this
-- encoding is correct by showing a isomorphism with the function. we also
-- show that as a correlary, the judgement is well moded at (∀, ∃!), which
-- is unsurprising if the jugement is written correctly.
--
-- taken together, these proofs allow us to move between the judgemental
-- form of erasure and the function form when it's convenient.
--
-- while we do not have it, the argument given here is sufficiently strong
-- to produce an equality between these things in a system with the
-- univalence axiom, as described in the homotopy type theory book and the
-- associated work done in agda.
module judgemental-erase where

  --cursor erasure for types, as written in the paper
  _◆t : ztyp → htyp
  ▹ t ◃ ◆t = t
  (t1 ==>₁ t2) ◆t = (t1 ◆t) ==> t2
  (t1 ==>₂ t2) ◆t = t1 ==> (t2 ◆t)
  (t1 ⊕₁ t2) ◆t = (t1 ◆t) ⊕ t2
  (t1 ⊕₂ t2) ◆t = t1 ⊕ (t2 ◆t)
  (t1 ⊠₁ t2) ◆t = (t1 ◆t) ⊠ t2
  (t1 ⊠₂ t2) ◆t = t1 ⊠ (t2 ◆t)

  --cursor erasure for expressions, as written in the paper
  _◆e : zexp → hexp
  ▹ x ◃ ◆e = x
  (e ·:₁ t) ◆e = (e ◆e) ·: t
  (e ·:₂ t) ◆e = e      ·: (t ◆t)
  ·λ x e ◆e = ·λ x (e ◆e)
  (·λ x ·[ t ]₁ e) ◆e = ·λ x ·[ t ◆t ] e
  (·λ x ·[ t ]₂ e) ◆e = ·λ x ·[ t ] (e ◆e)
  (e1 ∘₁ e2) ◆e = (e1 ◆e) ∘ e2
  (e1 ∘₂ e2) ◆e = e1 ∘ (e2 ◆e)
  (e1 ·+₁ e2) ◆e = (e1 ◆e) ·+ e2
  (e1 ·+₂ e2) ◆e = e1 ·+ (e2 ◆e)
  ⦇⌜ e ⌟⦈[ u ] ◆e = ⦇⌜ e ◆e ⌟⦈[ u ]
  (inl e) ◆e = inl (e ◆e)
  (inr e) ◆e = inr (e ◆e)
  (case₁ e x e1 y e2) ◆e = case (e ◆e) x e1 y e2
  (case₂ e x e1 y e2) ◆e = case e x (e1 ◆e) y e2
  (case₃ e x e1 y e2) ◆e = case e x e1 y (e2 ◆e)
  ⟨ e1 , e2 ⟩₁ ◆e = ⟨ e1 ◆e , e2 ⟩
  ⟨ e1 , e2 ⟩₂ ◆e = ⟨ e1 , e2 ◆e ⟩
  fst e ◆e = fst (e ◆e)
  snd e ◆e = snd (e ◆e)

  -- this pair of theorems moves from the judgmental form to the function form
  erase-t◆ : {t : ztyp} {tr : htyp} → (erase-t t tr) → (t ◆t == tr)
  erase-t◆ ETTop = refl
  erase-t◆ (ETArrL p) = ap1 (λ x → x ==> _) (erase-t◆ p)
  erase-t◆ (ETArrR p) = ap1 (λ x → _ ==> x) (erase-t◆ p)
  erase-t◆ (ETPlusL p) = ap1 (λ x → x ⊕ _) (erase-t◆ p)
  erase-t◆ (ETPlusR p) = ap1 (λ x → _ ⊕ x) (erase-t◆ p)
  erase-t◆ (ETProdL p) = ap1 (λ x → x ⊠ _) (erase-t◆ p)
  erase-t◆ (ETProdR p) = ap1 (λ x → _ ⊠ x) (erase-t◆ p)

  erase-e◆ : {e : zexp} {er : hexp} → (erase-e e er) → (e ◆e == er)
  erase-e◆ EETop = refl
  erase-e◆ (EEPlusL p) = ap1 (λ x → x ·+ _) (erase-e◆ p)
  erase-e◆ (EEPlusR p) = ap1 (λ x → _ ·+ x) (erase-e◆ p)
  erase-e◆ (EEAscL p) =  ap1 (λ x → x ·: _) (erase-e◆ p)
  erase-e◆ (EEAscR p) = ap1 (λ x → _ ·: x) (erase-t◆ p)
  erase-e◆ (EELam p) = ap1 (λ x → ·λ _ x) (erase-e◆ p)
  erase-e◆ (EEHalfLamL p) = ap1 (λ x → ·λ _ ·[ x ] _) (erase-t◆ p)
  erase-e◆ (EEHalfLamR p) = ap1 (λ x → ·λ _ ·[ _ ] x) (erase-e◆ p)
  erase-e◆ (EEApL p) = ap1 (λ x → x ∘ _) (erase-e◆ p)
  erase-e◆ (EEApR p) = ap1 (λ x → _ ∘ x) (erase-e◆ p)
  erase-e◆ (EEInl p) = ap1 inl (erase-e◆ p)
  erase-e◆ (EEInr p) = ap1 inr (erase-e◆ p)
  erase-e◆ (EECase1 p) = ap1 (λ x → case x _ _ _ _) (erase-e◆ p)
  erase-e◆ (EECase2 p) = ap1 (λ x → case _ _ x _ _) (erase-e◆ p)
  erase-e◆ (EECase3 p) = ap1 (λ x → case _ _ _ _ x) (erase-e◆ p)
  erase-e◆ (EEPairL p) = ap1 (λ x → ⟨ x , _ ⟩ ) (erase-e◆ p)
  erase-e◆ (EEPairR p) = ap1 (λ x → ⟨ _ , x ⟩ ) (erase-e◆ p)
  erase-e◆ (EEFst p) = ap1 fst (erase-e◆ p)
  erase-e◆ (EESnd p) = ap1 snd (erase-e◆ p)
  erase-e◆ (EENEHole p) = ap1 (λ x → ⦇⌜ x ⌟⦈[ _ ]) (erase-e◆ p)

  -- this pair of theorems moves back from judgmental form to the function form
  ◆erase-t : (t : ztyp) (tr : htyp) → (t ◆t == tr) → (erase-t t tr)
  ◆erase-t ▹ x ◃ .x refl = ETTop
  ◆erase-t (t ==>₁ x) (.(t ◆t) ==> .x) refl with ◆erase-t t (t ◆t) refl
  ... | ih = ETArrL ih
  ◆erase-t (x ==>₂ t) (.x ==> .(t ◆t)) refl with ◆erase-t t (t ◆t) refl
  ... | ih = ETArrR ih
  ◆erase-t (t1 ⊕₁ t2) (.(t1 ◆t) ⊕ .t2) refl = ETPlusL (◆erase-t t1 (t1 ◆t) refl)
  ◆erase-t (t1 ⊕₂ t2) (.t1 ⊕ .(t2 ◆t)) refl = ETPlusR (◆erase-t t2 (t2 ◆t) refl)
  ◆erase-t (t1 ⊠₁ t2) (.(t1 ◆t) ⊠ .t2) refl = ETProdL (◆erase-t t1 (t1 ◆t) refl)
  ◆erase-t (t1 ⊠₂ t2) (.t1 ⊠ .(t2 ◆t)) refl = ETProdR (◆erase-t t2 (t2 ◆t) refl)

  ◆erase-e : (e : zexp) (er : hexp) → (e ◆e == er) → (erase-e e er)
  ◆erase-e ▹ x ◃ .x refl = EETop
  ◆erase-e (e ·:₁ x) .((e ◆e) ·: x) refl with ◆erase-e e (e ◆e) refl
  ... | ih = EEAscL ih
  ◆erase-e (x ·:₂ x₁) .(x ·: (x₁ ◆t)) refl = EEAscR (◆erase-t x₁ (x₁ ◆t) refl)
  ◆erase-e (·λ x e) .(·λ x (e ◆e)) refl = EELam (◆erase-e e (e ◆e) refl)
  ◆erase-e (·λ x ·[ x₁ ]₁ x₂) _ refl = EEHalfLamL (◆erase-t x₁ (x₁ ◆t) refl)
  ◆erase-e (·λ x ·[ x₁ ]₂ e) _ refl = EEHalfLamR (◆erase-e e (e ◆e) refl)
  ◆erase-e (e ∘₁ x) .((e ◆e) ∘ x) refl = EEApL (◆erase-e e (e ◆e) refl)
  ◆erase-e (x ∘₂ e) .(x ∘ (e ◆e)) refl = EEApR (◆erase-e e (e ◆e) refl)
  ◆erase-e (e ·+₁ x) .((e ◆e) ·+ x) refl = EEPlusL (◆erase-e e (e ◆e) refl)
  ◆erase-e (x ·+₂ e) .(x ·+ (e ◆e)) refl = EEPlusR (◆erase-e e (e ◆e) refl)
  ◆erase-e ⦇⌜ e ⌟⦈[ u ] .(⦇⌜ e ◆e ⌟⦈[ u ]) refl = EENEHole (◆erase-e e (e ◆e) refl)
  ◆erase-e (inl e) _ refl = EEInl (◆erase-e e (e ◆e) refl)
  ◆erase-e (inr e) _ refl = EEInr (◆erase-e e (e ◆e) refl)
  ◆erase-e (case₁ e _ _ _ _) _ refl = EECase1 (◆erase-e e (e ◆e) refl)
  ◆erase-e (case₂ _ _ e _ _) _ refl = EECase2 (◆erase-e e (e ◆e) refl)
  ◆erase-e (case₃ _ _ _ _ e) _ refl = EECase3 (◆erase-e e (e ◆e) refl)
  ◆erase-e ⟨ e , x ⟩₁ .(⟨ (e ◆e) , x ⟩) refl = EEPairL (◆erase-e e (e ◆e) refl)
  ◆erase-e ⟨ x , e ⟩₂ .(⟨ x , (e ◆e) ⟩) refl = EEPairR (◆erase-e e (e ◆e) refl)
  ◆erase-e (fst e) _ refl = EEFst (◆erase-e e (e ◆e) refl)
  ◆erase-e (snd e) _ refl = EESnd (◆erase-e e (e ◆e) refl)

  -- jugemental erasure for both types and terms only has one proof for
  -- relating the a term to its non-judgemental erasure
  t-contr : (t : ztyp) → (x y : erase-t t (t ◆t)) → x == y
  t-contr ▹ x ◃ ETTop ETTop = refl
  t-contr (t ==>₁ x) (ETArrL y) (ETArrL z) = ap1 ETArrL (t-contr t y z)
  t-contr (x ==>₂ t) (ETArrR y) (ETArrR z) = ap1 ETArrR (t-contr t y z)
  t-contr (x ⊕₁ x₁) (ETPlusL y) (ETPlusL z) = ap1 ETPlusL (t-contr x y z)
  t-contr (x₁ ⊕₂ x) (ETPlusR y) (ETPlusR z) = ap1 ETPlusR (t-contr x y z)
  t-contr (x ⊠₁ x₁) (ETProdL y) (ETProdL z) = ap1 ETProdL (t-contr x y z)
  t-contr (x₁ ⊠₂ x) (ETProdR y) (ETProdR z) = ap1 ETProdR (t-contr x y z)

  e-contr : (e : zexp) → (x y : erase-e e (e ◆e)) → x == y
  e-contr ▹ x ◃ EETop EETop = refl
  e-contr (e ·:₁ x) (EEAscL x₁) (EEAscL y) = ap1 EEAscL (e-contr e x₁ y)
  e-contr (x₁ ·:₂ x) (EEAscR x₂) (EEAscR x₃) = ap1 EEAscR (t-contr x x₂ x₃)
  e-contr (·λ x e) (EELam x₁) (EELam y) = ap1 EELam (e-contr e x₁ y)
  e-contr (·λ x ·[ x₁ ]₁ x₂) (EEHalfLamL x₃) (EEHalfLamL x₄) = ap1 EEHalfLamL (t-contr x₁ x₃ x₄)
  e-contr (·λ x ·[ x₁ ]₂ x₂) (EEHalfLamR y) (EEHalfLamR z) = ap1 EEHalfLamR (e-contr x₂ y z)
  e-contr (e ∘₁ x) (EEApL x₁) (EEApL y) = ap1 EEApL (e-contr e x₁ y)
  e-contr (x ∘₂ e) (EEApR x₁) (EEApR y) = ap1 EEApR (e-contr e x₁ y)
  e-contr (e ·+₁ x) (EEPlusL x₁) (EEPlusL y) = ap1 EEPlusL (e-contr e x₁ y)
  e-contr (x ·+₂ e) (EEPlusR x₁) (EEPlusR y) = ap1 EEPlusR (e-contr e x₁ y)
  e-contr ⦇⌜ e ⌟⦈[ u ] (EENEHole x) (EENEHole y) = ap1 EENEHole (e-contr e x y)
  e-contr (inl x) (EEInl y) (EEInl z) = ap1 EEInl (e-contr x y z)
  e-contr (inr x) (EEInr y) (EEInr z) = ap1 EEInr (e-contr x y z)
  e-contr (case₁ x x₁ x₂ x₃ x₄) (EECase1 y) (EECase1 z) = ap1 EECase1 (e-contr x y z)
  e-contr (case₂ x₁ x₂ x x₃ x₄) (EECase2 y) (EECase2 z) = ap1 EECase2 (e-contr x y z)
  e-contr (case₃ x₁ x₂ x₃ x₄ x) (EECase3 y) (EECase3 z) = ap1 EECase3 (e-contr x y z)
  e-contr ⟨ e , x ⟩₁ (EEPairL x₁) (EEPairL y) = ap1 EEPairL (e-contr e x₁ y)
  e-contr ⟨ x , e ⟩₂ (EEPairR x₁) (EEPairR y) = ap1 EEPairR (e-contr e x₁ y)
  e-contr (fst x) (EEFst y) (EEFst z) = ap1 EEFst (e-contr x y z)
  e-contr (snd x) (EESnd y) (EESnd z) = ap1 EESnd (e-contr x y z)

  -- taken together, these four theorems demonstrate that both round-trips
  -- of the above functions are stable up to ==
  erase-trt1 : (t : ztyp) (tr : htyp) →
               (x : t ◆t == tr) →
               (erase-t◆ (◆erase-t t tr x)) == x
  erase-trt1 ▹ x ◃ .x refl = refl
  erase-trt1 (t ==>₁ x) (.(t ◆t) ==> .x) refl with erase-t◆ (◆erase-t t (t ◆t) refl)
  erase-trt1 (t ==>₁ x) (.(t ◆t) ==> .x) refl | refl = refl
  erase-trt1 (x ==>₂ t) (.x ==> .(t ◆t)) refl with erase-t◆ (◆erase-t t (t ◆t) refl)
  erase-trt1 (x ==>₂ t) (.x ==> .(t ◆t)) refl | refl = refl
  erase-trt1 (x ⊕₁ x₁) .((x ◆t) ⊕ x₁) refl with erase-t◆ (◆erase-t x (x ◆t) refl)
  erase-trt1 (x ⊕₁ x₁) .((x ◆t) ⊕ x₁) refl | refl = refl
  erase-trt1 (x ⊕₂ x₁) .(x ⊕ (x₁ ◆t)) refl with erase-t◆ (◆erase-t x₁ (x₁ ◆t) refl)
  erase-trt1 (x ⊕₂ x₁) .(x ⊕ (x₁ ◆t)) refl | refl = refl
  erase-trt1 (x ⊠₁ x₁) .((x ◆t) ⊠ x₁) refl with erase-t◆ (◆erase-t x (x ◆t) refl)
  erase-trt1 (x ⊠₁ x₁) .((x ◆t) ⊠ x₁) refl | refl = refl
  erase-trt1 (x ⊠₂ x₁) .(x ⊠ (x₁ ◆t)) refl with erase-t◆ (◆erase-t x₁ (x₁ ◆t) refl)
  erase-trt1 (x ⊠₂ x₁) .(x ⊠ (x₁ ◆t)) refl | refl = refl

  erase-trt2 : (t : ztyp) (tr : htyp) →
               (x : erase-t t tr) →
               ◆erase-t t tr (erase-t◆ x) == x
  erase-trt2 .(▹ tr ◃) tr ETTop = refl
  erase-trt2 _ _ (ETArrL ETTop) = refl
  erase-trt2 (t1 ==>₁ t2) _ (ETArrL x) with erase-t◆ x
  erase-trt2 (t1 ==>₁ t2) _ (ETArrL x) | refl =
    ap1 ETArrL (t-contr _ (◆erase-t t1 (t1 ◆t) refl) x)
  erase-trt2 (t1 ==>₂ t2) _ (ETArrR x) with erase-t◆ x
  erase-trt2 (t1 ==>₂ t2) _ (ETArrR x) | refl =
    ap1 ETArrR (t-contr _ (◆erase-t t2 (t2 ◆t) refl) x)
  erase-trt2 (t1 ⊕₁ t2) _ (ETPlusL x) with erase-t◆ x
  erase-trt2 (t1 ⊕₁ t2) _ (ETPlusL x) | refl =
    ap1 ETPlusL (t-contr _ (◆erase-t t1 (t1 ◆t) refl) x)
  erase-trt2 (t1 ⊕₂ t2) _ (ETPlusR x) with erase-t◆ x
  erase-trt2 (t1 ⊕₂ t2) _ (ETPlusR x) | refl =
    ap1 ETPlusR (t-contr _ (◆erase-t t2 (t2 ◆t) refl) x)
  erase-trt2 (t1 ⊠₁ t2) _ (ETProdL x) with erase-t◆ x
  erase-trt2 (t1 ⊠₁ t2) _ (ETProdL x) | refl =
    ap1 ETProdL (t-contr _ (◆erase-t t1 (t1 ◆t) refl) x)
  erase-trt2 (t1 ⊠₂ t2) _ (ETProdR x) with erase-t◆ x
  erase-trt2 (t1 ⊠₂ t2) _ (ETProdR x) | refl =
    ap1 ETProdR (t-contr _ (◆erase-t t2 (t2 ◆t) refl) x)

  erase-ert1 : (e : zexp) (er : hexp) →
               (x : e ◆e == er) →
               (erase-e◆ (◆erase-e e er x)) == x
  erase-ert1 ▹ x ◃ .x refl = refl
  erase-ert1 (e ·:₁ x) .((e ◆e) ·: x) refl with erase-e◆ (◆erase-e e (e ◆e) refl)
  erase-ert1 (e ·:₁ x) .((e ◆e) ·: x) refl | refl = refl
  erase-ert1 (x ·:₂ t) .(x ·: (t ◆t)) refl = ap1 (λ a → ap1 (_·:_ x) a) (erase-trt1 t _ refl)
  erase-ert1 (·λ x e) .(·λ x (e ◆e)) refl = ap1 (λ a → ap1 (·λ x) a) (erase-ert1 e _ refl)
  erase-ert1 (·λ x ·[ t ]₁ e) .((·λ x ·[ t ]₁ e) ◆e) refl =
    ap1 (λ a → ap1 (λ b → ·λ x ·[ b ] e) a) (erase-trt1 t _ refl)
  erase-ert1 (·λ x ·[ t ]₂ e) .((·λ x ·[ t ]₂ e) ◆e) refl =
    ap1 (λ a → ap1 (λ b → ·λ x ·[ t ] b) a) (erase-ert1 e _ refl)
  erase-ert1 (e ∘₁ x) .((e ◆e) ∘ x) refl =
    ap1 (λ a → ap1 (λ x₁ → x₁ ∘ x) a) (erase-ert1 e _ refl)
  erase-ert1 (x ∘₂ e) .(x ∘ (e ◆e)) refl =
    ap1 (λ a → ap1 (_∘_ x) a) (erase-ert1 e _ refl)
  erase-ert1 (e ·+₁ x) .((e ◆e) ·+ x) refl =
    ap1 (λ a → ap1 (λ x₁ → x₁ ·+ x) a) (erase-ert1 e _ refl)
  erase-ert1 (x ·+₂ e) .(x ·+ (e ◆e)) refl =
    ap1 (λ a → ap1 (_·+_ x) a) (erase-ert1 e _ refl)
  erase-ert1 ⦇⌜ e ⌟⦈[ u ] .(⦇⌜ e ◆e ⌟⦈[ u ]) refl =
    ap1 (λ a → ap1 ⦇⌜_⌟⦈[ u ] a) (erase-ert1 e _ refl)
  erase-ert1 (inl x) .(inl (x ◆e)) refl = ap1 (λ a → ap1 inl a) (erase-ert1 x _ refl)
  erase-ert1 (inr x) .(inr (x ◆e)) refl = ap1 (λ a → ap1 inr a) (erase-ert1 x _ refl)
  erase-ert1 (case₁ x x₁ x₂ x₃ x₄) .(case (x ◆e) x₁ x₂ x₃ x₄) refl =
    ap1 (ap1 (λ a → case a x₁ x₂ x₃ x₄)) (erase-ert1 x _ refl)
  erase-ert1 (case₂ x x₁ x₂ x₃ x₄) .(case x x₁ (x₂ ◆e) x₃ x₄) refl =
    ap1 (ap1 (λ a → case x x₁ a x₃ x₄)) (erase-ert1 x₂ _ refl)
  erase-ert1 (case₃ x x₁ x₂ x₃ x₄) .(case x x₁ x₂ x₃ (x₄ ◆e)) refl =
    ap1 (ap1 (λ a → case x x₁ x₂ x₃ a)) (erase-ert1 x₄ _ refl)
  erase-ert1 ⟨ e , x ⟩₁ .(⟨ (e ◆e) , x ⟩) refl =
    ap1 (λ a → ap1 (λ x₁ → ⟨ x₁ , x ⟩) a) (erase-ert1 e _ refl)
  erase-ert1 ⟨ x , e ⟩₂ .(⟨ x , (e ◆e) ⟩) refl =
    ap1 (λ a → ap1 (⟨_,_⟩ x) a) (erase-ert1 e _ refl)
  erase-ert1 (fst x) .(fst (x ◆e)) refl = ap1 (λ a → ap1 fst a) (erase-ert1 x _ refl)
  erase-ert1 (snd x) .(snd (x ◆e)) refl = ap1 (λ a → ap1 snd a) (erase-ert1 x _ refl)

  erase-ert2 : (e : zexp) (er : hexp) →
               (b : erase-e e er) →
               ◆erase-e e er (erase-e◆ b) == b
  erase-ert2 .(▹ er ◃) er EETop = refl
  erase-ert2 (e ·:₁ x) _ (EEAscL b) with erase-e◆ b
  erase-ert2 (e ·:₁ x) _ (EEAscL b) | refl =
    ap1 EEAscL (e-contr _ (◆erase-e e (e ◆e) refl) b)
  erase-ert2 (e ·:₂ x) _ (EEAscR b) with erase-t◆ b
  erase-ert2 (e ·:₂ x) .(e ·: (x ◆t)) (EEAscR b) | refl =
    ap1 EEAscR (t-contr _ (◆erase-t x (x ◆t) refl) b)
  erase-ert2 (·λ x e) _ (EELam b) with erase-e◆ b
  erase-ert2 (·λ x e) .(·λ x (e ◆e)) (EELam b) | refl =
    ap1 EELam (e-contr _ (◆erase-e e (e ◆e) refl) b)
  erase-ert2 (·λ x ·[ t ]₁ e) _ (EEHalfLamL b) with erase-t◆ b
  erase-ert2 (·λ x ·[ t ]₁ e) .(·λ x ·[ t ◆t ] e) (EEHalfLamL b) | refl =
    ap1 EEHalfLamL (t-contr _ (◆erase-t t (t ◆t) refl) b)
  erase-ert2 (·λ x ·[ t ]₂ e) _ (EEHalfLamR b) with erase-e◆ b
  erase-ert2 (·λ x ·[ t ]₂ e) .(·λ x ·[ t ] (e ◆e)) (EEHalfLamR b) | refl =
    ap1 EEHalfLamR (e-contr _ (◆erase-e e (e ◆e) refl) b)
  erase-ert2 (e ∘₁ x) _ (EEApL b) with erase-e◆ b
  erase-ert2 (e ∘₁ x) .((e ◆e) ∘ x) (EEApL b) | refl =
    ap1 EEApL (e-contr e (◆erase-e e (e ◆e) refl) b)
  erase-ert2 (e1 ∘₂ e) _ (EEApR b) with erase-e◆ b
  erase-ert2 (e1 ∘₂ e) .(e1 ∘ (e ◆e)) (EEApR b) | refl =
    ap1 EEApR (e-contr e (◆erase-e e (e ◆e) refl) b)
  erase-ert2 (e ·+₁ x) _ (EEPlusL b) with erase-e◆ b
  erase-ert2 (e ·+₁ x) .((e ◆e) ·+ x) (EEPlusL b) | refl =
    ap1 EEPlusL (e-contr e (◆erase-e e (e ◆e) refl) b)
  erase-ert2 (e1 ·+₂ e) _ (EEPlusR b) with erase-e◆ b
  erase-ert2 (e1 ·+₂ e) .(e1 ·+ (e ◆e)) (EEPlusR b) | refl =
    ap1 EEPlusR (e-contr e (◆erase-e e (e ◆e) refl) b)
  erase-ert2 ⦇⌜ e ⌟⦈[ u ] _ (EENEHole b) with erase-e◆ b
  erase-ert2 ⦇⌜ e ⌟⦈[ u ] .(⦇⌜ e ◆e ⌟⦈[ u ]) (EENEHole b) | refl =
    ap1 EENEHole (e-contr e (◆erase-e e (e ◆e) refl) b)
  erase-ert2 (inl x) _ (EEInl z) with erase-e◆ z
  erase-ert2 (inl x) .(inl (x ◆e)) (EEInl z) | refl = ap1 EEInl (e-contr x _ z)
  erase-ert2 (inr x) _ (EEInr z) with erase-e◆ z
  erase-ert2 (inr x) .(inr (x ◆e)) (EEInr z) | refl = ap1 EEInr (e-contr x _ z)
  erase-ert2 (case₁ x x₁ x₂ x₃ x₄) _ (EECase1 z) with erase-e◆ z
  erase-ert2 (case₁ x x₁ x₂ x₃ x₄) .(case (x ◆e) x₁ x₂ x₃ x₄) (EECase1 z) | refl =
    ap1 EECase1 (e-contr x _ z)
  erase-ert2 (case₂ e x₁ x₂ x₃ x₄) _ (EECase2 z) with erase-e◆ z
  erase-ert2 (case₂ e x₁ x₂ x₃ x₄) .(case e x₁ (x₂ ◆e) x₃ x₄) (EECase2 z) | refl =
    ap1 EECase2 (e-contr x₂ _ z)
  erase-ert2 (case₃ e x₁ x₂ x₃ x₄) _ (EECase3 z) with erase-e◆ z
  erase-ert2 (case₃ e x₁ x₂ x₃ x₄) .(case e x₁ x₂ x₃ (x₄ ◆e)) (EECase3 z) | refl =
    ap1 EECase3 (e-contr x₄ _ z)
  erase-ert2 ⟨ e , x ⟩₁ _ (EEPairL b) with erase-e◆ b
  erase-ert2 ⟨ e , x ⟩₁ .(⟨ (e ◆e) , x ⟩) (EEPairL b) | refl =
    ap1 EEPairL (e-contr e (◆erase-e e (e ◆e) refl) b)
  erase-ert2 ⟨ e1 , e ⟩₂ _ (EEPairR b) with erase-e◆ b
  erase-ert2 ⟨ e1 , e ⟩₂ .(⟨ e1 , (e ◆e) ⟩) (EEPairR b) | refl =
    ap1 EEPairR (e-contr e (◆erase-e e (e ◆e) refl) b)
  erase-ert2 (fst x) _ (EEFst z) with erase-e◆ z
  erase-ert2 (fst x) .(fst (x ◆e)) (EEFst z) | refl = ap1 EEFst (e-contr x _ z)
  erase-ert2 (snd x) _ (EESnd z) with erase-e◆ z
  erase-ert2 (snd x) .(snd (x ◆e)) (EESnd z) | refl = ap1 EESnd (e-contr x _ z)

  -- since both round trips are stable, these functions demonstrate
  -- isomorphisms between the jugemental and non-judgemental definitions of
  -- erasure
  erase-e-iso : (e : zexp) (er : hexp) → (e ◆e == er) ≃ (erase-e e er)
  erase-e-iso e er = (◆erase-e e er) , (erase-e◆ , erase-ert1 e er , erase-ert2 e er)

  erase-t-iso : (t : ztyp) (tr : htyp) → (t ◆t == tr) ≃ (erase-t t tr)
  erase-t-iso t tr = (◆erase-t t tr) , (erase-t◆ , erase-trt1 t tr , erase-trt2 t tr)

  -- this isomorphism supplies the argument that the judgement has mode (∀,
  -- !∃), where uniqueness comes from erase-e◆.
  erase-e-mode : (e : zexp) → Σ[ er ∈ hexp ] (erase-e e er)
  erase-e-mode e = (e ◆e) , (◆erase-e e (e ◆e) refl)

  -- some translations and lemmas to move between the different
  -- forms. these are not needed to show that this is an ok encoding pair,
  -- but they are helpful when actually using it.

  -- even more specifically, the relation relates an expression to its
  -- functional erasure.
  rel◆t : (t : ztyp) → (erase-t t (t ◆t))
  rel◆t t = ◆erase-t t (t ◆t) refl

  rel◆ : (e : zexp) → (erase-e e (e ◆e))
  rel◆ e = ◆erase-e e (e ◆e) refl

  lem-erase-synth : ∀{e e' Γ t} → erase-e e e' → Γ ⊢ e' => t → Γ ⊢ (e ◆e) => t
  lem-erase-synth er wt = tr (λ x → _ ⊢ x => _) (! (erase-e◆ er)) wt

  lem-erase-ana : ∀{e e' Γ t} → erase-e e e' → Γ ⊢ e' <= t → Γ ⊢ (e ◆e) <= t
  lem-erase-ana er wt = tr (λ x → _ ⊢ x <= _) (! (erase-e◆ er)) wt

  lem-synth-erase : ∀{Γ e t e' } → Γ ⊢ e ◆e => t → erase-e e e' → Γ ⊢ e' => t
  lem-synth-erase d1 d2 with erase-e◆ d2
  ... | refl = d1

  eraset-det : ∀{t t' t''} → erase-t t t' → erase-t t t'' → t' == t''
  eraset-det e1 e2 with erase-t◆ e1
  ... | refl = erase-t◆ e2

  erasee-det : ∀{e e' e''} → erase-e e e' → erase-e e e'' → e' == e''
  erasee-det e1 e2 with erase-e◆ e1
  ... | refl = erase-e◆ e2

  erase-in-hole : ∀ {e e' u} → erase-e e e' → erase-e ⦇⌜ e ⌟⦈[ u ] ⦇⌜ e' ⌟⦈[ u ]
  erase-in-hole (EENEHole er) = EENEHole (erase-in-hole er)
  erase-in-hole x = EENEHole x

  eq-er-trans : ∀{e e◆ e'} →
                (e ◆e) == (e' ◆e) →
                erase-e e e◆ →
                erase-e e' e◆
  eq-er-trans {e} {e◆} {e'} eq er =
    tr (λ f → erase-e e' f) (erasee-det (◆erase-e e (e' ◆e) eq) er) (rel◆ e')

  eq-ert-trans : ∀{t t' t1 t2} →
                 (t ◆t) == (t' ◆t) →
                 erase-t t t1 →
                 erase-t t' t2 →
                 t1 == t2
  eq-ert-trans eq er1 er2 = ! (erase-t◆ er1) · (eq · (erase-t◆ er2))

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
{-# OPTIONS --rewriting #-}

module Issue2792 where

open import Issue2792.Safe


text:
------------------------------------------------------------------------
-- Equivalences with erased "proofs"
------------------------------------------------------------------------

-- This module contains some basic definitions with few dependencies.
-- See Equivalence.Erased for more definitions. The definitions below
-- are reexported from Equivalence.Erased.

{-# OPTIONS --without-K --safe #-}

open import Equality

module Equivalence.Erased.Basics
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open Derived-definitions-and-properties eq
open import Logical-equivalence using (_⇔_)
open import Prelude as P hiding (id; [_,_]) renaming (_∘_ to _⊚_)

open import Equivalence eq as Eq using (_≃_; Is-equivalence)
import Equivalence.Half-adjoint eq as HA
open import Erased.Basics
open import Preimage eq as Preimage using (_⁻¹_)

private
  variable
    a b c d ℓ : Level
    A B C     : Type a
    p x y     : A
    P Q       : A → Type p
    f g       : (x : A) → P x

------------------------------------------------------------------------
-- Is-equivalenceᴱ

-- Is-equivalence with erased proofs.

Is-equivalenceᴱ : {A : Type a} {B : Type b} → @0 (A → B) → Type (a ⊔ b)
Is-equivalenceᴱ {A = A} {B = B} f =
  ∃ λ (f⁻¹ : B → A) → Erased (HA.Proofs f f⁻¹)

------------------------------------------------------------------------
-- Some conversion lemmas

-- Conversions between Is-equivalence and Is-equivalenceᴱ.

Is-equivalence→Is-equivalenceᴱ :
  {@0 A : Type a} {@0 B : Type b} {@0 f : A → B} →
  Is-equivalence f → Is-equivalenceᴱ f
Is-equivalence→Is-equivalenceᴱ = Σ-map P.id [_]→

@0 Is-equivalenceᴱ→Is-equivalence :
  Is-equivalenceᴱ f → Is-equivalence f
Is-equivalenceᴱ→Is-equivalence = Σ-map P.id erased

-- See also Equivalence.Erased.Is-equivalence≃Is-equivalenceᴱ.

------------------------------------------------------------------------
-- _≃ᴱ_

private
 module Dummy where

  -- Equivalences with erased proofs.

  infix 4 _≃ᴱ_

  record _≃ᴱ_ (A : Type a) (B : Type b) : Type (a ⊔ b) where
    constructor ⟨_,_⟩
    field
      to             : A → B
      is-equivalence : Is-equivalenceᴱ to

open Dummy public using (_≃ᴱ_; ⟨_,_⟩) hiding (module _≃ᴱ_)

-- A variant of the constructor of _≃ᴱ_ with erased type arguments.

⟨_,_⟩₀ :
  {@0 A : Type a} {@0 B : Type b}
  (to : A → B) → Is-equivalenceᴱ to → A ≃ᴱ B
⟨ to , eq ⟩₀ = ⟨ to , eq ⟩

-- Note that the type arguments A and B are erased. This is not the
-- case for the record module Dummy._≃ᴱ_.

module _≃ᴱ_ {@0 A : Type a} {@0 B : Type b} (A≃B : A ≃ᴱ B) where

  -- The "left-to-right" direction of the equivalence.

  to : A → B
  to = let ⟨ to , _ ⟩ = A≃B in to

  -- The function to is an equivalence.

  is-equivalence : Is-equivalenceᴱ to
  is-equivalence = let ⟨ _ , eq ⟩ = A≃B in eq

  -- The "right-to-left" direction of the equivalence.

  from : B → A
  from = let from , _ = is-equivalence in from

  -- The underlying logical equivalence.

  logical-equivalence : A ⇔ B
  logical-equivalence = record
    { to   = to
    ; from = from
    }

  -- In an erased context one can construct a corresponding
  -- equivalence.

  @0 equivalence : A ≃ B
  equivalence =
    Eq.⟨ to , Is-equivalenceᴱ→Is-equivalence is-equivalence ⟩

  -- In an erased context the function from is a right inverse of to.

  @0 right-inverse-of : ∀ y → to (from y) ≡ y
  right-inverse-of = _≃_.right-inverse-of equivalence

  -- In an erased context the function from is a left inverse of to.

  @0 left-inverse-of : ∀ x → from (to x) ≡ x
  left-inverse-of = _≃_.left-inverse-of equivalence

  -- Two coherence properties.

  @0 left-right-lemma :
    ∀ x → cong to (left-inverse-of x) ≡ right-inverse-of (to x)
  left-right-lemma = _≃_.left-right-lemma equivalence

  @0 right-left-lemma :
    ∀ x → cong from (right-inverse-of x) ≡ left-inverse-of (from x)
  right-left-lemma = _≃_.right-left-lemma equivalence

private
  variable
    A≃B : A ≃ᴱ B

------------------------------------------------------------------------
-- More conversion lemmas

-- Equivalences are equivalent to pairs.

≃ᴱ-as-Σ : (A ≃ᴱ B) ≃ (∃ λ (f : A → B) → Is-equivalenceᴱ f)
≃ᴱ-as-Σ = Eq.↔⇒≃ (record
  { surjection = record
    { logical-equivalence = record
      { to   = λ { ⟨ f , is ⟩ → f , is }
      ; from = uncurry ⟨_,_⟩
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = refl
  })

-- Conversions between _≃_ and _≃ᴱ_.

≃→≃ᴱ :
  {@0 A : Type a} {@0 B : Type b} →
  A ≃ B → A ≃ᴱ B
≃→≃ᴱ Eq.⟨ f , is-equiv ⟩ =
  ⟨ f , Is-equivalence→Is-equivalenceᴱ is-equiv ⟩

@0 ≃ᴱ→≃ : A ≃ᴱ B → A ≃ B
≃ᴱ→≃ = _≃ᴱ_.equivalence

-- Data corresponding to the erased proofs of an equivalence with
-- erased proofs.

record Erased-proofs {A : Type a} {B : Type b}
                     (to : A → B) (from : B → A) : Type (a ⊔ b) where
  field
    proofs : HA.Proofs to from

-- Extracts "erased proofs" from a regular equivalence.

[proofs] :
  {@0 A : Type a} {@0 B : Type b}
  (A≃B : A ≃ B) → Erased-proofs (_≃_.to A≃B) (_≃_.from A≃B)
[proofs] A≃B .Erased-proofs.proofs =
  let record { is-equivalence = is-equivalence } = A≃B in
  proj₂₀ is-equivalence

-- Converts two functions and some erased proofs to an equivalence
-- with erased proofs.
--
-- Note that Agda can in many cases infer "to" and "from" from the
-- first explicit argument, see (for instance) ↔→≃ᴱ below.

[≃]→≃ᴱ :
  {@0 A : Type a} {@0 B : Type b} {to : A → B} {from : B → A} →
  @0 Erased-proofs to from →
  A ≃ᴱ B
[≃]→≃ᴱ {to = to} {from = from} ep =
  ⟨ to , (from , [ ep .Erased-proofs.proofs ]) ⟩

-- A function with a quasi-inverse with erased proofs can be turned
-- into an equivalence with erased proofs.

↔→≃ᴱ :
  {@0 A : Type a} {@0 B : Type b}
  (f : A → B) (g : B → A) →
  @0 (∀ x → f (g x) ≡ x) →
  @0 (∀ x → g (f x) ≡ x) →
  A ≃ᴱ B
↔→≃ᴱ {A = A} {B = B} f g f∘g g∘f = [≃]→≃ᴱ ([proofs] A≃B′)
  where
  @0 A≃B′ : A ≃ B
  A≃B′ = Eq.↔⇒≃ (record
    { surjection = record
      { logical-equivalence = record
        { to   = f
        ; from = g
        }
      ; right-inverse-of = f∘g
      }
    ; left-inverse-of = g∘f
    })

-- A variant of ↔→≃ᴱ.

⇔→≃ᴱ :
  {@0 A : Type a} {@0 B : Type b} →
  @0 Is-proposition A → @0 Is-proposition B →
  (A → B) → (B → A) →
  A ≃ᴱ B
⇔→≃ᴱ A-prop B-prop to from =
  [≃]→≃ᴱ ([proofs] (Eq.⇔→≃ A-prop B-prop to from))

------------------------------------------------------------------------
-- Equivalences with erased proofs form an equivalence relation

-- Identity.

id : {@0 A : Type a} → A ≃ᴱ A
id = [≃]→≃ᴱ ([proofs] Eq.id)

-- Inverse.

inverse :
  {@0 A : Type a} {@0 B : Type b} →
  A ≃ᴱ B → B ≃ᴱ A
inverse A≃B = [≃]→≃ᴱ ([proofs] (Eq.inverse (≃ᴱ→≃ A≃B)))

-- Composition.

infixr 9 _∘_

_∘_ :
  {@0 A : Type a} {@0 B : Type b} {@0 C : Type c} →
  B ≃ᴱ C → A ≃ᴱ B → A ≃ᴱ C
f ∘ g = [≃]→≃ᴱ ([proofs] (≃ᴱ→≃ f Eq.∘ ≃ᴱ→≃ g))

------------------------------------------------------------------------
-- A preservation lemma

-- Is-equivalenceᴱ f is logically equivalent to Is-equivalenceᴱ g if f
-- and g are pointwise equal.
--
-- See also Equivalence.Erased.[]-cong₂-⊔.Is-equivalenceᴱ-cong.

Is-equivalenceᴱ-cong-⇔ :
  {@0 A : Type a} {@0 B : Type b} {@0 f g : A → B} →
  @0 (∀ x → f x ≡ g x) →
  Is-equivalenceᴱ f ⇔ Is-equivalenceᴱ g
Is-equivalenceᴱ-cong-⇔ {f = f} {g = g} f≡g =
  record { to = to f≡g; from = to (sym ⊚ f≡g) }
  where
  to :
    {@0 A : Type a} {@0 B : Type b} {@0 f g : A → B} →
    @0 (∀ x → f x ≡ g x) →
    Is-equivalenceᴱ f → Is-equivalenceᴱ g
  to f≡g f-eq@(f⁻¹ , _) =
    ( f⁻¹
    , [ erased $ proj₂ $
        Is-equivalence→Is-equivalenceᴱ $
        Eq.respects-extensional-equality f≡g $
        Is-equivalenceᴱ→Is-equivalence f-eq
      ]
    )

----------------------------------------------------------------------
-- The left-to-right and right-to-left components of an equivalence
-- with erased proofs can be replaced with extensionally equal
-- functions

-- The forward direction of an equivalence with erased proofs can be
-- replaced by an extensionally equal function.

with-other-function :
  {@0 A : Type a} {@0 B : Type b}
  (A≃B : A ≃ᴱ B) (f : A → B) →
  @0 (∀ x → _≃ᴱ_.to A≃B x ≡ f x) →
  A ≃ᴱ B
with-other-function ⟨ g , is-equivalence ⟩ f g≡f =
  ⟨ f
  , (let record { to = to } = Is-equivalenceᴱ-cong-⇔ g≡f in
     to is-equivalence)
  ⟩₀

_ : _≃ᴱ_.to (with-other-function A≃B f p) ≡ f
_ = refl _

_ : _≃ᴱ_.from (with-other-function A≃B f p) ≡ _≃ᴱ_.from A≃B
_ = refl _

-- The same applies to the other direction.

with-other-inverse :
  {@0 A : Type a} {@0 B : Type b}
  (A≃B : A ≃ᴱ B) (g : B → A) →
  @0 (∀ x → _≃ᴱ_.from A≃B x ≡ g x) →
  A ≃ᴱ B
with-other-inverse A≃B g ≡g =
  inverse $ with-other-function (inverse A≃B) g ≡g

_ : _≃ᴱ_.from (with-other-inverse A≃B g p) ≡ g
_ = refl _

_ : _≃ᴱ_.to (with-other-inverse A≃B f p) ≡ _≃ᴱ_.to A≃B
_ = refl _

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
-- 2012-03-08 Andreas
module NoTerminationCheck4 where

data Bool : Set where
  true false : Bool

{-# NON_TERMINATING #-}
private
  f : Bool -> Bool
  f true = f true
  f false = f false

-- error: must place pragma before f