text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Modalities.Modality where

{-
  translated from
  https://github.com/HoTT/HoTT-Agda/blob/master/core/lib/types/Modality.agda
-}

open import Cubical.Core.Everything
open import Cubical.Foundations.Everything

record Modality ℓ : Type (ℓ-suc ℓ) where
  field
    isModal : Type ℓ → Type ℓ
    isModalIsProp : {A : Type ℓ} → isProp (isModal A)

    ◯ : Type ℓ → Type ℓ                                  -- \ciO
    ◯-isModal : {A : Type ℓ} → isModal (◯ A)

    η : {A : Type ℓ} → A → ◯ A

    ◯-elim : {A : Type ℓ} {B : ◯ A → Type ℓ}
      (B-modal : (x : ◯ A) → isModal (B x))
      → ((x : A) → (B (η x))) → ((x : ◯ A) → B x)

    ◯-elim-β : {A : Type ℓ} {B : ◯ A → Type ℓ}
      (B-modal : (x : ◯ A) → isModal (B x)) (f : (x : A) → (B (η x)))
      → (a : A) → ◯-elim B-modal f (η a) ≡ f a

    ◯-=-isModal : {A : Type ℓ} (x y : ◯ A) → isModal (x ≡ y)

  ◯-Types : Type (ℓ-suc ℓ)
  ◯-Types = Σ[ A ∈ Type ℓ ] isModal A

  {- elimination rules -}

  module ◯Elim {A : Type ℓ} {B : ◯ A → Type ℓ}
    (B-modal : (x : ◯ A) → isModal (B x)) (η* : (x : A) → (B (η x))) where
      f : (x : ◯ A) → B x
      f = ◯-elim B-modal η*
      η-β : (a : A) → ◯-elim B-modal η* (η a) ≡ η* a
      η-β = ◯-elim-β B-modal η*

  module ◯Rec {A : Type ℓ} {B : Type ℓ}
         (B-modal : isModal B) (η* : A → B)
      = ◯Elim (λ _ → B-modal) η*

  ◯-rec = ◯Rec.f
  ◯-rec-β = ◯Rec.η-β

  {- functoriality -}

  module ◯Fmap {A B : Type ℓ} (f : A → B) =
      ◯Rec ◯-isModal (η ∘ f)

  ◯-map = ◯Fmap.f
  ◯-map-β = ◯Fmap.η-β

  ◯-preservesEquiv : {A B : Type ℓ} (f : A → B) → isEquiv f → isEquiv (◯-map f)
  ◯-preservesEquiv f f-ise = isoToIsEquiv (iso _ (◯-map inv) to-from from-to) where
    open Iso (equivToIso (f , f-ise))
    abstract
      to-from : ∀ ◯b → ◯-map f (◯-map inv ◯b) ≡ ◯b
      to-from = ◯-elim
        (λ ◯b → ◯-=-isModal (◯-map f (◯-map inv ◯b)) ◯b)
        (λ b → cong (◯-map f) (◯-map-β inv b) ∙ ◯-map-β f (inv b) ∙ cong η (rightInv b))
      from-to : ∀ ◯a → ◯-map inv (◯-map f ◯a) ≡ ◯a
      from-to = ◯-elim
          (λ ◯a → ◯-=-isModal (◯-map inv (◯-map f ◯a)) ◯a)
          (λ a → cong (◯-map inv) (◯-map-β f a) ∙ ◯-map-β inv (f a) ∙ cong η (leftInv a))

  ◯-equiv : {A B : Type ℓ} → A ≃ B → ◯ A ≃ ◯ B
  ◯-equiv (f , f-ise) = ◯-map f , ◯-preservesEquiv f f-ise

  {- equivalences preserve being modal -}

  equivPreservesIsModal : {A B : Type ℓ} → A ≃ B → isModal A → isModal B
  equivPreservesIsModal eq = fst (pathToEquiv (cong isModal (ua eq)))

  {- modal types and [η] being an equivalence -}

  isModalToIsEquiv : {A : Type ℓ} → isModal A → isEquiv (η {A})
  isModalToIsEquiv {A} w =  isoToIsEquiv (iso (η {A}) η-inv inv-l inv-r)
       where η-inv : ◯ A → A
             η-inv = ◯-rec w (idfun A)

             abstract
               inv-r : (a : A) → η-inv (η a) ≡ a
               inv-r = ◯-rec-β w (idfun A)

               inv-l : (a : ◯ A) → η (η-inv a) ≡ a
               inv-l = ◯-elim (λ a₀ → ◯-=-isModal _ _)
                              (λ a₀ → cong η (inv-r a₀))

  abstract
    isEquivToIsModal : {A : Type ℓ} → isEquiv (η {A}) → isModal A
    isEquivToIsModal {A} eq = equivPreservesIsModal (invEquiv (η , eq)) ◯-isModal

    retractIsModal : {A B : Type ℓ} (w : isModal A)
        (f : A → B) (g : B → A) (r : (b : B) → f (g b) ≡ b) →
        isModal B
    retractIsModal {A} {B} w f g r =
      isEquivToIsModal
        (isoToIsEquiv (iso η η-inv inv-l inv-r))
      where η-inv : ◯ B → B
            η-inv = f ∘ (◯-rec w g)

            inv-r : (b : B) → η-inv (η b) ≡ b
            inv-r b = cong f (◯-rec-β w g b) ∙ r b

            inv-l : (b : ◯ B) → η (η-inv b) ≡ b
            inv-l = ◯-elim (λ b → ◯-=-isModal _ _) (λ b → cong η (inv-r b))

  {- function types with modal codomain are modal -}

  abstract
    Π-isModal : {A : Type ℓ} {B : A → Type ℓ}
              (w : (a : A) → isModal (B a)) → isModal ((x : A) → B x)
    Π-isModal {A} {B} w = retractIsModal {◯ _} {(x : A) → B x} ◯-isModal η-inv η r

        where η-inv : ◯ ((x : A) → B x) → (x : A) → B x
              η-inv φ' a = ◯-rec (w a) (λ φ → φ a) φ'

              r : (φ : (x : A) →  B x) → η-inv (η φ) ≡ φ
              r φ = funExt (λ a → ◯-rec-β (w a) (λ φ₀ → φ₀ a) φ)

    →-isModal : {A B : Type ℓ} → isModal B → isModal (A → B)
    →-isModal w = Π-isModal (λ _ → w)

  {- sigma types of a modal dependent type with modal base are modal -}

  abstract
    Σ-isModal : {A : Type ℓ} (B : A → Type ℓ)
      → isModal A → ((a : A) → isModal (B a))
      → isModal (Σ A B)
    Σ-isModal {A} B A-modal B-modal =
      retractIsModal {◯ (Σ A B)} {Σ A B} ◯-isModal η-inv η r

      where h : ◯ (Σ A B) → A
            h = ◯-rec A-modal fst

            h-β : (x : Σ A B) → h (η x) ≡ fst x
            h-β = ◯-rec-β A-modal fst

            f : (j : I) → (x : Σ A B) → B (h-β x j)
            f j x = transp (λ i → B (h-β x ((~ i) ∨ j))) j (snd x)

            k : (y : ◯ (Σ A B)) → B (h y)
            k = ◯-elim (B-modal ∘ h) (f i0)

            η-inv : ◯ (Σ A B) → Σ A B
            η-inv y = h y , k y

            p : (x : Σ A B) → k (η x) ≡ f i0 x
            p = ◯-elim-β (B-modal ∘ h) (f i0)

            almost : (x : Σ A B) → (h (η x) , f i0 x) ≡ x
            almost x i = h-β x i , f i x

            r : (x : Σ A B) → η-inv (η x) ≡ x
            r x = (λ i → h (η x) , p x i) ∙ (almost x)

ext: agda

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
{- MJ where variable declarations have been hoisted to the top of a block -}
module CF.Transform.Hoist where

open import Level
open import Function using (_∘_)
open import Data.List
open import Data.List.Properties
open import Data.Unit
open import Data.Product
open import Relation.Unary hiding (_⊢_)
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Ternary.Core
open import Relation.Ternary.Structures
open import Relation.Ternary.Structures.Syntax
open import Relation.Ternary.Monad
open import Relation.Ternary.Monad.Weakening
open import Relation.Ternary.Structures.Syntax

open import CF.Types
open import CF.Contexts.Lexical
open import CF.Syntax as Src hiding (Stmt; Block; Statement; var) public
open import CF.Syntax.Hoisted as Hoisted

open import Relation.Ternary.Construct.List.Overlapping Ty
open import Relation.Ternary.Data.Bigstar

pattern _⍮⟨_⟩_ s σ b = cons (s ∙⟨ σ ⟩ b)

hoist-binder : ∀ {P : Pred Ctx 0ℓ} {Γ} → ∀[ (Γ ⊢ P) ⇒ ◇ (Vars Γ ✴ P) ]
hoist-binder px = pack (⊢-zip (∙-copy _) (binders ∙⟨ ∙-idˡ ⟩ px))

-- A typed hoisting transformation for statement blocks
{-# TERMINATING #-}
mutual
  {- Hoist local variables from blocks -}
  hoist : ∀[ Src.Block r ⇒ ◇ (Block r) ]
  hoist Src.emp = do
    return nil

  hoist (ss Src.⍮⟨ σ ⟩ b) = do
    b ∙⟨ σ ⟩ s               ← translate ss                   &⟨ Src.Block _ # ∙-comm σ ⟩ b
    s ∙⟨ σ ⟩ b               ← hoist b                        &⟨ Hoisted.Stmt _ # ∙-comm σ ⟩ s
    return (s ⍮⟨ σ ⟩ b)

  hoist (e Src.≔⟨ σ ⟩ Γ⊢b) = do
    e×v ∙⟨ σ ⟩ b             ← ✴-assocₗ ⟨$⟩ (hoist-binder Γ⊢b &⟨ Src.Exp _ # σ ⟩ e)
    (e ∙⟨ σ₁ ⟩ v) ∙⟨ σ₂ ⟩ b' ← hoist b                        &⟨ _ ✴ _ # σ ⟩ e×v
    return (Hoisted.asgn (v ∙⟨ ∙-comm σ₁ ⟩ e) ⍮⟨ σ₂ ⟩ b')

  {- Hoist local variables from statements -}
  translate : ∀[ Src.Stmt r ⇒ ◇ (Stmt r) ]

  translate (Src.asgn x) = do
    return (Hoisted.asgn x)

  translate (Src.run e) = do
    return (Hoisted.run e)

  translate (Src.while (e ∙⟨ σ ⟩ body)) = do
    e ∙⟨ σ ⟩ body'           ← translate body                 &⟨ Src.Exp _ # σ ⟩ e
    return (Hoisted.while (e ∙⟨ σ ⟩ body'))

  translate (Src.ifthenelse e×s₁×s₂) = do
    let (s₁ ∙⟨ σ ⟩ s₂×e) = ✴-rotateₗ e×s₁×s₂
    s₂ ∙⟨ σ ⟩ e×s₁           ← ✴-assocᵣ ⟨$⟩ (translate s₁     &⟨ _ ✴ _ # ∙-comm σ ⟩ s₂×e)
    e×s₁×s₂                  ← ✴-assocᵣ ⟨$⟩ (translate s₂     &⟨ _ ✴ _ # ∙-comm σ ⟩ e×s₁)
    return (Hoisted.ifthenelse e×s₁×s₂)

  translate (Src.block bl) = do
    bl'                      ← hoist bl
    return (Hoisted.block bl')


text:
{-# OPTIONS --cubical --safe #-}

module Cardinality.Infinite.Split where

open import Prelude
open import Data.List.Kleene
open import Data.Fin
import Data.Nat as ℕ
open import Data.Nat using (_+_)
open import Cubical.Data.Sigma.Properties
open import Cubical.Foundations.Prelude using (J)
import Data.List.Kleene.Membership as Kleene
open import Codata.Stream
open import Data.Sigma.Properties

private
  variable
    u : Level
    U : A → Type u
    s : Level
    S : ℕ → Type s

ℰ! : Type a → Type a
ℰ! A = Σ[ xs ⦂ Stream A ] Π[ x ⦂ A ] x ∈ xs

ℰ!⇔ℕ↠! : ℰ! A ≡ (ℕ ↠! A)
ℰ!⇔ℕ↠! = refl

infixl 6 _*_ _*⋆_[_]
_*_ : Stream A → (∀ x → Stream (U x)) → Stream (Σ A U ⁺)
_*⋆_[_] : Stream A → (∀ x → Stream (U x)) → Stream (Σ A U ⋆)
cantor : Stream A → (∀ x → Stream (U x)) → Stream (Σ A U)
cantor xs ys = concat (xs * ys)

xs *⋆ ys [ zero   ] = []
xs *⋆ ys [ suc n  ] = ∹ (xs * ys) n

(xs * ys) n .head  = x , ys x n where x = xs 0
(xs * ys) n .tail  = (xs ∘ suc) *⋆ ys [ n ]

*-cover : ∀ (x : A) xs (y : U x) (ys : ∀ x → Stream (U x)) → x ∈ xs → y ∈ ys x → (x , y) ∈² xs * ys
*-cover {U = U} x xs y ys (n , x∈xs) (m , y∈ys) = (n + m) , lemma xs n x∈xs
  where
  lemma : ∀ xs n → xs n ≡ x → (x , y) Kleene.∈⁺ (xs * ys) (n + m)
  lemma xs zero    x∈xs .fst = f0
  lemma xs zero    x∈xs .snd i .fst = x∈xs i
  lemma xs zero    x∈xs .snd i .snd = J (λ z z≡ → PathP (λ j → U (sym z≡ j)) (ys z m) y) y∈ys (sym x∈xs) i
  lemma xs (suc n) x∈xs = let i , p = lemma (xs ∘ suc) n x∈xs in fs i , p

_|Σ|_ : ℰ! A → (∀ x → ℰ! (U x)) → ℰ! (Σ A U)
(xs |Σ| ys) .fst = cantor (xs .fst) (fst ∘ ys)
(xs |Σ| ys) .snd (x , y) =
  concat-∈
    (x , y)
    (xs .fst * (fst ∘ ys))
    (*-cover x (xs .fst) y (fst ∘ ys) (xs .snd x) (ys x .snd y))

open import Data.Nat using (_+_)

infixl 6 _∔_
_∔_ : ℕ → ℕ → ℕ
zero ∔ m = m
suc n ∔ m = n ∔ suc m

∔-suc : ∀ n m → suc n ∔ m ≡ suc (n ∔ m)
∔-suc zero    m = refl
∔-suc (suc n) m = ∔-suc n (suc m)

∔0 : ∀ n → n ∔ zero ≡ n
∔0 zero    = refl
∔0 (suc n) = ∔-suc n 0 ; cong suc (∔0 n)

module _ (xs : Stream A) where
  mutual
    star⁺ : (A ⋆ → B) → B ⋆ → Stream (B ⁺)
    star⁺ k ks zero    = k [] & ks
    star⁺ k ks (suc i) = plus⁺ zero (k ∘ ∹_) ks i

    plus⋆ : ℕ → (A ⁺ → B) → B ⋆ → Stream (B ⋆)
    plus⋆ n k ks zero    = ks
    plus⋆ n k ks (suc i) = ∹ plus⁺ n k ks i

    plus⁺ : ℕ → (A ⁺ → B) → B ⋆ → Stream (B ⁺)
    plus⁺ n k ks i = star⁺ (k ∘ (xs n &_)) (plus⋆ (suc n) k ks i) i

  star : Stream (A ⋆)
  star = concat (star⁺ id [])

  plus : Stream (A ⁺)
  plus = concat (plus⁺ zero id [])

  module _ (cover : ∀ x → x ∈ xs) where
    dist : A ⋆ → ℕ
    dist = foldr⋆ (λ y ys → suc (cover y .fst + ys)) zero

    mutual
      star⁺-cover : (k : A ⋆ → B) → (ks : B ⋆) → ∀ x → k x Kleene.∈⁺ star⁺ k ks (dist x)
      star⁺-cover k ks [] = f0 , refl
      star⁺-cover k ks (∹ x ) = plus⁺-cover (k ∘ ∹_) ks x

      plus⁺-cover : ∀ (k : A ⁺ → B) ks → ∀ x → k x Kleene.∈⁺ plus⁺ zero k ks (cover (head x) .fst + dist (tail x))
      plus⁺-cover k ks (x & xxs) =
        let n , p = cover x
            m , q = plus⁺-dist n (k ) ks xxs
            z = m , q ; cong (k ∘ (_& xxs)) p
        in plus⁺-shift zero (dist xxs) n k ks (x & xxs) (subst (λ s → k (x & xxs) Kleene.∈⁺ plus⁺ s k ks (dist xxs)) (sym (∔0 (cover x .fst))) z)

      plus⁺-dist : ∀ n (k : A ⁺ → B) ks → ∀ xxs → k (xs n & xxs) Kleene.∈⁺ plus⁺ n k ks (dist xxs)
      plus⁺-dist n k ks xxs = star⁺-cover (k ∘ _&_ (xs n)) (plus⋆ (suc n) k ks (dist xxs)) xxs

      plus⁺-run : ∀ n i (k : A ⁺ → B) ks → ∀ xxs → xxs Kleene.∈⋆ ks → xxs Kleene.∈⁺ plus⁺ n k ks i
      plus⁺-run n zero    k ks xxs (m , p) = fs m , p
      plus⁺-run n (suc i) k ks xxs =
        plus⁺-run zero i (k ∘ (xs n &_) ∘ ∹_) (plus⋆ (suc n) k ks (suc i)) xxs ∘
        plus⁺-run (suc n) i k ks xxs

      plus⁺-shift : ∀ i d n (k : A ⁺ → B) (ks : B ⋆) → ∀ xxs → k xxs Kleene.∈⁺ plus⁺ (n ∔ i) k ks d → k xxs Kleene.∈⁺ plus⁺ i k ks (n + d)
      plus⁺-shift i d zero    k ks xxs p = p
      plus⁺-shift i d (suc n) k ks xxs p = plus⁺-run zero (n + d) (λ z → k (xs i & ∹ z)) (∹ plus⁺ (suc i) k ks (n + d)) (k xxs) (plus⁺-shift (suc i) d n k ks xxs p)

    star-cover : ∀ x → x ∈ star
    star-cover x = concat-∈ x (star⁺ id []) (dist x , star⁺-cover id [] x)

    plus-cover : ∀ x → x ∈ plus
    plus-cover x = concat-∈ x (plus⁺ zero id []) (cover (head x) .fst + dist (tail x) , plus⁺-cover id [] x)

|star| : ℰ! A → ℰ! (A ⋆)
|star| xs .fst = star (xs .fst)
|star| xs .snd = star-cover (xs .fst) (xs .snd)

|plus| : ℰ! A → ℰ! (A ⁺)
|plus| xs .fst = plus (xs .fst)
|plus| xs .snd = plus-cover (xs .fst) (xs .snd)

open import Data.Bool using (not; bool)

x≢¬x : ∀ x → x ≢ not x
x≢¬x false p = subst (bool ⊤ ⊥) p tt
x≢¬x true  p = subst (bool ⊥ ⊤) p tt

cantor-diag : ¬ (ℰ! (Stream Bool))
cantor-diag (sup , cov) = let n , p = cov (λ n → not (sup n n)) in x≢¬x _ (cong (_$ n) p)

ℰ : Type a → Type a
ℰ A = ∥ ℰ! A ∥

open import Function.Surjective.Properties
open import Data.Nat.Properties using (discreteℕ)
open import HITs.PropositionalTruncation
open import Relation.Nullary.Discrete.Properties

ℰ!⇒Discrete : ℰ! A → Discrete A
ℰ!⇒Discrete xs = Discrete-distrib-surj xs discreteℕ

ℰ⇒Discrete : ℰ A → Discrete A
ℰ⇒Discrete = rec isPropDiscrete ℰ!⇒Discrete

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
{-# OPTIONS --enable-prop #-}

True : Prop
True = {P : Prop} → P → P

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text:
module Issue784.Transformer where

open import Data.List using (List; []; _∷_; _++_; [_]; filter) renaming (map to mapL)
import Level

open import Issue784.Values
open import Issue784.Context

Transformer : ∀ {ℓ} → NonRepetitiveTypes ℓ → NonRepetitiveTypes ℓ → Set (Level.suc ℓ)
Transformer {ℓ} (t-in , nr-in) (t-out , nr-out) =
  (v : Context ℓ) → NonRepetitiveContext v → t-in ⊆ signature v → NonRepetitive (ctxnames v ∖ names t-in ∪ names t-out) →
  Σ[ w ∈ Context ℓ ] signature w ≋ signature v ∖∖ names t-in ∪ t-out

pipe : ∀ {ℓ} {t-in₁ t-out₁ t-in₂ t-out₂ : Types ℓ} {nr-in₁ nr-out₁ nr-in₂ nr-out₂} →
       Transformer (t-in₁ , nr-in₁) (t-out₁ , nr-out₁) →
       Transformer (t-in₂ , nr-in₂) (t-out₂ , nr-out₂) →
       let n-out₁ = names t-out₁
           n-in₂ = names t-in₂
           t-in = t-in₁ ∪ (t-in₂ ∖∖ n-out₁)
           t-out = t-out₁ ∖∖ n-in₂ ∪ t-out₂
       in
       filter-∈ t-out₁ n-in₂ ≋ filter-∈ t-in₂ n-out₁ →
       (nr-in : NonRepetitiveNames t-in) (nr-out : NonRepetitiveNames t-out) →
       Transformer (t-in , nr-in) (t-out , nr-out)
pipe {ℓ} {t-in₁} {t-out₁} {t-in₂} {t-out₂} {nr-in₁} {nr-out₁} {nr-in₂} {nr-out₂} tr₁ tr₂ pr-t nr-in nr-out = tr where
    n-in₁ = names t-in₁
    n-out₁ = names t-out₁
    n-in₂ = names t-in₂
    n-out₂ = names t-out₂

    t-in = t-in₁ ∪ (t-in₂ ∖∖ n-out₁)
    t-out = (t-out₁ ∖∖ n-in₂) ∪ t-out₂

    tr : Transformer (t-in , nr-in) (t-out , nr-out)
    tr ctx nr-v t-ì⊆v nr-ò = context w , w≋out where
        v = Context.get ctx
        n-in = names t-in
        v̀ = filter-∈ v n-in
        nr-v̀ : NonRepetitiveNames v̀
        nr-v̀ = nr-x⇒nr-x∩y nr-v n-in

        v̀≋i : types v̀ ≋ t-in
        v̀≋i = ≋-sym $ ≋-trans p₁ p₂ where
            p₁ : t-in ≋ filter-∈ (types v) n-in
            p₁ = t₁⊆t₂⇒t₁≋f∈-t₂-nt₁ nr-in (≡-elim′ NonRepetitive (≡-sym $ n-types v) nr-v) t-ì⊆v
            p₂ : filter-∈ (types v) n-in ≋ types v̀
            p₂ = ≡⇒≋ $ ≡-sym $ t-filter-∈ v n-in

        -- transformer₁
        i₁⊆v̀ : t-in₁ ⊆ types v̀
        i₁⊆v̀ = x⊆y≋z (x⊆x∪y t-in₁ (t-in₂ ∖∖ n-out₁)) (≋-sym v̀≋i)

        v̀∖i₁∪o₁≋i₂∖o₁∪o₁ : types v̀ ∖∖ n-in₁ ∪ t-out₁ ≋ t-in₂ ∖∖ n-out₁ ∪ t-out₁
        v̀∖i₁∪o₁≋i₂∖o₁∪o₁ = x≋x̀⇒x∪y≋x̀∪y p₂ t-out₁ where
            p₁ : NonRepetitiveNames (types v̀)
            p₁ = nr-x≋y (≡⇒≋ $ ≡-sym $ n-types v̀) nr-v̀
            p₂ : types v̀ ∖∖ n-in₁ ≋ t-in₂ ∖∖ n-out₁
            p₂ = t≋t₁∪t₂⇒t∖t₁≋t₂ p₁ t-in₁ (t-in₂ ∖∖ n-out₁) v̀≋i

        n-v̀∖i₁∪o₁≋i₂∖o₁∪o₁ : names v̀ ∖ n-in₁ ∪ n-out₁ ≋ n-in₂ ∖ n-out₁ ∪ n-out₁
        n-v̀∖i₁∪o₁≋i₂∖o₁∪o₁ = x≋x̀⇒x∪y≋x̀∪y p₃ n-out₁ where
            p₁ : names v̀ ≋ n-in
            p₁ = ≋-trans (≡⇒≋ $ n-filter-∈ v n-in) (y⊆x⇒x∩y≋y nr-in nr-v (≡-elim′ (λ x → n-in ⊆ x) (n-types v) (x⊆y⇒nx⊆ny t-ì⊆v)))
            p₂ : n-in ≋ n-in₁ ∪ (n-in₂ ∖ n-out₁)
            p₂ = ≡⇒≋ $ ≡-trans (n-x∪y t-in₁ $ t-in₂ ∖∖ n-out₁) (≡-cong (λ x → n-in₁ ∪ x) (n-x∖y t-in₂ n-out₁))
            p₃ : names v̀ ∖ n-in₁ ≋ n-in₂ ∖ n-out₁
            p₃ = x≋y∪z⇒x∖y≋z (nr-x≋y (≋-sym p₁) nr-in) n-in₁ (n-in₂ ∖ n-out₁) (≋-trans p₁ p₂)

        nr-v̀∖i₁∪o₁ : NonRepetitive (names v̀ ∖ n-in₁ ∪ n-out₁)
        nr-v̀∖i₁∪o₁ = nr-x≋y (≋-sym n-v̀∖i₁∪o₁≋i₂∖o₁∪o₁) p₁ where
            p₁ : NonRepetitive (n-in₂ ∖ n-out₁ ∪ n-out₁)
            p₁ = nr-x∖y∪y nr-in₂ nr-out₁

        w-all₁ : Σ[ w ∈ Context ℓ ] signature w ≋ signature (context v̀) ∖∖ names t-in₁ ∪ t-out₁
        w-all₁ = tr₁ (context v̀) nr-v̀ i₁⊆v̀ nr-v̀∖i₁∪o₁

        w₁ = Context.get $ proj₁ w-all₁
        w₁≋v̀∖i₁∪o₁ = proj₂ w-all₁

        -- transformer₂
        n-w₁≋v̀∖i₁∪o₁ : names w₁ ≋ names v̀ ∖ names t-in₁ ∪ names t-out₁
        n-w₁≋v̀∖i₁∪o₁ = ≡-elim p₆ p₅ where
            p₁ : names (types w₁) ≋ names (types v̀ ∖∖ names t-in₁ ∪ t-out₁)
            p₁ = n-x≋y w₁≋v̀∖i₁∪o₁
            p₂ : names (types v̀ ∖∖ names t-in₁ ∪ t-out₁) ≡ names (types v̀ ∖∖ names t-in₁) ∪ names t-out₁
            p₂ = n-x∪y (types v̀ ∖∖ names t-in₁) t-out₁
            p₃ : names (types v̀ ∖∖ names t-in₁) ≡ names (types v̀) ∖ names t-in₁
            p₃ = n-x∖y (types v̀) (names t-in₁)
            p₄ : names (types w₁) ≋ names (types v̀ ∖∖ names t-in₁) ∪ names t-out₁
            p₄ = ≡-elim′ (λ x → names (types w₁) ≋ x) p₂ p₁
            p₅ : names (types w₁) ≋ names (types v̀) ∖ names t-in₁ ∪ names t-out₁
            p₅ = ≡-elim′ (λ x → names (types w₁) ≋ x ∪ names t-out₁) p₃ p₄
            p₆ : (names (types w₁) ≋ names (types v̀) ∖ names t-in₁ ∪ names t-out₁) ≡
                 (names w₁ ≋ names v̀ ∖ names t-in₁ ∪ names t-out₁)
            p₆ = ≡-cong₂ (λ x y → x ≋ y ∖ names t-in₁ ∪ names t-out₁) (n-types w₁) (n-types v̀)

        nr-w₁ : NonRepetitiveNames w₁
        nr-w₁ = nr-x≋y (≋-sym n-w₁≋v̀∖i₁∪o₁) nr-v̀∖i₁∪o₁

        i₂⊆w₁ : t-in₂ ⊆ types w₁
        i₂⊆w₁ = x⊆y≋z (x≋y⊆z (≋-sym p₁) p₄) (≋-sym w₁≋v̀∖i₁∪o₁) where
            p₁ : t-in₂ ≋ (t-in₂ ∖∖ n-out₁) ∪ filter-∈ t-in₂ n-out₁
            p₁ = t≋t∖n∪t∩n t-in₂ n-out₁
            p₂ : filter-∈ t-in₂ n-out₁ ⊆ t-out₁
            p₂ = x≋y⊆z pr-t $ x∩y⊆x t-out₁ n-in₂
            p₃ : types v̀ ∖∖ n-in₁ ≋ t-in₂ ∖∖ n-out₁
            p₃ = t≋t₁∪t₂⇒t∖t₁≋t₂ (≡-elim′ NonRepetitive (≡-sym $ n-types v̀) nr-v̀) t-in₁ (t-in₂ ∖∖ n-out₁) v̀≋i
            p₄ : (t-in₂ ∖∖ n-out₁) ∪ (filter-∈ t-in₂ n-out₁) ⊆ (types v̀ ∖∖ n-in₁) ∪ t-out₁
            p₄ = x∪y⊆x̀∪ỳ (≋⇒⊆ $ ≋-sym p₃) p₂

        w₁∖i₂∪o₂≋out : types w₁ ∖∖ n-in₂ ∪ t-out₂ ≋ t-out
        w₁∖i₂∪o₂≋out = x≋x̀⇒x∪y≋x̀∪y p₄ t-out₂ where
            p₁ : t-in₂ ∖∖ n-out₁ ∪ t-out₁ ≋ t-out₁ ∖∖ n-in₂ ∪ t-in₂
            p₁ = ≋-sym $ x∖y∪y≋y∖x∪x t-out₁ t-in₂ pr-t
            p₂ : (t-out₁ ∖∖ n-in₂) ∪ t-in₂ ≋ t-in₂ ∪ (t-out₁ ∖∖ n-in₂)
            p₂ = ∪-sym (t-out₁ ∖∖ n-in₂) t-in₂
            p₃ : types w₁ ≋ t-in₂ ∪ (t-out₁ ∖∖ n-in₂)
            p₃ = ≋-trans w₁≋v̀∖i₁∪o₁ $ ≋-trans v̀∖i₁∪o₁≋i₂∖o₁∪o₁ $ ≋-trans p₁ p₂
            p₄ : types w₁ ∖∖ n-in₂ ≋ t-out₁ ∖∖ n-in₂
            p₄ = t≋t₁∪t₂⇒t∖t₁≋t₂ (nr-x≋y (≡⇒≋ $ ≡-sym $ n-types w₁) nr-w₁) t-in₂ (t-out₁ ∖∖ n-in₂) p₃

        nr-w₁∖i₂∪o₂ : NonRepetitive (names w₁ ∖ n-in₂ ∪ n-out₂)
        nr-w₁∖i₂∪o₂ = ≡-elim′ NonRepetitive p₄ p₅ where
            p₁ : names (types w₁ ∖∖ n-in₂ ∪ t-out₂) ≡ names (types w₁ ∖∖ n-in₂) ∪ n-out₂
            p₁ = n-x∪y (types w₁ ∖∖ n-in₂) t-out₂
            p₂ : names (types w₁ ∖∖ n-in₂) ∪ n-out₂ ≡ (names (types w₁) ∖ n-in₂) ∪ n-out₂
            p₂ = ≡-cong (λ x → x ∪ names t-out₂) (n-x∖y (types w₁) n-in₂)
            p₃ : (names (types w₁) ∖ n-in₂) ∪ n-out₂ ≡ names w₁ ∖ n-in₂ ∪ n-out₂
            p₃ = ≡-cong (λ x → x ∖ n-in₂ ∪ n-out₂) (n-types w₁)
            p₄ : names (types w₁ ∖∖ n-in₂ ∪ t-out₂) ≡ names w₁ ∖ n-in₂ ∪ n-out₂
            p₄ = ≡-trans p₁ $ ≡-trans p₂ p₃
            p₅ : NonRepetitiveNames (types w₁ ∖∖ n-in₂ ∪ t-out₂)
            p₅ = nr-x≋y (≋-sym $ n-x≋y w₁∖i₂∪o₂≋out) nr-out

        w-all₂ : Σ[ w ∈ Context ℓ ] signature w ≋ signature (context w₁) ∖∖ names t-in₂ ∪ t-out₂
        w-all₂ = tr₂ (context w₁) nr-w₁ i₂⊆w₁ nr-w₁∖i₂∪o₂

        w₂ = Context.get $ proj₁ w-all₂
        w₂≋out : types w₂ ≋ t-out
        w₂≋out = ≋-trans (proj₂ w-all₂) w₁∖i₂∪o₂≋out

        w =  Values ℓ ∋ v ∖∖ n-in ∪ w₂
        w≋out : types w ≋ types v ∖∖ n-in ∪ t-out
        w≋out = ≋-trans (≡⇒≋ p₁) p₂ where
            p₁ : types (v ∖∖ n-in ∪ w₂) ≡ types v ∖∖ n-in ∪ types w₂
            p₁ = ≡-trans (t-x∪y (v ∖∖ n-in) w₂) (≡-cong (λ x → x ∪ types w₂) (t-x∖y v n-in))
            p₂ : types v ∖∖ n-in ∪ types w₂ ≋ types v ∖∖ n-in ∪ t-out
            p₂ = y≋ỳ⇒x∪y≋x∪ỳ (types v ∖∖ n-in) w₂≋out

Transformer! : ∀ {ℓ} (t-in : Types ℓ) (t-out : Types ℓ) {nr!-in : NonRepetitiveNames! t-in} {nr!-out : NonRepetitiveNames! t-out} → Set (Level.suc ℓ)
Transformer! t-in t-out {nr!-in = nr!-in} {nr!-out} = Transformer (t-in , s-nr!⇒nr nr!-in) (t-out , s-nr!⇒nr nr!-out)

infix 1 _:=_
_:=_ : ∀ {ℓ} {A : String → Set ℓ} (n : String) → ((n : String) → A n) → A n
n := f = f n

infixl 0 _⇒⟦_⟧⇒_
_⇒⟦_⟧⇒_ : ∀ {ℓ} {t-in₁ t-out₁ t-in₂ t-out₂ : Types ℓ}
          {nr!-in₁ : NonRepetitiveNames! t-in₁}
          {nr!-out₁ : NonRepetitiveNames! t-out₁}
          {nr!-in₂ : NonRepetitiveNames! t-in₂}
          {nr!-out₂ : NonRepetitiveNames! t-out₂} →
       Transformer (t-in₁ , s-nr!⇒nr nr!-in₁) (t-out₁ , s-nr!⇒nr nr!-out₁) →

       let n-out₁ = names t-out₁
           n-in₂ = names t-in₂
           t-in = t-in₁ ∪ (t-in₂ ∖∖ n-out₁)
           t-out = t-out₁ ∖∖ n-in₂ ∪ t-out₂
       in
       filter-∈ t-out₁ n-in₂ ≋ filter-∈ t-in₂ n-out₁ →
       {nr!-in : NonRepetitiveNames! t-in} →
       {nr!-out : NonRepetitiveNames! t-out} →

       Transformer (t-in₂ , s-nr!⇒nr nr!-in₂) (t-out₂ , s-nr!⇒nr nr!-out₂) →
       Transformer (t-in , s-nr!⇒nr nr!-in) (t-out , s-nr!⇒nr nr!-out)

_⇒⟦_⟧⇒_ {nr!-in₁ = nr!-in₁} {nr!-out₁ = nr!-out₁} {nr!-in₂ = nr!-in₂} {nr!-out₂ = nr!-out₂}
        tr₁ f≋f {nr!-in = nr!-in} {nr!-out = nr!-out} tr₂ =
    pipe {nr-in₁ = s-nr!⇒nr nr!-in₁} {nr-out₁ = s-nr!⇒nr nr!-out₁} {nr-in₂ = s-nr!⇒nr nr!-in₂} {nr-out₂ = s-nr!⇒nr nr!-out₂}
        tr₁ tr₂ f≋f (s-nr!⇒nr nr!-in) (s-nr!⇒nr nr!-out)

record Pure {ℓ} (A : Set ℓ) : Set ℓ where
    constructor pure
    field get : A

record Unique {ℓ} (A : Set ℓ) : Set ℓ where
    constructor unique
    field get : A

extract : ∀ {ℓ} {n : String} {A : Set ℓ} → let t = [ (n , Pure A) ] in {nr!-t : NonRepetitiveNames! t} → Transformer ([] , []) (t , s-nr!⇒nr nr!-t) → A
extract {n = n} {A = A} {nr!-t = nr!-t} tr =
  let e = n , Pure A
      v , t-v≋t = (Σ[ v ∈ Context _ ] signature v ≋ [ e ]) ∋ tr (context []) [] (≋⇒⊆ refl) (s-nr!⇒nr nr!-t)
  in Pure.get ∘ getBySignature $ a∈x⇒x≋y⇒a∈y (e ∈ [ e ] ∋ here refl) (≋-sym t-v≋t)

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- Nested applications of the defined function can be handled
------------------------------------------------------------------------

module Nested where

open import Codata.Musical.Notation
open import Codata.Musical.Stream
open import Function
import Relation.Binary.PropositionalEquality as P

------------------------------------------------------------------------
-- A definition of φ (x ∷ xs) = x ∷ φ (φ xs)

module φ where

  infixr 5 _∷_

  data StreamP (A : Set) : Set where
    _∷_ : (x : A) (xs : ∞ (StreamP A)) → StreamP A
    φP  : (xs : StreamP A) → StreamP A

  data StreamW (A : Set) : Set where
    _∷_ : (x : A) (xs : StreamP A) → StreamW A

  φW  : {A : Set} → StreamW A → StreamW A
  φW (x ∷ xs) = x ∷ φP (φP xs)

  whnf : {A : Set} → StreamP A → StreamW A
  whnf (x ∷ xs)   = x ∷ ♭ xs
  whnf (φP xs)    = φW (whnf xs)

  mutual

    ⟦_⟧W : {A : Set} → StreamW A → Stream A
    ⟦ x ∷ xs ⟧W = x ∷ ♯ ⟦ xs ⟧P

    ⟦_⟧P : {A : Set} → StreamP A → Stream A
    ⟦ xs ⟧P = ⟦ whnf xs ⟧W

  ⌈_⌉ : {A : Set} → Stream A → StreamP A
  ⌈ x ∷ xs ⌉ = x ∷ ♯ ⌈ ♭ xs ⌉

  φ : {A : Set} → Stream A → Stream A
  φ xs = ⟦ φP ⌈ xs ⌉ ⟧P

open φ using (⟦_⟧P; ⟦_⟧W; φP; φW; φ; _∷_; ⌈_⌉)

------------------------------------------------------------------------
-- An equality proof language

module Equality where

  φ-rhs : {A : Set} → (Stream A → Stream A) → Stream A → Stream A
  φ-rhs φ (x ∷ xs) = x ∷ ♯ φ (φ (♭ xs))

  SatisfiesEquation : {A : Set} → (Stream A → Stream A) → Set
  SatisfiesEquation φ = ∀ xs → φ xs ≈ φ-rhs φ xs

  infixr 5 _∷_
  infix  4 _≈P_ _≈W_
  infix  3 _∎
  infixr 2 _≈⟨_⟩_

  data _≈P_ {A : Set} : Stream A → Stream A → Set where
    _∷_     : ∀ (x : A) {xs ys}
              (xs≈ys : ∞ (♭ xs ≈P ♭ ys)) → x ∷ xs ≈P x ∷ ys
    _≈⟨_⟩_  : ∀ (xs : Stream A) {ys zs}
              (xs≈ys : xs ≈P ys) (ys≈zs : ys ≈P zs) → xs ≈P zs
    _∎      : (xs : Stream A) → xs ≈P xs
    sym     : ∀ {xs ys} (xs≈ys : xs ≈P ys) → ys ≈P xs
    φP-cong : (xs ys : φ.StreamP A) (xs≈ys : ⟦ xs ⟧P ≈P ⟦ ys ⟧P) →
              ⟦ φP xs ⟧P ≈P ⟦ φP ys ⟧P
    lemma   : (φ₁ φ₂ : Stream A → Stream A)
              (s₁ : SatisfiesEquation φ₁) (s₂ : SatisfiesEquation φ₂) →
              ∀ {xs ys} (xs≈ys : xs ≈P ys) → φ-rhs φ₁ xs ≈P φ-rhs φ₂ ys

  -- Completeness.

  completeP : {A : Set} {xs ys : Stream A} → xs ≈ ys → xs ≈P ys
  completeP (P.refl ∷ xs≈ys) = _ ∷ ♯ completeP (♭ xs≈ys)

  -- Weak head normal forms.

  data _≈W_ {A : Set} : Stream A → Stream A → Set where
    _∷_ : ∀ x {xs ys} (xs≈ys : ♭ xs ≈P ♭ ys) → x ∷ xs ≈W x ∷ ys

  transW : {A : Set} {xs ys zs : Stream A} →
           xs ≈W ys → ys ≈W zs → xs ≈W zs
  transW (x ∷ xs≈ys) (.x ∷ ys≈zs) = x ∷ (_ ≈⟨ xs≈ys ⟩ ys≈zs)

  reflW : {A : Set} (xs : Stream A) → xs ≈W xs
  reflW (x ∷ xs) = x ∷ (♭ xs ∎)

  symW : {A : Set} {xs ys : Stream A} → xs ≈W ys → ys ≈W xs
  symW (x ∷ xs≈ys) = x ∷ sym xs≈ys

  φW-cong : {A : Set} (xs ys : φ.StreamW A) →
            ⟦ xs ⟧W ≈W ⟦ ys ⟧W → ⟦ φW xs ⟧W ≈W ⟦ φW ys ⟧W
  φW-cong (.x ∷ xs) (.x ∷ ys) (x ∷ xs≈ys) =
    x ∷ φP-cong (φP xs) (φP ys) (φP-cong xs ys xs≈ys)

  lemmaW : {A : Set} (φ₁ φ₂ : Stream A → Stream A)
           (s₁ : SatisfiesEquation φ₁) (s₂ : SatisfiesEquation φ₂) →
           ∀ {xs ys} → xs ≈W ys → φ-rhs φ₁ xs ≈W φ-rhs φ₂ ys
  lemmaW φ₁ φ₂ s₁ s₂ {.x ∷ xs} {.x ∷ ys} (x ∷ xs≈ys) = x ∷ (
    φ₁ (φ₁ (♭ xs))        ≈⟨ completeP $ s₁ (φ₁ (♭ xs)) ⟩
    φ-rhs φ₁ (φ₁ (♭ xs))  ≈⟨ lemma φ₁ φ₂ s₁ s₂ (
      φ₁ (♭ xs)                ≈⟨ completeP $ s₁ (♭ xs) ⟩
      φ-rhs φ₁ (♭ xs)          ≈⟨ lemma φ₁ φ₂ s₁ s₂ xs≈ys ⟩
      φ-rhs φ₂ (♭ ys)          ≈⟨ sym $ completeP $ s₂ (♭ ys) ⟩
      φ₂ (♭ ys)                ∎) ⟩
    φ-rhs φ₂ (φ₂ (♭ ys))  ≈⟨ sym $ completeP $ s₂ (φ₂ (♭ ys)) ⟩
    φ₂ (φ₂ (♭ ys))        ∎)

  whnf : {A : Set} {xs ys : Stream A} → xs ≈P ys → xs ≈W ys
  whnf (x ∷ xs≈ys)               = x ∷ ♭ xs≈ys
  whnf (xs ≈⟨ xs≈ys ⟩ ys≈zs)     = transW (whnf xs≈ys) (whnf ys≈zs)
  whnf (xs ∎)                    = reflW xs
  whnf (sym xs≈ys)               = symW (whnf xs≈ys)
  whnf (lemma φ₁ φ₂ s₁ s₂ xs≈ys) = lemmaW φ₁ φ₂ s₁ s₂ (whnf xs≈ys)
  whnf (φP-cong xs ys xs≈ys)     =
    φW-cong (φ.whnf xs) (φ.whnf ys) (whnf xs≈ys)

  -- Soundness.

  mutual

    soundW : {A : Set} {xs ys : Stream A} → xs ≈W ys → xs ≈ ys
    soundW (x ∷ xs≈ys) = P.refl ∷ ♯ soundP xs≈ys

    soundP : {A : Set} {xs ys : Stream A} → xs ≈P ys → xs ≈ ys
    soundP xs≈ys = soundW (whnf xs≈ys)

open Equality
  using (_≈P_; _∷_; _≈⟨_⟩_; _∎; sym; φP-cong; φ-rhs; SatisfiesEquation)

------------------------------------------------------------------------
-- Correctness

module Correctness where

  -- Uniqueness of solutions for φ's defining equation.

  φ-unique : {A : Set} (φ₁ φ₂ : Stream A → Stream A) →
             SatisfiesEquation φ₁ → SatisfiesEquation φ₂ →
             ∀ xs → φ₁ xs ≈P φ₂ xs
  φ-unique φ₁ φ₂ hyp₁ hyp₂ xs =
    φ₁ xs        ≈⟨ Equality.completeP (hyp₁ xs) ⟩
    φ-rhs φ₁ xs  ≈⟨ Equality.lemma φ₁ φ₂ hyp₁ hyp₂ (xs ∎) ⟩
    φ-rhs φ₂ xs  ≈⟨ sym (Equality.completeP (hyp₂ xs)) ⟩
    φ₂ xs        ∎

  -- The remainder of this module establishes the existence of a
  -- solution.

  ⟦⌈_⌉⟧P : {A : Set} (xs : Stream A) → ⟦ ⌈ xs ⌉ ⟧P ≈P xs
  ⟦⌈ x ∷ xs ⌉⟧P = x ∷ ♯ ⟦⌈ ♭ xs ⌉⟧P

  φ-cong : {A : Set} (xs ys : Stream A) → xs ≈P ys → φ xs ≈P φ ys
  φ-cong xs ys xs≈ys =
    φ xs            ≈⟨ φ xs ∎ ⟩
    ⟦ φP ⌈ xs ⌉ ⟧P  ≈⟨ φP-cong ⌈ xs ⌉ ⌈ ys ⌉ lemma ⟩
    ⟦ φP ⌈ ys ⌉ ⟧P  ≈⟨ φ ys ∎ ⟩
    φ ys  ∎
    where
    lemma =
      ⟦ ⌈ xs ⌉ ⟧P  ≈⟨ ⟦⌈ xs ⌉⟧P ⟩
      xs           ≈⟨ xs≈ys ⟩
      ys           ≈⟨ sym ⟦⌈ ys ⌉⟧P ⟩
      ⟦ ⌈ ys ⌉ ⟧P  ∎

  -- ♯′ provides a workaround for Agda's strange definitional
  -- equality.

  infix 10 ♯′_

  ♯′_ : {A : Set} → A → ∞ A
  ♯′ x = ♯ x

  φW-hom : {A : Set} (xs : φ.StreamW A) →
           ⟦ φW xs ⟧W ≈P head ⟦ xs ⟧W ∷ ♯′ φ (φ (tail ⟦ xs ⟧W))
  φW-hom (x ∷ xs) = x ∷ ♯ (
    ⟦ φP (φP xs) ⟧P                  ≈⟨ φP-cong (φP xs) (φP ⌈ ⟦ xs ⟧P ⌉) $
                                                φP-cong xs (⌈ ⟦ xs ⟧P ⌉)
                                                        (sym ⟦⌈ ⟦ xs ⟧P ⌉⟧P) ⟩
    ⟦ φP (φP ⌈ ⟦ xs ⟧P ⌉) ⟧P         ≈⟨ φP-cong (φP ⌈ ⟦ xs ⟧P ⌉)
                                                ⌈ ⟦ φP ⌈ ⟦ xs ⟧P ⌉ ⟧P ⌉
                                                (sym ⟦⌈ ⟦ φP ⌈ ⟦ xs ⟧P ⌉ ⟧P ⌉⟧P) ⟩
    ⟦ φP ⌈ ⟦ φP ⌈ ⟦ xs ⟧P ⌉ ⟧P ⌉ ⟧P  ∎)

  φ-hom : {A : Set} (xs : φ.StreamP A) →
          ⟦ φP xs ⟧P ≈P head ⟦ xs ⟧P ∷ ♯′ φ (φ (tail ⟦ xs ⟧P))
  φ-hom xs = φW-hom (φ.whnf xs)

  φ-correct : {A : Set} (xs : Stream A) →
              φ xs ≈P φ-rhs φ xs
  φ-correct (x ∷ xs) =
    φ (x ∷ xs)                  ≈⟨ φ (x ∷ xs) ∎ ⟩
    ⟦ φP ⌈ x ∷ xs ⌉ ⟧P          ≈⟨ φ-hom ⌈ x ∷ xs ⌉ ⟩
    x ∷ ♯′ φ (φ ⟦ ⌈ ♭ xs ⌉ ⟧P)  ≈⟨ x ∷ ♯ φ-cong (φ ⟦ ⌈ ♭ xs ⌉ ⟧P) (φ (♭ xs))
                                                (φ-cong (⟦ ⌈ ♭ xs ⌉ ⟧P) (♭ xs) ⟦⌈ ♭ xs ⌉⟧P) ⟩
    φ-rhs φ (x ∷ xs)            ∎

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Homotopy.Connected where

open import Cubical.Core.Everything
open import Cubical.Foundations.Everything
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Path
open import Cubical.Foundations.Univalence
open import Cubical.Functions.Fibration
open import Cubical.Data.Nat
open import Cubical.Data.Sigma
open import Cubical.HITs.Nullification
open import Cubical.HITs.Truncation as Trunc

isHLevelConnected : ∀ {ℓ} (n : ℕ) (A : Type ℓ) → Type ℓ
isHLevelConnected n A = isContr (hLevelTrunc n A)

isHLevelConnectedFun : ∀ {ℓ ℓ'} (n : ℕ) {A : Type ℓ} {B : Type ℓ'} (f : A → B) → Type (ℓ-max ℓ ℓ')
isHLevelConnectedFun n f = ∀ b → isHLevelConnected n (fiber f b)

isEquivPrecomposeConnected : ∀ {ℓ ℓ' ℓ''} (n : ℕ)
  {A : Type ℓ} {B : Type ℓ'} (P : B → HLevel ℓ'' n) (f : A → B)
  → isHLevelConnectedFun n f
  → isEquiv (λ(s : (b : B) → P b .fst) → s ∘ f)
isEquivPrecomposeConnected n {A} {B} P f fConn =
  isoToIsEquiv
    (iso (_∘ f)
      (λ t b → inv t b (fConn b .fst))
      (λ t → funExt λ a →
        cong (inv t (f a)) (fConn (f a) .snd ∣ a , refl ∣)
        ∙ substRefl {B = fst ∘ P} (t a))
      (λ s → funExt λ b →
        Trunc.elim
          {B = λ d → inv (s ∘ f) b d ≡ s b}
          (λ _ → isOfHLevelPath n (P b .snd) _ _)
          (λ {(a , p) i → transp (λ j → P (p (j ∨ i)) .fst) i (s (p i))})
          (fConn b .fst)))
  where
  inv : ((a : A) → P (f a) .fst) → (b : B) → hLevelTrunc n (fiber f b) → P b .fst
  inv t b =
    Trunc.rec
      (P b .snd)
      (λ {(a , p) → subst (fst ∘ P) p (t a)})

isOfHLevelPrecomposeConnected : ∀ {ℓ ℓ' ℓ''} (k : ℕ) (n : ℕ)
  {A : Type ℓ} {B : Type ℓ'} (P : B → HLevel ℓ'' (k + n)) (f : A → B)
  → isHLevelConnectedFun n f
  → isOfHLevelFun k (λ(s : (b : B) → P b .fst) → s ∘ f)
isOfHLevelPrecomposeConnected zero n P f fConn =
  isEquivPrecomposeConnected n P f fConn .equiv-proof
isOfHLevelPrecomposeConnected (suc k) n P f fConn t =
    isOfHLevelPath'⁻ k
      (λ {(s₀ , p₀) (s₁ , p₁) →
        subst (isOfHLevel k) (sym (fiber≡ (s₀ , p₀) (s₁ , p₁)))
          (isOfHLevelRetract k
            (λ {(q , α) → (funExt⁻ q) , (cong funExt⁻ α)})
            (λ {(h , β) → (funExt h) , (cong funExt β)})
            (λ _ → refl)
            (isOfHLevelPrecomposeConnected k n
              (λ b → (s₀ b ≡ s₁ b) , isOfHLevelPath' (k + n) (P b .snd) _ _)
              f fConn
              (funExt⁻ (p₀ ∙∙ refl ∙∙ sym p₁))))})

isHLevelConnectedPath : ∀ {ℓ} (n : ℕ) {A : Type ℓ}
  → isHLevelConnected (suc n) A
  → (a₀ a₁ : A) → isHLevelConnected n (a₀ ≡ a₁)
isHLevelConnectedPath n connA a₀ a₁ =
  subst isContr (PathIdTrunc _)
    (isContr→isContrPath connA _ _)

isHLevelConnectedRetract : ∀ {ℓ ℓ'} (n : ℕ)
  {A : Type ℓ} {B : Type ℓ'}
  (f : A → B) (g : B → A)
  (h : (x : A) → g (f x) ≡ x)
  → isHLevelConnected n B → isHLevelConnected n A
isHLevelConnectedRetract n f g h =
  isContrRetract
    (Trunc.map f)
    (Trunc.map g)
    (Trunc.elim
      (λ _ → isOfHLevelPath n (isOfHLevelTrunc n) _ _)
      (λ a → cong ∣_∣ (h a)))

isHLevelConnectedPoint : ∀ {ℓ} (n : ℕ) {A : Type ℓ}
  → isHLevelConnected (suc n) A
  → (a : A) → isHLevelConnectedFun n (λ(_ : Unit) → a)
isHLevelConnectedPoint n connA a₀ a =
  isHLevelConnectedRetract n
    snd (_ ,_) (λ _ → refl)
    (isHLevelConnectedPath n connA a₀ a)


text:
module cry.ec where

open import Level
open import Relation.Nullary
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat using () renaming (Nat to ℕ)
open import Agda.Builtin.List

open import cry.gfp

infixr 4 _,_
infixr 2 _×_

record _×_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B

open _×_ public

-- EC: group of points of elliptic curve (in jacobian coordinates, without conversion to affine)

module ec {c ℓ} (gfp : RawField c ℓ) (a b : RawField.Carrier gfp) where
  module F = RawField gfp
  open F renaming (Carrier to 𝔽; _≈_ to _=F_; _≈?_ to _≟F_)

  record Point : Set c where
    constructor _∶_∶_
    field
      x y z : 𝔽

  is-point : Point → Bool
  -- (y/z³) ² ≡ (x/z²) ³ + a * (x/z²) + b
  is-point (x ∶ y ∶ z) =
    let
      y² = y ²
      x² = x ²
      x³ = x² * x
      z² = z ²
      z⁴ = z² ²
      z⁶ = z² * z⁴
      xz⁴ = x * z⁴
      axz⁴ = a * xz⁴
      bz⁶ = b * z⁶
      x³+axz⁴ = x³ + axz⁴
      x³+axz⁴+bz⁶ = x³+axz⁴ + bz⁶
    in y² F.?≈ x³+axz⁴+bz⁶

  aff : Point → Point
  aff (x ∶ y ∶ z) = x′ ∶ y′ ∶ 1# where
    z⁻¹ = z ⁻¹
    z⁻² = z⁻¹ ²
    z⁻³ = z⁻² * z⁻¹
    x′ = x * z⁻²
    y′ = y * z⁻³

  _==_ : Point → Point → Set _
  (x₁ ∶ y₁ ∶ z₁) == (x₂ ∶ y₂ ∶ z₂)
  -- p₁ == p₂ with norm2 p₁ p₂
  -- ... | (x₁z₂² , x₂z₁²) , (y₁z₂³ , y₂z₁³)
    = x₁z₂² =F x₂z₁² × y₁z₂³ =F y₂z₁³ where
    {-
    x₁/z₁² ≡ x₂/z₂²
    y₁/z₁³ ≡ y₂/z₂³
    -}
    z₂² = z₂ ²
    z₁² = z₁ ²
    x₁z₂² = x₁ * z₂²
    x₂z₁² = x₂ * z₁²
    z₂³ = z₂ * z₂²
    z₁³ = z₁ * z₁²
    y₁z₂³ = y₁ * z₂³
    y₂z₁³ = y₂ * z₁³

  _≟_ : (p₁ p₂ : Point) → Dec (p₁ == p₂)
  (x₁ ∶ y₁ ∶ z₁) ≟ (x₂ ∶ y₂ ∶ z₂) = r where
    z₂² = z₂ ²
    z₁² = z₁ ²
    x₁z₂² = x₁ * z₂²
    x₂z₁² = x₂ * z₁²
    z₂³ = z₂ * z₂²
    z₁³ = z₁ * z₁²
    y₁z₂³ = y₁ * z₂³
    y₂z₁³ = y₂ * z₁³
    r : _
    r with x₁z₂² ≟F x₂z₁²
    ... | no x₁≠x₂ = no (λ p₁=p₂ → x₁≠x₂ (proj₁ p₁=p₂))
    ... | yes x₁=x₂ with y₁z₂³ ≟F y₂z₁³
    ... | no y₁≠y₂ = no (λ p₁=p₂ → y₁≠y₂ (proj₂ p₁=p₂))
    ... | yes y₁=y₂ = yes (x₁=x₂ , y₁=y₂)

  is-𝕆 : Point → Set _
  is-𝕆 (_ ∶ _ ∶ z) = z =F 0#
  {-
  x₃ = λ² − x₁ − x₂
  y₃ = λ(x₁ − x₃) − y₁
  λ = (y₂ - y₁) / (x₂ - x₁), p₁ ≠ p₂
  λ = (3 x₁ ² + a) / (2 y₁), p₁ = p₂

  (x/z²)₃ = λ² − (x/z²)₁ − (x/z²)₂
  (y/z³)₃ = λ((x/z²)₁ − (x/z²)₃) − (y/z³)₁
  λ = ((y/z³)₂ - (y/z³)₁) / ((x/z²)₂ - (x/z²)₁), p₁ ≠ p₂
  λ = (3 (x/z²)₁ ² + a) / (2 (y/z³)₁), p₁ = p₂

  x₃/z₃² z₁² z₂² = λ² z₁² z₂² − x₁ z₂² − x₂ z₁²
  y₁/z₁³ + y₃/z₃³ = λ(x₁/z₁² − (x₃/z₃²))
  y₂/z₂³ + y₃/z₃³ = λ(x₂/z₂² − (x₃/z₃²))
  λ z₁ z₂ (x₂ z₁² - x₁ z₂²) = (y₂ z₁³ - y₁ z₂³), p₁ ≠ p₂
  λ = (3 (x/z²)₁ ² + a) / (2 (y/z³)₁), p₁ = p₂

  p₁ ≠ p₂:
  z₃ = z₁ z₂ (x₂ z₁² - x₁ z₂²)
  λ z₃ = (y₂ z₁³ - y₁ z₂³)
  x₃ = (y₂ z₁³ - y₁ z₂³)² − (x₁ z₂² + x₂ z₁²) (x₂ z₁² - x₁ z₂²)²
  y₃ z₁³ = (y₂ z₁³ - y₁ z₂³) (z₃² x₁ − x₃ z₁²) z₁ − y₁ z₃³

  (y₁ z₃³ + y₃ z₁³)/(y₂ z₁³ - y₁ z₂³) = (x₁ z₃² − x₃ z₁²) z₁
  (y₂ z₃³ + y₃ z₂³)/(y₂ z₁³ - y₁ z₂³) = (x₂ z₃² − x₃ z₂²) z₂

  x₁ z₃² − x₃ z₁² =
     x₁ (z₁ z₂ (x₂ z₁² - x₁ z₂²))² -
     (y₂ z₁³ - y₁ z₂³)² z₁² +
     ((x₂ z₁²)² - (x₁ z₂²)²) (x₂ z₁² - x₁ z₂²) z₁²
  = x₁ z₁² z₂² ((x₂ z₁²)² - 2 x₂ z₁² x₁ z₂² + (x₁ z₂²)²)
    + ((x₂ z₁²)³ - (x₂ z₁²)² x₁ z₂² - (x₁ z₂²)² x₂ z₁² + (x₁ z₂²)³) z₁²
    - (y₂ z₁³ - y₁ z₂³)² z₁²
  = (- (y₂ z₁³ - y₁ z₂³)²
    + 2 x₁³ z₂⁶ + x₂³ z₁⁶ + x₁² x₂ (-3 z₁² z₂⁴)) z₁²

  (y₁ z₃³ + y₃ z₁³) = (y₂ z₁³ - y₁ z₂³) (- (y₂ z₁³ - y₁ z₂³)²
    + 2 x₁³ z₂⁶ + x₂³ z₁⁶ + x₁² x₂ (-3 z₁² z₂⁴)) z₁³
  -}

  𝕆 : Point
  𝕆 = (1# ∶ 1# ∶ 0#)

  dbl : Point → Point
  dbl (x₁ ∶ y₁ ∶ z₁) = (x₃ ∶ y₃ ∶ z₃) where
    {- p₁ = p₂
    x₃ = λ² − x₁ − x₁
    y₃ = λ(x₁ − x₃) − y₁
    λ = (3 x₁ ² + a) / (2 y₁)

    x₃ = λ² z₃² − 2 x₁/z₁² z₃²
    y₃/z₃³ = λ(x₁/z₁² − x₃/z₃²) − y₁/z₁³
    λ = (3 (x₁/z₁²) ² + a) / (2 y₁/z₁³)

    λ 2 y₁ z₁ = 3 x₁² + a z₁⁴
    z₃ = 2 y₁ z₁
    x₃ = (3 x₁² + a z₁⁴)² − 2 x₁ (2 y₁)²

    y₃ = (3 x₁² + a z₁⁴) (x₁ (2 y₁)² − x₃) − y₁ (2 y₁)³
    -}
    2y₁ = y₁ + y₁
    z₃ = 2y₁ * z₁

    x₁² = x₁ ²
    2x₁² = x₁² + x₁²
    3x₁² = 2x₁² + x₁²
    z₁² = z₁ ²
    z₁⁴ = z₁² ²
    az₁⁴ = a * z₁⁴
    3x₁²+az₁⁴ = 3x₁² + az₁⁴
    [3x₁²+az₁⁴]² = 3x₁²+az₁⁴ ²
    y₁² = y₁ ²
    2y₁² = y₁² + y₁²
    4y₁² = 2y₁² + 2y₁²
    x₁[2y₁]² = x₁ * 4y₁²
    2x₁[2y₁]² = x₁[2y₁]² + x₁[2y₁]²
    x₃ = [3x₁²+az₁⁴]² - 2x₁[2y₁]²

    4y₁⁴ = 2y₁² ²
    8y₁⁴ = 4y₁⁴ + 4y₁⁴
    x₁[2y₁]²-x₃ = x₁[2y₁]² - x₃
    [3x₁²+az₁⁴][x₁[2y₁]²-x₃] = 3x₁²+az₁⁴ * x₁[2y₁]²-x₃
    y₃ = [3x₁²+az₁⁴][x₁[2y₁]²-x₃] - 8y₁⁴

  add : Point → Point → Point
  add (x₁ ∶ y₁ ∶ z₁) (x₂ ∶ y₂ ∶ z₂) = x₃ ∶ y₃ ∶ z₃ where
    {- p₁ ≠ p₂
    x₃ = λ² − x₁ − x₂
    y₃ = λ(x₁ − x₃) − y₁
    λ = (y₂ - y₁) / (x₂ - x₁)

    (x/z²)₃ = λ² − (x/z²)₁ − (x/z²)₂
    (y/z³)₃ = λ((x/z²)₁ − (x/z²)₃) − (y/z³)₁
    λ = ((y/z³)₂ - (y/z³)₁) / ((x/z²)₂ - (x/z²)₁)

    λ z₁ z₂ (x₂ z₁² - x₁ z₂²) = (y₂ z₁³ - y₁ z₂³)
    x₃/z₃² z₁² z₂² + x₁ z₂² + x₂ z₁² = λ² z₁² z₂²
    y₃/z₃³ = λ(x₁/z₁² − x₃/z₃²) − y₁/z₁³

    z₃ = z₁ z₂ (x₂ z₁² - x₁ z₂²)
    x₃ = (y₂ z₁³ - y₁ z₂³)² - (x₁ z₂² + x₂ z₁²) (x₂ z₁² - x₁ z₂²)²
    y₃ = (y₂ z₁³ - y₁ z₂³) (x₁ z₂² (x₂ z₁² - x₁ z₂²)² − x₃) − y₁ z₂³ (x₂ z₁² - x₁ z₂²)³
    y₃ = (y₂ z₁³ - y₁ z₂³) ((x₁ z₂²+x₂ z₁²)/2 (x₂ z₁² - x₁ z₂²)² − x₃)
       − (x₂ z₁² - x₁ z₂²)³ (y₁ z₂³ + y₂ z₁³)/2
    -}

    z₁z₂ = z₁ * z₂
    z₁² = z₁ ²
    z₂² = z₂ ²
    x₁z₂² = x₁ * z₂²
    x₂z₁² = x₂ * z₁²
    z₂³ = z₂ * z₂²
    z₁³ = z₁ * z₁²
    y₁z₂³ = y₁ * z₂³
    y₂z₁³ = y₂ * z₁³
    x₂z₁²+x₁z₂² = x₂z₁² + x₁z₂²
    x₂z₁²-x₁z₂² = x₂z₁² - x₁z₂²
    y₂z₁³-y₁z₂³ = y₂z₁³ - y₁z₂³

    z₃ = z₁z₂ * x₂z₁²-x₁z₂²

    [x₂z₁²-x₁z₂²]² = x₂z₁²-x₁z₂² ²
    [y₂z₁³-y₁z₂³]² = y₂z₁³-y₁z₂³ ²
    [x₂z₁²+x₁z₂²][x₂z₁²-x₁z₂²]² = x₂z₁²+x₁z₂² * [x₂z₁²-x₁z₂²]²
    x₃ = [y₂z₁³-y₁z₂³]² - [x₂z₁²+x₁z₂²][x₂z₁²-x₁z₂²]²

    [x₂z₁²-x₁z₂²]³ = x₂z₁²-x₁z₂² * [x₂z₁²-x₁z₂²]²
    y₁z₂³[x₂z₁²-x₁z₂²]³ = y₁z₂³ * [x₂z₁²-x₁z₂²]³
    x₁z₂²[x₂z₁²-x₁z₂²]² = x₁z₂² * [x₂z₁²-x₁z₂²]²
    x₁z₂²[x₂z₁²-x₁z₂²]²-x₃ = x₁z₂²[x₂z₁²-x₁z₂²]² - x₃
    [y₂z₁³-y₁z₂³][x₁z₂²[x₂z₁²-x₁z₂²]²-x₃] = y₂z₁³-y₁z₂³ * x₁z₂²[x₂z₁²-x₁z₂²]²-x₃
    y₃ = [y₂z₁³-y₁z₂³][x₁z₂²[x₂z₁²-x₁z₂²]²-x₃] - y₁z₂³[x₂z₁²-x₁z₂²]³

  dblAdd : Point → ℕ → Point
  dblAdd = times 𝕆 dbl add

module test-ec where
  g = cry.gfp.gfp 7

  open RawField g renaming (Carrier to 𝔽) public

  a b : 𝔽
  a = 4
  b = 1

  xₚ yₚ zₚ : 𝔽
  xₚ = 4
  yₚ = 2
  zₚ = 1

  open ec g a b public
  P 2P : Point
  P = (xₚ ∶ yₚ ∶ zₚ)
  2P = dbl P

max_stars_repo_name: semenov-vladyslav/cry-agda

max_issues_repo_name: semenov-vladyslav/cry-agda

max_forks_repo_name: semenov-vladyslav/cry-agda


text:
module io where

open import bool
open import char
open import list
open import string
open import unit

----------------------------------------------------------------------
-- datatypes
----------------------------------------------------------------------

postulate
  IO : Set → Set

{-# COMPILE GHC IO = type IO #-}
{-# BUILTIN IO IO #-}

----------------------------------------------------------------------
-- syntax
----------------------------------------------------------------------

infixl 1 _>>=_
infixl 1 _>>_

----------------------------------------------------------------------
-- postulated operations
----------------------------------------------------------------------

postulate
  return : ∀ {A : Set} → A → IO A
  _>>=_  : ∀ {A B : Set} → IO A → (A → IO B) → IO B

{-# COMPILE GHC return = \ _ -> return #-}
{-# COMPILE GHC _>>=_ = \ _ _ -> (>>=) #-}

postulate
  putStr : string -> IO ⊤

  -- Reads a file, which is assumed to be finite.
  readFiniteFile : string → IO string

  writeFile : string → string → IO ⊤

  -- set output to UTF-8 for Windows

  initializeStdoutToUTF8 : IO ⊤

  -- set newline mode for Windows

  setStdoutNewlineMode : IO ⊤

  getLine : IO string

private
  postulate
    privGetArgs : IO (𝕃 string)
    privDoesFileExist : string → IO 𝔹
    privCreateDirectoryIfMissing : 𝔹 → string → IO ⊤
    privTakeDirectory : string → string
    privTakeFileName : string → string
    privCombineFileNames : string → string → string
    privForceFileRead : string {- the contents of the file, not the file name -} → IO ⊤

    privGetHomeDirectory : IO string

{-# FOREIGN GHC import qualified System.IO #-}
{-# FOREIGN GHC import qualified Control.DeepSeq #-}
{-# FOREIGN GHC import qualified Data.Text.IO #-}
{-# COMPILE GHC putStr = Data.Text.IO.putStr #-}
{-# COMPILE GHC readFiniteFile = (\y -> let x = Data.Text.unpack y in do inh <- System.IO.openFile x System.IO.ReadMode; System.IO.hSetEncoding inh System.IO.utf8; fileAsString <- System.IO.hGetContents inh; Control.DeepSeq.rnf fileAsString `seq` System.IO.hClose inh; return (Data.Text.pack fileAsString)) #-}
{-# COMPILE GHC writeFile = (\path -> (\str -> do outh <- System.IO.openFile (Data.Text.unpack path) System.IO.WriteMode; System.IO.hSetNewlineMode outh System.IO.noNewlineTranslation; System.IO.hSetEncoding outh System.IO.utf8; Data.Text.IO.hPutStr outh str; System.IO.hFlush outh; System.IO.hClose outh; return () )) #-}
{-# COMPILE GHC initializeStdoutToUTF8 = System.IO.hSetEncoding System.IO.stdout System.IO.utf8 #-}
{-# COMPILE GHC setStdoutNewlineMode = System.IO.hSetNewlineMode System.IO.stdout System.IO.universalNewlineMode #-}
{-# FOREIGN GHC import qualified System.Environment #-}
{-# COMPILE GHC privGetArgs = (do l <- System.Environment.getArgs; return (map Data.Text.pack l)) #-}
{-# FOREIGN GHC import qualified System.Directory #-}
{-# COMPILE GHC privForceFileRead = (\ contents -> seq (length (Data.Text.unpack contents)) (return ())) #-}
{-# COMPILE GHC privDoesFileExist = (\ s -> System.Directory.doesFileExist (Data.Text.unpack s)) #-}
{-# COMPILE GHC privCreateDirectoryIfMissing = (\ b s -> System.Directory.createDirectoryIfMissing b (Data.Text.unpack s)) #-}
{-# FOREIGN GHC import qualified System.FilePath #-}
{-# COMPILE GHC privTakeDirectory = (\ s -> Data.Text.pack (System.FilePath.takeDirectory (Data.Text.unpack s))) #-}
{-# COMPILE GHC privTakeFileName = (\ s -> Data.Text.pack (System.FilePath.takeFileName (Data.Text.unpack s))) #-}
{-# COMPILE GHC privCombineFileNames = (\ s1 s2 -> Data.Text.pack (System.FilePath.combine (Data.Text.unpack s1) (Data.Text.unpack s2))) #-}
{-# COMPILE GHC getLine = (Data.Text.IO.hGetLine System.IO.stdin) #-}
{-# COMPILE GHC privGetHomeDirectory = (do x <- System.Directory.getHomeDirectory; return (Data.Text.pack x)) #-}

getArgs : IO (𝕃 string)
getArgs = privGetArgs

doesFileExist : string → IO 𝔹
doesFileExist = privDoesFileExist

createDirectoryIfMissing : 𝔹 → string → IO ⊤
createDirectoryIfMissing = privCreateDirectoryIfMissing

takeDirectory : string → string
takeDirectory = privTakeDirectory

takeFileName : string → string
takeFileName = privTakeFileName

combineFileNames : string → string → string
combineFileNames = privCombineFileNames

forceFileRead : string {- the contents of the file, not the file name -} → IO ⊤
forceFileRead = privForceFileRead

getHomeDirectory : IO string
getHomeDirectory = privGetHomeDirectory

postulate
  fileIsOlder : string → string → IO 𝔹
  canonicalizePath : string → IO string
{-# COMPILE GHC fileIsOlder = (\ s1 s2 -> (System.Directory.getModificationTime (Data.Text.unpack s1)) >>= \ t1 -> (System.Directory.getModificationTime (Data.Text.unpack s2)) >>= \ t2 -> return (t1 < t2)) #-}
{-# COMPILE GHC canonicalizePath = (\ s -> do x <- System.Directory.canonicalizePath (Data.Text.unpack s); return (Data.Text.pack x)) #-}

----------------------------------------------------------------------
-- defined operations
----------------------------------------------------------------------

_>>_ : ∀ {A B : Set} → IO A → IO B → IO B
x >> y = x >>= (λ q -> y)

base-filenameh : 𝕃 char → 𝕃 char
base-filenameh [] = []
base-filenameh ('.' :: cs) = cs
base-filenameh (_ :: cs) = base-filenameh cs

-- return the part of the string up to the last (rightmost) period ('.'); so for "foo.txt" return "foo"
base-filename : string → string
base-filename s = 𝕃char-to-string (reverse (base-filenameh (reverse (string-to-𝕃char s))))

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


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

open import lib.Basics -- hiding (_=⟨_⟩_ ; _∎)
open import lib.types.Paths
open import lib.types.Pi
open import lib.types.Unit
open import lib.types.Nat
open import lib.types.TLevel
open import lib.types.Pointed
open import lib.types.Sigma
open import lib.NType2
open import lib.PathGroupoid

open import nicolai.pseudotruncations.Preliminary-definitions

module nicolai.pseudotruncations.Liblemmas where

-- transport along constant family
transport-const-fam : ∀ {i j} {A : Type i} {B : Type j} {a₁ a₂ : A}
                → (p : a₁ == a₂) → (b : B) → transport (λ _ → B) p b == b
transport-const-fam idp b = idp

-- interaction of transport and ap
trans-ap : ∀ {i j} {A : Type i} {B : Type j} {a₁ a₂ : A}
           → (f g : A → B) → (p : a₁ == a₂) → (q : f a₁ == g a₁)
           → transport (λ x → f x == g x) p q == ! (ap f p) ∙ q ∙ (ap g p)
trans-ap f g idp q = ! (∙-unit-r q)

-- special interaction of transport and ap, where the second map is constant at a point
trans-ap₁ : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) {a₁ a₂ : A} (b : B)
            (p : a₁ == a₂) (q : f a₁ == b)
            → transport (λ a → f a == b) p q == ! (ap f p) ∙ q
trans-ap₁ f b idp q = idp

-- first map is constant at a point
trans-ap₂ : ∀ {i j} {A : Type i} {B : Type j} (g : A → B) {a₁ a₂ : A} (b : B)
            (p : a₁ == a₂) (q : b == g a₁)
            → transport (λ a → b == g a) p q == q ∙ ap g p
trans-ap₂ g b idp q = !( ∙-unit-r _)

-- if f is weakly constant, then so is ap f
ap-const : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
           → wconst f → {a₁ a₂ : A} → wconst (ap f {x = a₁} {y = a₂})
ap-const {A = A} f wc p q = calc-ap p ∙ ! (calc-ap q) where
  calc-ap : {a₁ a₂ : A} → (p : a₁ == a₂) → ap f p == wc a₁ a₂ ∙ ! (wc a₂ a₂)
  calc-ap idp = ! (!-inv-r (wc _ _))

-- in particular, if f is weakly constant, then ap f maps loops to 'refl'
ap-const₁ : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
           → wconst f → {a₁ : A} → (p : a₁ == a₁) → ap f p == idp
ap-const₁ f wc p = ap-const f wc p idp

-- if f is constant at a point, it maps every path to 'refl'
ap-const-at-point : ∀ {i j} {A : Type i} {B : Type j} {a₁ a₂ : A}
                    (b : B) (p : a₁ == a₂) → ap (λ _ → b) p == idp
ap-const-at-point b idp = idp

{- this lemma is ad-hoc; it could be proved as a concatenation of
   many library lemmas, but it would be much more tedious to do -}
adhoc-lemma : ∀ {i} {A : Type i} {x y z : A}
                (p : x == y)
                (q : z == y)
                (r : z == x)
                → p ∙ ! q ∙ r == idp
                → p == ! r ∙ q
adhoc-lemma p idp idp e = ! (∙-unit-r p) ∙ e

{- If f is weakly constant, then so is ap f. This is a lemma from our
   old Hedberg article. -}
ap-wconst : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) (w : wconst f)
            → {a₁ a₂ : A} → wconst (ap f {a₁} {a₂})
ap-wconst f w p q = lemma p ∙ ! (lemma q) where
  lemma : ∀ {x y} (p : x == y) → ap f {x} {y} p == ! (w x x) ∙ (w x y)
  lemma {x} idp = ! (!-inv-l (w x x))

-- Silly little lemma (is it in the library?)
ap-fst : ∀ {i j} {A : Type i} {B : Type j} {a₁ a₂ : A} {b₁ b₂ : B}
           (p : a₁ == a₂) (q : b₁ == b₂)
           → ap fst (pair×= p q) == p
ap-fst idp idp = idp

{- An ad-hoc lemma. Whenever this appears, one could (should, to be honest)
   use library lemmas, but it's just so much more convenient to formulate it
   and pattern match... -}
adhoc-=-eqv : ∀ {i} {A : Type i} {x y : A} (p : y == x) (q : y == x)
                → (! p ∙ q == idp) ≃ (p == q)
adhoc-=-eqv idp  q = !-equiv

{- Another ad-hoc equality; it could be proved easily with many nested
   library lemmas -}
multi-cancelling : ∀ {i} {A : Type i} {x y z w : A} (p : y == x) (q : y == z) (r : x == w)
                   → (! p) ∙ q ∙ (! q) ∙ p ∙ r == r
multi-cancelling idp idp r = idp

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
-- self-contained notes following https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html and relevant parts of HoTT book

open import Agda.Primitive public
  using (Level ; _⊔_)
  renaming (Set to Type ; lzero to 𝓾₀ ; lsuc to _⁺)

variable
  𝓁 𝓂 𝓃 : Level

Π : {X : Type 𝓁} (A : X → Type 𝓂) → Type (𝓁 ⊔ 𝓂)
Π A = (x : _) → A x

id : {X : Type 𝓁} → X → X
id x = x

_∘_ : {X : Type 𝓁} {Y : Type 𝓂} {Z : Y → Type 𝓃}
  → ((y : Y) → Z y) → (f : X → Y) → (x : X) → Z (f x)
g ∘ f = λ x → g (f x)
{-# INLINE _∘_ #-}

infixr 50 _∘_

data ⊥ : Type where

⊥-induction : (A : ⊥ → Type 𝓁) → Π A
⊥-induction A ()

data ⊤ : Type where
  ⋆ : ⊤

⊤-induction : (A : ⊤ → Type 𝓁) → A ⋆ → Π A
⊤-induction A a ⋆ = a

data _+_ (X : Type 𝓁) (Y : Type 𝓂) : Type (𝓁 ⊔ 𝓂)  where
  inl : X → X + Y
  inr : Y → X + Y

+-induction : {X : Type 𝓁} {Y : Type 𝓂} (A : X + Y → Type 𝓃)
  → ((x : X) → A (inl x))
  → ((y : Y) → A (inr y))
  → Π A
+-induction A f g (inl x) = f x
+-induction A f g (inr y) = g y

𝟚 : Type
𝟚 = ⊤ + ⊤

pattern ₀ = inl ⋆
pattern ₁ = inr ⋆

record Σ {X : Type 𝓁} (Y : X → Type 𝓂) : Type (𝓁 ⊔ 𝓂) where
  constructor _,_
  field
    fst : X
    snd : Y fst

open Σ

Σ-induction : {X : Type 𝓁} {Y : X → Type 𝓂} (A : Σ Y → Type 𝓃)
  → ((x : X) (y : Y x) → A (x , y))
  → Π A
Σ-induction A f (x , y) = f x y

_×_ : Type 𝓁 → Type 𝓂 → Type (𝓁 ⊔ 𝓂)
X × Y = Σ (λ (_ : X) → Y)

data Id (X : Type 𝓁) (x : X) : X → Type 𝓁 where
  refl : Id X x x

Id-induction : {X : Type 𝓁} {x : X} (A : (y : X) → Id X x y → Type 𝓂)
  → A x refl
  → (y : X) (p : Id X x y) → A y p
Id-induction A σ _ refl = σ

data Id2 (X : Type 𝓁) : X → X → Type 𝓁 where
  refl2 : (x : X) → Id2 X x x

Id2-induction : {X : Type 𝓁} (A : (x y : X) → Id2 X x y → Type 𝓂)
  → ((x : X) → A x x (refl2 x))
  → (x y : X) (p : Id2 X x y) → A x y p
Id2-induction A σ x x (refl2 x) = σ x

Id→Id2 : {X : Type 𝓁} → (x y : X) → Id X x y → Id2 X x y
Id→Id2 x x refl = refl2 x

Id2→Id : {X : Type 𝓁} → (x y : X) → Id2 X x y → Id X x y
Id2→Id x x (refl2 x) = refl

_≡_ : {X : Type 𝓁} (x y : X) → Type 𝓁
x ≡ y = Id _ x y

infix 1 _≡_

sym : {X : Type 𝓁} {x y : X} → x ≡ y → y ≡ x
sym refl = refl

_∙_ : {X : Type 𝓁} {x y z : X} → x ≡ y → y ≡ z → x ≡ z
refl ∙ refl = refl

_∙∙_∙∙_ : {X : Type 𝓁} {x y z t : X} → x ≡ y → y ≡ z → z ≡ t → x ≡ t
refl ∙∙ refl ∙∙ refl = refl

_≡⟨_⟩_ : {X : Type 𝓁 } (x : X) {y z : X} → x ≡ y → y ≡ z → x ≡ z
x ≡⟨ p ⟩ q = p ∙ q

infixr  0 _≡⟨_⟩_

_∎ : {X : Type 𝓁} (x : X) → x ≡ x
x ∎ = refl

infix 1 _∎

transport : {X Y : Type 𝓁} → X ≡ Y → X → Y
transport refl x = x

subst : {X : Type 𝓁} (A : X → Type 𝓂) {x y : X} → x ≡ y → A x → A y
subst A refl ax = ax

module _ {X : Type 𝓁} {x : X} where
  refl-left : {y : X} (p : x ≡ y) → refl ∙ p ≡ p
  refl-left refl = refl

  refl-right : {y : X} (p : x ≡ y) → p ∙ refl ≡ p
  refl-right refl = refl

  ∙-assoc : {y z t : X} (p : x ≡ y) (q : y ≡ z) (r : z ≡ t)
    → (p ∙ q) ∙ r ≡ p ∙ (q ∙ r)
  ∙-assoc refl refl refl = refl

  sym-left : {y : X} (p : x ≡ y) → sym p ∙ p ≡ refl
  sym-left refl = refl

  sym-right : {y : X} (p : x ≡ y) → p ∙ sym p ≡ refl
  sym-right refl = refl

  sym-involutive : {y : X} (p : x ≡ y) → sym (sym p) ≡ p
  sym-involutive refl = refl

∙-cancel-left : {X : Type 𝓁} {x y z : X} {p : x ≡ y} {q r : y ≡ z}
  → p ∙ q ≡ p ∙ r → q ≡ r
∙-cancel-left {p = refl} {q = q} {r = r} s =
  sym (refl-left q) ∙∙ s ∙∙ refl-left r

∙-cancel-right : {X : Type 𝓁} {x y z : X} {p q : x ≡ y} {r : y ≡ z}
  → p ∙ r ≡ q ∙ r → p ≡ q
∙-cancel-right {p = p} {q = q} {r = refl} s =
  sym (refl-right p) ∙∙ s ∙∙ refl-right q

module _ {X : Type 𝓁} {Y : Type 𝓂} (f : X → Y) where
  cong : {x y : X} → x ≡ y → f x ≡ f y
  cong refl = refl

  cong-refl : (x : X) → cong (refl {x = x}) ≡ refl
  cong-refl x = refl

  cong-sym : {x y : X} → (p : x ≡ y) → cong (sym p) ≡ sym (cong p)
  cong-sym refl = refl

  cong-∙ : {x y z : X} (p : x ≡ y) (q : y ≡ z)
    → cong (p ∙ q) ≡ cong p ∙ cong q
  cong-∙ refl refl = refl

cong-id : {X : Type 𝓁} {x y : X} (p : x ≡ y) → cong id p ≡ p
cong-id refl = refl

cong-∘ : {X : Type 𝓁} {Y : Type 𝓂} {Z : Type 𝓃}
  (f : X → Y) (g : Y → Z) {x y : X} (p : x ≡ y)
  → cong (g ∘ f) p ≡ cong g (cong f p)
cong-∘ f g refl = refl

congd : {X : Type 𝓁} {Y : X → Type 𝓂} (f : Π Y) {x y : X} (p : x ≡ y)
  → subst Y p (f x) ≡ f y
congd f refl = refl

cong₂ : {X : Type 𝓁} {Y : Type 𝓂} {Z : Type 𝓃} (f : X → Y → Z)
  {x x' : X} → x ≡ x' → {y y' : Y} → y ≡ y' → f x y ≡ f x' y'
cong₂ f refl refl = refl

¬_ : Type 𝓁 → Type 𝓁
¬ A = A → ⊥

contrapositive : {X : Type 𝓁} {Y : Type 𝓂} → (X → Y) → ¬ Y → ¬ X
contrapositive f p x = p (f x)

decidable : Type 𝓁 → Type 𝓁
decidable A = A + (¬ A)

onAllPaths : (Type 𝓁 → Type 𝓁) → Type 𝓁 → Type 𝓁
onAllPaths A X = (x y : X) → A (x ≡ y)

discrete : Type 𝓁 → Type 𝓁
discrete = onAllPaths decidable

₁≢₀ : ¬ (₁ ≡ ₀)
₁≢₀ p = subst (λ { ₀ → ⊥ ; ₁ → ⊤ }) p ⋆

𝟚-is-discrete : discrete 𝟚
𝟚-is-discrete ₀ ₀ = inl refl
𝟚-is-discrete ₀ ₁ = inr (contrapositive sym ₁≢₀)
𝟚-is-discrete ₁ ₀ = inr ₁≢₀
𝟚-is-discrete ₁ ₁ = inl refl

isCenter : (X : Type 𝓁) → X → Type 𝓁
isCenter X x = (y : X) → x ≡ y

isContr : (X : Type 𝓁) → Type 𝓁
isContr X = Σ (isCenter X)

⊤-is-contr : isContr ⊤
⊤-is-contr = ⋆ , λ { ⋆ → refl }

surrounding : {X : Type 𝓁} (x : X) → Type 𝓁
surrounding x = Σ λ y → x ≡ y

surrounding-is-contr : {X : Type 𝓁} (x : X) → isContr (surrounding x)
surrounding-is-contr x = (x , refl) ,  λ { (.x , refl) → refl }

isProp : (X : Type 𝓁) → Type 𝓁
isProp X = Π (isCenter X)

⊥-is-prop : isProp ⊥
⊥-is-prop ()

⊤-is-prop : isProp ⊤
⊤-is-prop ⋆ ⋆ = refl

isContr→isProp : {X : Type 𝓁} → isContr X → isProp X
isContr→isProp (c , φ) x y = sym (φ x) ∙ φ y

no-unicorns : (X : Type 𝓁) → isProp X → ¬ (isContr X) → ¬ ¬ X → ⊥
no-unicorns X φ ns ne = ne empty where
  empty : ¬ X
  empty x = ns (x , φ x)

isSet : (X : Type 𝓁) → Type 𝓁
isSet = onAllPaths isProp

⊥-is-set : isSet ⊥
⊥-is-set ()

⊤-is-set : isSet ⊤
⊤-is-set ⋆ ⋆ refl refl = refl

⊤-is-set' : isSet ⊤
⊤-is-set' =
  ⊤-induction
    (λ x → (z : ⊤) → isProp (x ≡ z))
    (Id-induction
      (λ y → isCenter (⋆ ≡ y))
      (Id-induction
        refl-eq
        refl
        ⋆))
  where
  refl-eq : (x : ⊤) → ⋆ ≡ x → Type
  refl-eq =
    ⊤-induction
      (λ x → ⋆ ≡ x → Type)
      (Id (⋆ ≡ ⋆) refl)

wconstant : {X : Type 𝓁} {Y : Type 𝓂} → (X → Y) → Type (𝓁 ⊔ 𝓂)
wconstant {X = X} f = (x y : X) → f x ≡ f y

endo : Type 𝓁 → Type 𝓁
endo X = X → X

wconstant-endo : Type 𝓁 → Type 𝓁
wconstant-endo X = Σ λ (f : endo X) → wconstant f

Hedberg : {X : Type 𝓁} (x : X)
  → ((y : X) → wconstant-endo (x ≡ y))
  → (y : X) → isProp (x ≡ y)
Hedberg {X = X} x c y p q =
  p
  ≡⟨ sym (a y p) ⟩
  sym (f x refl) ∙ f y p
  ≡⟨ cong (λ r → sym (f x refl) ∙ r) (c y .snd p q) ⟩
  sym (f x refl) ∙ f y q
  ≡⟨ a y q ⟩
  q ∎
  where
  f : (z : X) → endo (x ≡ z)
  f z = c z .fst

  a : (z : X) (r : x ≡ z) → sym (f x refl) ∙ f z r ≡ r
  a x refl = sym-left (f x refl)

isProp→wconstant-endos : {X : Type 𝓁}
  → isProp X → onAllPaths wconstant-endo X
isProp→wconstant-endos φ x y = (λ _ → φ x y) , (λ _ _ → refl)

isSet→wconstant-endos : {X : Type 𝓁}
  → isSet X → onAllPaths wconstant-endo X
isSet→wconstant-endos φ x y = id , φ x y

wconstant-endos→isSet : {X : Type 𝓁}
  → onAllPaths wconstant-endo X → isSet X
wconstant-endos→isSet c x = Hedberg x (c x)

isProp→isSet : {X : Type 𝓁} → isProp X → isSet X
isProp→isSet = wconstant-endos→isSet ∘ isProp→wconstant-endos

pointed→wconstant-endo : {X : Type 𝓁} → X → wconstant-endo X
pointed→wconstant-endo x = (λ _ → x) , (λ _ _ → refl)

empty→wconstant-endo : {X : Type 𝓁} → ¬ X → wconstant-endo X
empty→wconstant-endo e = id , λ x → ⊥-induction _ (e x)

decidable→wconstant-endo : {X : Type 𝓁} → decidable X → wconstant-endo X
decidable→wconstant-endo (inl x) = pointed→wconstant-endo x
decidable→wconstant-endo (inr e) = empty→wconstant-endo e

discrete→wconstant-endos : {X : Type 𝓁}
  → discrete X → onAllPaths wconstant-endo X
discrete→wconstant-endos φ x y = decidable→wconstant-endo (φ x y)

discrete→isSet : {X : Type 𝓁} → discrete X → isSet X
discrete→isSet = wconstant-endos→isSet ∘ discrete→wconstant-endos

isContrΣ : {X : Type 𝓁} {Y : X → Type 𝓂}
  → isContr X → ((x : X) → isContr (Y x))
  → isContr (Σ Y)
isContrΣ {X = X} {Y = Y} (x₀ , c) cy =
  (x₀ , cy x₀ .fst) , λ { (x , y) → f (c x) (cy x .snd y) }
  where
  f : {x : X} {y : Y x} → x₀ ≡ x → cy x .fst ≡ y → (x₀ , cy x₀ .fst) ≡ (x , y)
  f refl refl = refl

isPropΣ : {X : Type 𝓁} {Y : X → Type 𝓂}
  → isProp X → ((x : X) → isProp (Y x))
  → isProp (Σ Y)
isPropΣ {X = X} {Y = Y} φ ψ (x₀ , y₀) (x₁ , y₁) =
  f (φ x₀ x₁) (ψ x₁ (subst Y (φ x₀ x₁) y₀) y₁)
  where
  f : {x : X} {y : Y x} → (p : x₀ ≡ x) → subst Y p y₀ ≡ y → (x₀ , y₀) ≡ (x , y)
  f refl refl = refl

_∼_ : {X : Type 𝓁} {Y : X → Type 𝓂} (f g : Π Y) → Type (𝓁 ⊔ 𝓂)
f ∼ g = (x : _) → f x ≡ g x

infix 2 _∼_

deformation-induces-natural-iso : {X : Type 𝓁}
  {f : X → X} (H : f ∼ id)
  {x y : X} (p : x ≡ y)
  → H x ∙ p ≡ cong f p ∙ H y
deformation-induces-natural-iso H {x = x} refl =
  refl-right (H x) ∙ sym (refl-left (H x))

deformation-induces-iso : {X : Type 𝓁} (f : X → X) (H : f ∼ id)
  (x : X) → H (f x) ≡ cong f (H x)
deformation-induces-iso f H x =
 ∙-cancel-right (deformation-induces-natural-iso H (H x))

retraction : {X : Type 𝓁} {Y : Type 𝓂} → (X → Y) → Type (𝓁 ⊔ 𝓂)
retraction f = Σ λ g → g ∘ f ∼ id

section : {X : Type 𝓁} {Y : Type 𝓂} → (X → Y) → Type (𝓁 ⊔ 𝓂)
section f = Σ λ h → f ∘ h ∼ id

_◁_ : Type 𝓁 → Type 𝓂 → Type (𝓁 ⊔ 𝓂)
X ◁ Y = Σ λ (r : Y → X) → section r

isContrRetract : {X : Type 𝓁} {Y : Type 𝓂}
  → Y ◁ X → isContr X → isContr Y
isContrRetract {Y = Y} (r , (s , η)) (c , φ) = r c , d
  where
  d : isCenter Y (r c)
  d y = r c ≡⟨ cong r (φ (s y)) ⟩ r (s y) ≡⟨ η y ⟩ y ∎

isPropRetract : {X : Type 𝓁} {Y : Type 𝓂}
  → Y ◁ X → isProp X → isProp Y
isPropRetract {Y = Y} (r , (s , η)) φ y₀ y₁ =
  y₀
  ≡⟨ sym (η y₀) ⟩
  r (s y₀)
  ≡⟨ cong r (φ (s y₀) (s y₁)) ⟩
  r (s y₁)
  ≡⟨ η y₁ ⟩
  y₁ ∎

Σ-retract : {X : Type 𝓁} (A : X → Type 𝓂) (B : X → Type 𝓃)
  → ((x : X) → A x ◁ B x) → Σ A ◁ Σ B
Σ-retract A B ρ = r , (s , η)
  where
  r : Σ B → Σ A
  r (x , b) = x , (ρ x .fst b)

  s : Σ A → Σ B
  s (x , a) = x , ρ x .snd .fst a

  η : r ∘ s ∼ id
  η (x , a) = cong (_,_ x) (ρ x .snd .snd a)

subst-is-retraction : {X : Type 𝓁} (A : X → Type 𝓂) {x y : X} (p : x ≡ y)
  → subst A p ∘ subst A (sym p) ∼ id
subst-is-retraction A refl ay = refl

subst-is-section : {X : Type 𝓁} (A : X → Type 𝓂) {x y : X} (p : x ≡ y)
  → subst A (sym p) ∘ subst A p ∼ id
subst-is-section A refl ax = refl

module _ {X : Type 𝓁} {A : X → Type 𝓃} where
  to-Σ≡ : {σ τ : Σ A}
    →  Σ (λ (p : σ .fst ≡ τ .fst) → subst A p (σ .snd) ≡ τ .snd)
    → σ ≡ τ
  to-Σ≡ (refl , refl) = refl

  from-Σ≡ : {σ τ : Σ A}
    → σ ≡ τ
    →  Σ (λ (p : σ .fst ≡ τ .fst) → subst A p (σ .snd) ≡ τ .snd)
  from-Σ≡ refl = (refl , refl)

  to-Σ≡-is-retraction :  {σ τ : Σ A} → to-Σ≡ {σ} {τ} ∘ from-Σ≡ {σ} {τ} ∼ id
  to-Σ≡-is-retraction refl = refl

  to-Σ≡-is-section :  {σ τ : Σ A} → from-Σ≡ {σ} {τ} ∘ to-Σ≡ {σ} {τ} ∼ id
  to-Σ≡-is-section (refl , refl) = refl

  isSetΣ : isSet X → ((x : X) → isSet (A x)) → isSet (Σ A)
  isSetΣ φ ψ (x₀ , y₀) (x₁ , y₁) =
    isPropRetract
      (to-Σ≡ , (from-Σ≡ , to-Σ≡-is-retraction))
      (isPropΣ (φ x₀ x₁) (λ x → ψ x₁ (subst A x y₀) y₁))

Σ-reindexing-retract : {X : Type 𝓁} {Y : Type 𝓂} (A : X → Type 𝓃) (r : Y → X)
  → section r
  → Σ A ◁ Σ (A ∘ r)
Σ-reindexing-retract A r (s , η) = r' , (s' , η')
  where
  r' : Σ (A ∘ r) → Σ A
  r' (y , a) = r y , a

  s' : Σ A → Σ (A ∘ r)
  s' (x , a) = s x , subst A (sym (η x)) a

  η' : r' ∘ s' ∼ id
  η' (x , a) = to-Σ≡ (η x , subst-is-retraction A (η x) a)

module Equiv {X : Type 𝓁} {Y : Type 𝓂} (f : X → Y) where
  fiber : Y → Type (𝓁 ⊔ 𝓂)
  fiber y = Σ λ x → f x ≡ y

  isEquiv : Type (𝓁 ⊔ 𝓂)
  isEquiv = (y : Y) → isContr (fiber y)

  inverse : isEquiv → Y → X
  inverse eq y = eq y .fst .fst

  inverse-is-section : (eq : isEquiv) → f ∘ inverse eq ∼ id
  inverse-is-section eq y = eq y .fst .snd

  inverse-is-retraction : (eq : isEquiv) → inverse eq ∘ f ∼ id
  inverse-is-retraction eq x = cong fst p where
    p : Id (fiber (f x)) (eq (f x) .fst) (x , refl)
    p = eq (f x) .snd (x , refl)

  isInvertible : Type (𝓁 ⊔ 𝓂)
  isInvertible = retraction f × section f

  isEquiv→isInvertible : isEquiv → isInvertible
  isEquiv→isInvertible eq =
    (inverse eq , inverse-is-retraction eq)
    , (inverse eq , inverse-is-section eq)

  toFiberEq : {y : Y} {σ : fiber y} (τ : fiber y)
    →  Σ (λ (γ : σ .fst ≡ τ .fst) → (cong f γ ∙ τ .snd ≡ σ .snd))
    → σ ≡ τ
  toFiberEq τ (refl , refl) = cong (λ p → (τ .fst , p)) (refl-left (τ .snd))

  record isHAEquiv : Type (𝓁 ⊔ 𝓂) where
    field
      g : Y → X
      η : g ∘ f ∼ id
      ε : f ∘ g ∼ id
      ha : (x : X) → cong f (η x) ≡ ε (f x)

  open isHAEquiv

  isHAEquiv→isInvertible : isHAEquiv → isInvertible
  isHAEquiv→isInvertible eq = (eq .g , eq .η) , (eq .g , eq .ε)

  isInvertible→isHAEquiv : isInvertible → isHAEquiv
  isInvertible→isHAEquiv ((g₀ , η₀) , (h₀ , ε₀)) = record {
      g = g₀
      ; η = η₀
      ; ε = ε₂
      ; ha = λ x → sym (ha₀ x)
    } where
    ε₁ : f ∘ g₀ ∼ id
    ε₁ y = sym (cong (f ∘ g₀) (ε₀ y)) ∙ (cong f (η₀ (h₀ y)) ∙ ε₀ y)

    ε₂ : f ∘ g₀ ∼ id
    ε₂ y = sym (ε₁ (f (g₀ y))) ∙ (cong f (η₀ (g₀ y)) ∙ ε₁ y)

    ha₀ : (x : X) →  ε₂ (f x) ≡ cong f (η₀ x)
    ha₀ x =
      sym (ε₁ (f (g₀ (f x)))) ∙ (cong f (η₀ (g₀ (f x))) ∙ ε₁ (f x))
      ≡⟨ cong (λ p → sym (ε₁ (f (g₀ (f x)))) ∙ p)
        (
          cong f (η₀ (g₀ (f x))) ∙ ε₁ (f x)
          ≡⟨ cong (λ p → cong f p ∙ ε₁ (f x))
            (deformation-induces-iso (g₀ ∘ f) η₀ x) ⟩
          cong f (cong (g₀ ∘ f) (η₀ x)) ∙ ε₁ (f x)
          ≡⟨ cong (λ p → p ∙ ε₁ (f x))
            (
              cong f (cong (g₀ ∘ f) (η₀ x))
              ≡⟨ sym (cong-∘ (g₀ ∘ f) f (η₀ x)) ⟩
              cong (f ∘ g₀ ∘ f) (η₀ x)
              ≡⟨ cong-∘ f (f ∘ g₀) (η₀ x) ⟩
              cong (f ∘ g₀) (cong f (η₀ x)) ∎ ) ⟩
          cong (f ∘ g₀) (cong f (η₀ x)) ∙ ε₁ (f x)
          ≡⟨ sym (deformation-induces-natural-iso ε₁ (cong f (η₀ x))) ⟩
          ε₁ (f (g₀ (f x))) ∙ cong f (η₀ x) ∎ )
      ⟩
      sym (ε₁ (f (g₀ (f x)))) ∙ (ε₁ (f (g₀ (f x))) ∙ cong f (η₀ x))
      ≡⟨ sym (∙-assoc _ _ _) ⟩
      (sym (ε₁ (f (g₀ (f x)))) ∙ ε₁ (f (g₀ (f x)))) ∙ cong f (η₀ x)
      ≡⟨  cong (λ p → p ∙ cong f (η₀ x)) (sym-left _) ⟩
      refl ∙ cong f (η₀ x)
      ≡⟨ refl-left _ ⟩
      cong f (η₀ x) ∎

  isHAEquiv→isEquiv : isHAEquiv → isEquiv
  isHAEquiv→isEquiv eq y =
    (eq .g y , eq .ε y)
    , λ τ → toFiberEq τ (γ τ , lem τ)
    where
    γ : (τ : fiber y) → eq .g y ≡ τ .fst
    γ (x , p) = cong (eq .g) (sym p) ∙ eq .η x

    natural : {h : Y → Y} (e : h ∼ id) {z z' : Y} (q : z ≡ z')
      → (sym (cong h q) ∙ e z) ∙ q ≡ e z'
    natural e {z = z} refl  = refl-right (refl ∙ e z) ∙ refl-left (e z)

    lem : (τ : fiber y) → cong f (γ τ) ∙ τ .snd ≡ eq .ε y
    lem (x , p) =
       cong f (cong (eq .g) (sym p) ∙ eq .η x) ∙ p
       ≡⟨ cong (λ q → q ∙ p)
         (
           cong f (cong (eq .g) (sym p) ∙ eq .η x)
           ≡⟨ cong-∙ f (cong (eq .g) (sym p)) (eq .η x) ⟩
           cong f (cong (eq .g) (sym p)) ∙ cong f (eq .η x)
           ≡⟨ cong₂ _∙_
              (sym (cong-∘ (eq .g) f (sym p)) ∙ cong-sym (f ∘ eq .g) p)
              (eq .ha x) ⟩
           sym (cong (f ∘ eq .g) p) ∙ eq .ε (f x) ∎ ) ⟩
       (sym (cong (f ∘ eq .g) p) ∙ eq .ε (f x)) ∙ p
       ≡⟨ natural (eq .ε) p ⟩
       eq .ε y ∎

open Equiv
open isHAEquiv

_≃_ : Type 𝓁 → Type 𝓂 → Type (𝓁 ⊔ 𝓂)
X ≃ Y = Σ λ (f : (X → Y)) → isHAEquiv f

idIsHAEquiv : (X : Type 𝓁) → isHAEquiv (id {X = X})
idIsHAEquiv X = record {
  g = id
  ; η = λ x → refl
  ; ε = λ x → refl
  ; ha = λ x → refl }

id-≃ : (X : Type 𝓁) → X ≃ X
id-≃ X = (id , idIsHAEquiv X)

∘-≃ : {X : Type 𝓁} {Y : Type 𝓂} {Z : Type 𝓃} → X ≃ Y → Y ≃ Z → X ≃ Z
∘-≃ {X = X} {Y = Y} {Z = Z} (f , eqf) (h , eqh) =
  (h ∘ f)
  , record { g = g₀ ; η = η₀ ; ε = ε₀ ; ha = ha₀ }
  where
  g₀ : Z → X
  g₀ = eqf .g ∘ eqh .g

  η₀ : g₀ ∘ (h ∘ f) ∼ id
  η₀ x = cong (eqf .g) (eqh .η (f x)) ∙ eqf .η x

  ε₀ : (h ∘ f) ∘ g₀ ∼ id
  ε₀ z = cong h (eqf .ε (eqh .g z)) ∙ eqh .ε z

  ha₀ : (x : X) → cong (h ∘ f) (η₀ x) ≡ ε₀ (h (f x))
  ha₀ x =
    cong (h ∘ f) (cong (eqf .g) (eqh .η (f x)) ∙ eqf .η x)
    ≡⟨ cong-∙ (h ∘ f) _ _ ⟩
    cong (h ∘ f) (cong (eqf .g) (eqh .η (f x))) ∙ cong (h ∘ f) (eqf .η x)
    ≡⟨ cong₂ _∙_
       (sym (cong-∘ (eqf .g) (h ∘ f) (eqh .η (f x))))
       (cong-∘ f h (eqf .η x)) ⟩
    cong (h ∘ f ∘ eqf .g) (eqh .η (f x)) ∙ cong h (cong f (eqf .η x))
    ≡⟨ cong₂ _∙_
       (cong-∘ (f ∘ eqf .g) h (eqh .η (f x)))
       (cong (cong h) (eqf .ha x)) ⟩
    cong h (cong (f ∘ eqf .g) (eqh .η (f x))) ∙ cong h (eqf .ε (f x))
    ≡⟨ sym (cong-∙ h _ _) ⟩
    cong h (cong (f ∘ eqf .g) (eqh .η (f x)) ∙ eqf .ε (f x))
    ≡⟨ cong (cong h) (sym (deformation-induces-natural-iso (eqf .ε) (eqh .η (f x)))) ⟩
    cong h (eqf .ε (eqh .g (h (f x))) ∙ eqh .η (f x))
    ≡⟨ cong-∙ h _ _ ⟩
    cong h (eqf .ε (eqh .g (h (f x)))) ∙ cong h (eqh .η (f x))
    ≡⟨ cong (λ p → _ ∙ p) (eqh .ha (f x)) ⟩
    cong h (eqf .ε (eqh .g (h (f x)))) ∙ eqh .ε (h (f x)) ∎

sym-≃ : {X : Type 𝓁} {Y : Type 𝓂} → X ≃ Y → Y ≃ X
sym-≃ {X = X} {Y = Y} (f , eq) =
  eq .g , record { g = f ; η = eq .ε ; ε = eq .η ; ha = ha₀ }
  where
  p : (y : Y)
    → cong (eq .g ∘ f ∘ eq .g) (eq .ε y) ∙ eq .η (eq .g y)
    ≡ cong (eq .g ∘ f ∘ eq .g) (eq .ε y) ∙ cong (eq .g) (eq .ε y)
  p y =
    cong (eq .g ∘ f ∘ eq .g) (eq .ε y) ∙ eq .η (eq .g y)
    ≡⟨ cong (λ p → p ∙ _) (cong-∘ (eq .g) (eq .g ∘ f) (eq .ε y)) ⟩
    cong (eq .g ∘ f) (cong (eq .g) (eq .ε y)) ∙ eq .η (eq .g y)
    ≡⟨ sym (deformation-induces-natural-iso (eq .η) (cong (eq .g) (eq .ε y))) ⟩
    eq .η (eq .g (f (eq .g y))) ∙ cong (eq .g) (eq .ε y)
    ≡⟨ cong (λ p → p ∙ _) (deformation-induces-iso (eq .g ∘ f) (eq .η) (eq .g y)) ⟩
    cong (eq .g ∘ f) (eq .η (eq .g y)) ∙ cong (eq .g) (eq .ε y)
    ≡⟨ cong (λ p → p ∙ cong (eq .g) (eq .ε y)) (cong-∘ f (eq .g) (eq .η (eq .g y))) ⟩
    cong (eq .g) (cong f (eq .η (eq .g y))) ∙ cong (eq .g) (eq .ε y)
    ≡⟨ cong (λ p → cong (eq .g) p ∙ cong (eq .g) (eq .ε y)) (eq .ha (eq .g y)) ⟩
    cong (eq .g) (eq .ε (f (eq .g y))) ∙ cong (eq .g) (eq .ε y)
    ≡⟨ sym (cong-∙ (eq .g) (eq .ε (f (eq .g y))) (eq .ε y)) ⟩
    cong (eq .g) (eq .ε (f (eq .g y)) ∙ eq .ε y)
    ≡⟨ cong (cong (eq .g)) (deformation-induces-natural-iso (eq .ε) (eq .ε y)) ⟩
    cong (eq .g) (cong (f ∘ eq .g) (eq .ε y) ∙ eq .ε y)
    ≡⟨ cong-∙ (eq .g) (cong (f ∘ eq .g) (eq .ε y)) (eq .ε y) ⟩
    cong (eq .g) (cong (f ∘ eq .g) (eq .ε y)) ∙ cong (eq .g) (eq .ε y)
    ≡⟨ cong (λ p → p ∙ cong (eq .g) (eq .ε y)) (sym (cong-∘ (f ∘ eq .g) (eq .g) (eq .ε y))) ⟩
    cong (eq .g ∘ f ∘ eq .g) (eq .ε y) ∙ cong (eq .g) (eq .ε y) ∎

  ha₀ :  (y : Y) → cong (eq .g) (eq .ε y) ≡ eq .η (eq .g y)
  ha₀ y = ∙-cancel-left (sym (p y))

cong-const : {X : Type 𝓁} {Y : Type 𝓂} (y : Y) {x x' : X} {p : x ≡ x'}
  → cong (λ _ → y) p ≡ refl
cong-const y {p = refl} = refl

contr-fiber : {X : Type 𝓁} (A : X → Type 𝓂) → ((x : X) → isContr (A x))
  → isHAEquiv (λ (a : Σ A) → a .fst)
contr-fiber {X = X} A c = record { g = g₀ ; η = η₀ ; ε = ε₀ ; ha = ha₀ }
  where
  g₀ : X → Σ A
  g₀ x = x , c x .fst

  η₀ : g₀ ∘ fst ∼ id
  η₀ (x , a) = cong (_,_ x) (c x .snd a)

  ε₀ : fst ∘ g₀ ∼ id
  ε₀ x = refl

  ha₀ : (a : Σ A) → cong fst (η₀ a) ≡ ε₀ (fst a)
  ha₀ (x , a) = cong fst (cong (_,_ x) (c x .snd a))
    ≡⟨ sym (cong-∘ (_,_ x) fst (c x .snd a)) ⟩
    cong (λ _ → x) (c x .snd a)
    ≡⟨ cong-const x ⟩
    refl
    ≡⟨ refl ⟩
    ε₀ x ∎

Id→Eq : (X Y : Type 𝓁) → X ≡ Y → X ≃ Y
Id→Eq X X refl = id-≃ X

isUnivalent : (𝓁 : Level) → Type (𝓁 ⁺)
isUnivalent 𝓁 = (X Y : Type 𝓁) → isHAEquiv (Id→Eq X Y)

max_stars_repo_name: howsiyu/hott-notes

max_issues_repo_name: howsiyu/hott-notes

max_forks_repo_name: howsiyu/hott-notes


text:
module Numeral.Natural.Relation.Properties where

import Lvl
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Logic.Predicate
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Induction
open import Numeral.Natural.Relation
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Function.Domain
open import Structure.Operator.Properties
open import Structure.Relator.Ordering
open import Structure.Relator.Properties
open import Type

[ℕ]-zero-or-nonzero : ∀{n : ℕ} → (n ≡ 𝟎)∨(n ≢ 𝟎)
[ℕ]-zero-or-nonzero {𝟎}    = [∨]-introₗ [≡]-intro
[ℕ]-zero-or-nonzero {𝐒(_)} = [∨]-introᵣ \()

[≡][ℕ]-excluded-middle : ∀{a b : ℕ} → (a ≡ b)∨(a ≢ b)
[≡][ℕ]-excluded-middle {𝟎}   {𝟎}    = [∨]-introₗ [≡]-intro
[≡][ℕ]-excluded-middle {𝟎}   {𝐒(_)} = [∨]-introᵣ \()
[≡][ℕ]-excluded-middle {𝐒(_)}{𝟎}    = [∨]-introᵣ \()
[≡][ℕ]-excluded-middle {𝐒(a)}{𝐒(b)} = [∨]-elim ([∨]-introₗ ∘ [≡]-with(𝐒)) ([∨]-introᵣ ∘ (contrapositiveᵣ(injective(𝐒)))) ([≡][ℕ]-excluded-middle {a}{b})

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:
{-# OPTIONS --safe #-}

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Weakening {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.MaybeEmbed
open import Definition.LogicalRelation.Substitution.Introductions.Universe

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Weakening of valid types by one.
wk1ᵛ : ∀ {A F rA rF Γ l l'}
      ([Γ] : ⊩ᵛ Γ)
      ([F] : Γ ⊩ᵛ⟨ l' ⟩ F ^ rF / [Γ])
    → Γ ⊩ᵛ⟨ l ⟩ A ^ rA / [Γ]
    → Γ ∙ F ^ rF ⊩ᵛ⟨ l ⟩ wk1 A ^ rA / ([Γ] ∙ [F])
wk1ᵛ {A} [Γ] [F] [A] ⊢Δ [σ] =
  let [σA] = proj₁ ([A] ⊢Δ (proj₁ [σ]))
      [σA]′ = irrelevance′ (PE.sym (subst-wk A)) [σA]
  in  [σA]′
  ,   (λ [σ′] [σ≡σ′] →
         irrelevanceEq″ (PE.sym (subst-wk A))
                        (PE.sym (subst-wk A)) PE.refl PE.refl
                        [σA] [σA]′
                        (proj₂ ([A] ⊢Δ (proj₁ [σ])) (proj₁ [σ′]) (proj₁ [σ≡σ′])))

-- Weakening of valid type equality by one.
wk1Eqᵛ : ∀ {A B F rA rF Γ l l'}
         ([Γ] : ⊩ᵛ Γ)
         ([F] : Γ ⊩ᵛ⟨ l' ⟩ F ^ rF / [Γ])
         ([A] : Γ ⊩ᵛ⟨ l ⟩ A ^ rA / [Γ])
         ([A≡B] : Γ ⊩ᵛ⟨ l ⟩ A ≡ B ^ rA / [Γ] / [A])
       → Γ ∙ F ^ rF ⊩ᵛ⟨ l ⟩ wk1 A ≡ wk1 B ^ rA / [Γ] ∙ [F] / wk1ᵛ {A} {F} [Γ] [F] [A]
wk1Eqᵛ {A} {B} [Γ] [F] [A] [A≡B] ⊢Δ [σ] =
  let [σA] = proj₁ ([A] ⊢Δ (proj₁ [σ]))
      [σA]′ = irrelevance′ (PE.sym (subst-wk A)) [σA]
  in  irrelevanceEq″ (PE.sym (subst-wk A))
                     (PE.sym (subst-wk B)) PE.refl PE.refl
                     [σA] [σA]′
                     ([A≡B] ⊢Δ (proj₁ [σ]))

-- Weakening of valid term as a type by one.
wk1ᵗᵛ : ∀ {F G rF rG lG Γ l'}
         ([Γ] : ⊩ᵛ Γ)
         ([F] : Γ ⊩ᵛ⟨ l' ⟩ F ^ rF / [Γ]) →
       let l    = ∞
           [UG] = maybeEmbᵛ {A = Univ rG _} [Γ] (Uᵛ (proj₂ (levelBounded lG)) [Γ])
           [wUG] = maybeEmbᵛ {A = Univ rG _} (_∙_ {A = F} [Γ] [F]) (λ {Δ} {σ} → Uᵛ (proj₂ (levelBounded lG)) (_∙_ {A = F} [Γ] [F])  {Δ} {σ})
       in Γ ⊩ᵛ⟨ l ⟩ G ∷ Univ rG lG ^ [ ! , next lG ] / [Γ] / [UG] →
          Γ ∙ F ^ rF ⊩ᵛ⟨ l ⟩ wk1 G ∷ Univ rG lG ^ [ ! , next lG ] / ([Γ] ∙ [F]) / (λ {Δ} {σ} → [wUG] {Δ} {σ})
wk1ᵗᵛ {F} {G} {rF} {rG} {lG} [Γ] [F] [G]ₜ {Δ} {σ} ⊢Δ [σ] =
  let l    = ∞
      [UG] = maybeEmbᵛ {A = Univ rG _} [Γ] (Uᵛ (proj₂ (levelBounded lG)) [Γ])
      [wUG] = maybeEmbᵛ {A = Univ rG _} (_∙_ {A = F} [Γ] [F]) (λ {Δ} {σ} → Uᵛ (proj₂ (levelBounded lG)) (_∙_ {A = F} [Γ] [F])  {Δ} {σ})
      [σG] = proj₁ ([G]ₜ ⊢Δ (proj₁ [σ]))
      [Geq] = PE.sym (subst-wk G)
      [σG]′ = irrelevanceTerm″ PE.refl PE.refl PE.refl [Geq] (proj₁ ([UG] ⊢Δ (proj₁ [σ]))) (proj₁ ([wUG] {Δ} {σ} ⊢Δ [σ])) [σG]
  in  [σG]′
  ,   (λ [σ′] [σ≡σ′] →
         irrelevanceEqTerm″ PE.refl PE.refl
                            (PE.sym (subst-wk G))
                            (PE.sym (subst-wk G)) PE.refl
                            (proj₁ ([UG] ⊢Δ (proj₁ [σ]))) (proj₁ ([wUG] {Δ} {σ} ⊢Δ [σ]))
                            (proj₂ ([G]ₜ ⊢Δ (proj₁ [σ])) (proj₁ [σ′]) (proj₁ [σ≡σ′])))

wk1Termᵛ : ∀ {F G rF rG t Γ l l'}
         ([Γ] : ⊩ᵛ Γ)
         ([F] : Γ ⊩ᵛ⟨ l' ⟩ F ^ rF / [Γ]) →
         ([G] : Γ ⊩ᵛ⟨ l ⟩ G ^ rG / [Γ]) →
          Γ ⊩ᵛ⟨ l ⟩ t ∷ G ^ rG / [Γ] / [G] →
          Γ ∙ F ^ rF ⊩ᵛ⟨ l ⟩ wk1 t ∷ wk1 G ^ rG / ([Γ] ∙ [F]) / wk1ᵛ {A = G} {F = F} [Γ] [F] [G]
wk1Termᵛ {F} {G} {rF} {rG} {t} [Γ] [F] [G] [t]ₜ {Δ} {σ} ⊢Δ [σ] =
         let [σt] = proj₁ ([t]ₜ ⊢Δ (proj₁ [σ]))
             [σG] = proj₁ ([G] ⊢Δ (proj₁ [σ]))
             [teq] = PE.sym (subst-wk {step id} {σ} t)
             [Geq] = PE.sym (subst-wk {step id} {σ} G)
             [σG]' = irrelevance′ [Geq] [σG]
         in irrelevanceTerm″ [Geq] PE.refl PE.refl [teq] [σG] [σG]' [σt] ,
            λ [σ′] [σ≡σ′] → irrelevanceEqTerm″ PE.refl PE.refl
                            (PE.sym (subst-wk t)) (PE.sym (subst-wk t)) (PE.sym (subst-wk G))
                            [σG] [σG]' (proj₂ ([t]ₜ ⊢Δ (proj₁ [σ])) (proj₁ [σ′]) (proj₁ [σ≡σ′]))

wk1dᵛ : ∀ {F F' G rF rF' lG Γ l l'}
         ([Γ] : ⊩ᵛ Γ)
         ([F] : Γ ⊩ᵛ⟨ l' ⟩ F ^ rF / [Γ]) →
         ([F'] : Γ ⊩ᵛ⟨ l' ⟩ F' ^ rF' / [Γ]) →
       let [ΓF] = _∙_ {A = F} [Γ] [F]
           [ΓF'] = _∙_ {A = F'} [Γ] [F']
           [ΓF'F] = _∙_ {A = wk1 F} [ΓF'] (wk1ᵛ {A = F} {F = F'} [Γ] [F'] [F])
       in Γ ∙ F ^ rF ⊩ᵛ⟨ l ⟩ G ^ [ ! , lG ] / [ΓF] →
          Γ ∙ F' ^ rF' ∙ wk1 F ^ rF ⊩ᵛ⟨ l ⟩ wk1d G ^ [ ! , lG ] / [ΓF'F]
wk1dᵛ {F} {F'} {G} [Γ] [F] [F'] [G] {Δ} {σ} ⊢Δ [σ] =
     let l    = ∞
         [ΓF'] = _∙_ {A = F'} [Γ] [F']
         [ΓF'F] = _∙_ {A = wk1 F} [ΓF'] (wk1ᵛ {A = F} {F = F'} [Γ] [F'] [F])
         [wσ] = proj₁ (proj₁ [σ]) , irrelevanceTerm″ (subst-wk F) PE.refl PE.refl PE.refl
                                                     (proj₁ (wk1ᵛ {A = F} {F = F'} [Γ] [F'] [F] ⊢Δ (proj₁ [σ])))
                                                     (proj₁ ([F] ⊢Δ (proj₁ (proj₁ [σ]))))
                                                     (proj₂ [σ])
         [σG] = proj₁ ([G] ⊢Δ [wσ])
         [Geq] = PE.sym (subst-wk G)
         [σG]′ = irrelevance′ [Geq] [σG]
     in  [σG]′
         ,   (λ {σ′} [σ′] [σ≡σ′] → let [wσ′] = proj₁ (proj₁ [σ′]) ,
                                               irrelevanceTerm″ (subst-wk F) PE.refl PE.refl PE.refl
                                                     (proj₁ (wk1ᵛ {A = F} {F = F'} [Γ] [F'] [F] ⊢Δ (proj₁ [σ′])))
                                                     (proj₁ ([F] ⊢Δ (proj₁ (proj₁ [σ′]))))
                                                     (proj₂ [σ′])
                                       [wσ≡σ′] = (proj₁ (proj₁ [σ≡σ′])),
                                                 irrelevanceEqTerm″ PE.refl PE.refl PE.refl PE.refl (subst-wk F)
                                                     (proj₁ (wk1ᵛ {A = F} {F = F'} [Γ] [F'] [F] ⊢Δ (proj₁ [σ])))
                                                     (proj₁ ([F] ⊢Δ (proj₁ (proj₁ [σ]))))
                                                     (proj₂  [σ≡σ′])
                              in irrelevanceEq″ (PE.sym (subst-wk G)) (PE.sym (subst-wk G)) PE.refl PE.refl
                                                (proj₁ ([G] ⊢Δ [wσ])) [σG]′
                                                (proj₂ ([G] ⊢Δ [wσ]) [wσ′] [wσ≡σ′]))

wk1dᵗᵛ : ∀ {F F' G rF rF' rG lG Γ l l'}
         ([Γ] : ⊩ᵛ Γ)
         ([F] : Γ ⊩ᵛ⟨ l' ⟩ F ^ rF / [Γ]) →
         ([F'] : Γ ⊩ᵛ⟨ l' ⟩ F' ^ rF' / [Γ]) →
       let [ΓF] = _∙_ {A = F} [Γ] [F]
           [ΓF'] = _∙_ {A = F'} [Γ] [F']
           [ΓF'F] = _∙_ {A = wk1 F} [ΓF'] (wk1ᵛ {A = F} {F = F'} [Γ] [F'] [F])
       in ([UG] : (Γ ∙ F ^ rF) ⊩ᵛ⟨ l ⟩ Univ rG lG ^ [ ! , next lG ] / [ΓF]) →
          ([wUG] : (Γ ∙ F' ^ rF' ∙ wk1 F ^ rF) ⊩ᵛ⟨ l ⟩ Univ rG lG ^ [ ! , next lG ] / [ΓF'F]) →
          Γ ∙ F ^ rF ⊩ᵛ⟨ l ⟩ G ∷ Univ rG lG ^ [ ! , next lG ] / [ΓF] / (λ {Δ} {σ} → [UG] {Δ} {σ}) →
          Γ ∙ F' ^ rF' ∙ wk1 F ^ rF ⊩ᵛ⟨ l ⟩ wk1d G ∷ Univ rG lG ^ [ ! , next lG ] / [ΓF'F] / (λ {Δ} {σ} → [wUG] {Δ} {σ})
wk1dᵗᵛ {F} {F'} {G} {rF} {rF'} {rG} {lG} [Γ] [F] [F'] [UG] [wUG] [G]ₜ {Δ} {σ} ⊢Δ [σ] =
     let l    = ∞
         [ΓF'] = _∙_ {A = F'} [Γ] [F']
         [ΓF'F] = _∙_ {A = wk1 F} [ΓF'] (wk1ᵛ {A = F} {F = F'} [Γ] [F'] [F])
         [wσ] = proj₁ (proj₁ [σ]) , irrelevanceTerm″ (subst-wk F) PE.refl PE.refl PE.refl
                                                     (proj₁ (wk1ᵛ {A = F} {F = F'} [Γ] [F'] [F] ⊢Δ (proj₁ [σ])))
                                                     (proj₁ ([F] ⊢Δ (proj₁ (proj₁ [σ]))))
                                                     (proj₂ [σ])
         [σG] = proj₁ ([G]ₜ ⊢Δ [wσ])
         [Geq] = PE.sym (subst-wk G)
         [σG]′ = irrelevanceTerm″ PE.refl PE.refl PE.refl [Geq] (proj₁ ([UG] ⊢Δ [wσ])) (proj₁ ([wUG] {Δ} {σ} ⊢Δ [σ])) [σG]
     in  [σG]′
         ,   (λ {σ′} [σ′] [σ≡σ′] → let [wσ′] = proj₁ (proj₁ [σ′]) ,
                                               irrelevanceTerm″ (subst-wk F) PE.refl PE.refl PE.refl
                                                     (proj₁ (wk1ᵛ {A = F} {F = F'} [Γ] [F'] [F] ⊢Δ (proj₁ [σ′])))
                                                     (proj₁ ([F] ⊢Δ (proj₁ (proj₁ [σ′]))))
                                                     (proj₂ [σ′])
                                       [wσ≡σ′] = (proj₁ (proj₁ [σ≡σ′])),
                                                 irrelevanceEqTerm″ PE.refl PE.refl PE.refl PE.refl (subst-wk F)
                                                     (proj₁ (wk1ᵛ {A = F} {F = F'} [Γ] [F'] [F] ⊢Δ (proj₁ [σ])))
                                                     (proj₁ ([F] ⊢Δ (proj₁ (proj₁ [σ]))))
                                                     (proj₂  [σ≡σ′])
                              in irrelevanceEqTerm″ PE.refl PE.refl
                                                    (PE.sym (subst-wk G))
                                                    (PE.sym (subst-wk G)) PE.refl
                                                    (proj₁ ([UG] ⊢Δ [wσ])) (proj₁ ([wUG] {Δ} {σ} ⊢Δ [σ]))
                                                    (proj₂ ([G]ₜ ⊢Δ [wσ]) [wσ′] [wσ≡σ′]))

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
module Data.Finitude where

open import Data.Fin as Fin
open import Data.Nat as ℕ
open import Level

open import Function as Fun hiding (id; _∘_)
open import Function.Equality as F using (_⟨$⟩_)
open import Function.Injection as Inj hiding (id; _∘_)
open import Function.Bijection as Bij hiding (id; _∘_)
open import Function.LeftInverse      hiding (id; _∘_)
open import Function.Inverse   as Inv hiding (id; _∘_)
open import Relation.Binary
import Relation.Binary.PropositionalEquality as P
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)

Finitude : ∀ {a ℓ} (A : Setoid a ℓ) (n : ℕ) → Set _
Finitude A n = Inverse A (P.setoid (Fin n))

module Subset where
  open import Data.Product as Prod hiding (map)
  open import Data.Fin.Subset using (Subset; _∈_; outside; inside; ∣_∣) renaming (⊥ to ∅)
  open import Data.Vec
  subset-finitude : ∀ {n}(s : Subset n) → Finitude (P.setoid (∃ (_∈ s))) ∣ s ∣
  subset-finitude {ℕ.zero} [] = record {
      to = P.→-to-⟶ (λ ())
    ; from = P.→-to-⟶ (λ () )
    ; inverse-of = record {
        left-inverse-of = λ ()
      ; right-inverse-of = λ ()
      }
    }
  subset-finitude {ℕ.suc n} (inside ∷ s) = record {
        to = P.→-to-⟶ λ { (_ , here) → Fin.zero
                          ; (_ , there p) → Fin.suc (to ⟨$⟩ (_ , p)) }
      ; from = P.→-to-⟶ λ { Fin.zero → _ , here
                           ; (Fin.suc i) → _ , there (proj₂ (from ⟨$⟩ i))}
      ; inverse-of = record {
            left-inverse-of = λ { (_ , here) → P.refl
                                 ; (_ , there p) → P.cong
                                   (Prod.map Fin.suc there) (linv (_ , p))}
          ; right-inverse-of = λ { Fin.zero → P.refl
                                 ; (Fin.suc i) → P.cong Fin.suc (rinv i)}
        }
      }
    where
      open Inverse (subset-finitude s)
      open _InverseOf_ inverse-of renaming (left-inverse-of to linv
                                           ;right-inverse-of to rinv)

  subset-finitude {ℕ.suc n} (outside ∷ s) = record {
      to = P.→-to-⟶ (λ { (_ , there p) → to ⟨$⟩ (_ , p)})
    ; from = P.→-to-⟶ (λ i → Prod.map Fin.suc there (from ⟨$⟩ i) )
    ; inverse-of = record {
           left-inverse-of = λ { (_ , there p) →
             P.cong (Prod.map Fin.suc there) (linv (_ , p)) }
         ; right-inverse-of = rinv
      }
    }
      where
        open Inverse (subset-finitude s)
        open _InverseOf_ inverse-of renaming ( left-inverse-of to linv
                                             ; right-inverse-of to rinv)

max_stars_repo_name: tizmd/agda-finitary

max_issues_repo_name: tizmd/agda-finitary

max_forks_repo_name: tizmd/agda-finitary


text:
{-# OPTIONS --cubical --safe #-}

module Container.List.Syntax where

open import Prelude
open import Container
open import Container.List
open import Data.Fin

record ListSyntax {a b} (A : Type a) (B : Type b) : Type (a ℓ⊔ b) where
  field [_] : B → List A

open ListSyntax ⦃ ... ⦄ public

instance
  cons : ⦃ _ : ListSyntax A B ⦄ →  ListSyntax A (A × B)
  [_] ⦃ cons ⦄ (x , xs) .fst = suc ([ xs ] .fst)
  [_] ⦃ cons ⦄ (x , xs) .snd f0 = x
  [_] ⦃ cons ⦄ (x , xs) .snd (fs n) = [ xs ] .snd n

instance
  sing : ListSyntax A A
  [_] ⦃ sing ⦄ x = 1 , const x


text:
open import Formalization.PredicateLogic.Signature

module Formalization.PredicateLogic.Syntax.Substitution (𝔏 : Signature) where
open Signature(𝔏)

open import Data.Boolean
open import Data.ListSized
import      Data.ListSized.Functions as List
open import Formalization.PredicateLogic.Syntax(𝔏)
open import Functional using (_∘_ ; _∘₂_ ; id ; apply)
open import Numeral.CoordinateVector as Vector using (Vector)
open import Numeral.Finite
open import Numeral.Natural
open import Syntax.Function
open import Type

private variable args n vars vars₁ vars₂ : ℕ

-- Substitutes the variables of a term by mapping every variable index to a term.
substituteTerm : Vector(vars₁)(Term(vars₂)) → Term(vars₁) → Term(vars₂)
substituteTerm₊ : Vector(vars₁)(Term(vars₂)) → List(Term(vars₁))(args) → List(Term(vars₂))(args)
substituteTerm  t (var v)    = Vector.proj t v
substituteTerm  t (func f x) = func f (substituteTerm₊ t x)
substituteTerm₊ t ∅        = ∅
substituteTerm₊ t (x ⊰ xs) = (substituteTerm t x) ⊰ (substituteTerm₊ t xs)

-- Adds a new untouched variable to a term mapper.
-- Example: termMapper𝐒(0 ↦ t0 ; 1 ↦ t1 ; 2 ↦ t2) = (0 ↦ var 0 ; 1 ↦ t0 ; 2 ↦ t1 ; 3 ↦ t2)
termMapper𝐒 : Vector(vars₁)(Term(vars₂)) → Vector(𝐒(vars₁))(Term(𝐒(vars₂)))
termMapper𝐒 = Vector.prepend(var 𝟎) ∘ Vector.map(substituteTerm(var ∘ 𝐒))

-- Substitutes the variables of a formula by mapping every variable index to a term.
substitute : Vector(vars₁)(Term(vars₂)) → Formula(vars₁) → Formula(vars₂)
substitute t (P $ x)  = P $ (substituteTerm₊ t x)
substitute t ⊤        = ⊤
substitute t ⊥        = ⊥
substitute t (φ ∧ ψ)  = (substitute t φ) ∧ (substitute t ψ)
substitute t (φ ∨ ψ)  = (substitute t φ) ∨ (substitute t ψ)
substitute t (φ ⟶ ψ)  = (substitute t φ) ⟶ (substitute t ψ)
substitute t (Ɐ φ)    = Ɐ(substitute (termMapper𝐒 t) φ)
substitute t (∃ φ)    = ∃(substitute (termMapper𝐒 t) φ)

-- Substitutes the most recent variable of a formula by mapping it to a term.
substitute0 : Term(vars) → Formula(𝐒(vars)) → Formula(vars)
substitute0 = substitute ∘ (t ↦ Vector.prepend t var)

-- Substitutes a single arbitrary variable of a formula by mapping it to a term.
-- Note: (substituteN 𝟎) normalizes to substitute0 because of the definition for Vector.insert.
substituteN : 𝕟₌(vars) → Term(vars) → Formula(𝐒(vars)) → Formula(vars)
substituteN n = substitute ∘ (t ↦ Vector.insert₊ n t var)

open import Data
open import Function.Equals
import      Function.Names as Names
import      Lvl
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Function
open import Structure.Operator
open import Syntax.Number

private variable ℓ : Lvl.Level
private variable A B : Type{ℓ}
private variable f g : A → B
private variable φ : Formula(vars)

termMapper𝐒-identity : (termMapper𝐒{vars₁ = vars} var ⊜ var)
_⊜_.proof termMapper𝐒-identity {x = 𝟎}   = [≡]-intro
_⊜_.proof termMapper𝐒-identity {x = 𝐒 v} = [≡]-intro

module _ {f g : 𝕟(vars₁) → Term(vars₂)} (eq : f ⊜ g) where
  termMapper𝐒-equal-functions : (termMapper𝐒 f ⊜ termMapper𝐒 g)
  _⊜_.proof termMapper𝐒-equal-functions {𝟎} = [≡]-intro
  _⊜_.proof termMapper𝐒-equal-functions {𝐒 v} rewrite _⊜_.proof eq{v} = [≡]-intro

  substituteTerm-equal-functions-raw : (substituteTerm f Names.⊜ substituteTerm g)
  substituteTerm₊-equal-functions-raw : (substituteTerm₊{args = args} f Names.⊜ substituteTerm₊ g)
  (substituteTerm-equal-functions-raw) {var x} = _⊜_.proof eq
  (substituteTerm-equal-functions-raw) {func f x}
    rewrite substituteTerm₊-equal-functions-raw {x = x}
    = [≡]-intro
  (substituteTerm₊-equal-functions-raw) {x = ∅}      = [≡]-intro
  (substituteTerm₊-equal-functions-raw) {x = x ⊰ xs}
    rewrite substituteTerm-equal-functions-raw {x}
    rewrite substituteTerm₊-equal-functions-raw {x = xs}
    = [≡]-intro
  substituteTerm-equal-functions : (substituteTerm f ⊜ substituteTerm g)
  substituteTerm-equal-functions = intro(\{x} → substituteTerm-equal-functions-raw{x})
  substituteTerm₊-equal-functions : (substituteTerm₊{args = args} f ⊜ substituteTerm₊ g)
  substituteTerm₊-equal-functions = intro substituteTerm₊-equal-functions-raw

substitute-equal-functions : (f ⊜ g) → (substitute f ⊜ substitute g)
substitute-equal-functions = intro ∘ p where
  p : (f ⊜ g) → (substitute f Names.⊜ substitute g)
  p eq {P $ x}
    rewrite _⊜_.proof (substituteTerm₊-equal-functions eq) {x}
    = [≡]-intro
  p eq {⊤}     = [≡]-intro
  p eq {⊥}     = [≡]-intro
  p eq {φ ∧ ψ}
    rewrite p eq {φ}
    rewrite p eq {ψ}
    = [≡]-intro
  p eq {φ ∨ ψ}
    rewrite p eq {φ}
    rewrite p eq {ψ}
    = [≡]-intro
  p eq {φ ⟶ ψ}
    rewrite p eq {φ}
    rewrite p eq {ψ}
    = [≡]-intro
  p eq {Ɐ φ}
    rewrite p (termMapper𝐒-equal-functions eq) {φ}
    = [≡]-intro
  p eq {∃ φ}
    rewrite p (termMapper𝐒-equal-functions eq) {φ}
    = [≡]-intro

substituteTerm-identity-raw : (substituteTerm{vars₁ = vars} var Names.⊜ id)
substituteTerm₊-identity-raw : (substituteTerm₊{vars₁ = vars}{args = args} var Names.⊜ id)
substituteTerm-identity-raw {x = var x}    = [≡]-intro
substituteTerm-identity-raw {x = func f x} rewrite substituteTerm₊-identity-raw{x = x} = [≡]-intro
substituteTerm₊-identity-raw {x = ∅} = [≡]-intro
substituteTerm₊-identity-raw {x = x ⊰ xs}
  rewrite substituteTerm-identity-raw{x = x}
  rewrite substituteTerm₊-identity-raw{x = xs}
  = [≡]-intro
substituteTerm-identity : (substituteTerm{vars₁ = vars} var ⊜ id)
substituteTerm-identity = intro substituteTerm-identity-raw
substituteTerm₊-identity : (substituteTerm₊{vars₁ = vars}{args = args} var ⊜ id)
substituteTerm₊-identity = intro substituteTerm₊-identity-raw

substitute-identity : (substitute{vars₁ = vars} var ⊜ id)
substitute-identity = intro p where
  p : (substitute{vars₁ = vars} var Names.⊜ id)
  p {x = P $ x} rewrite _⊜_.proof substituteTerm₊-identity {x} = [≡]-intro
  p {x = ⊤}     = [≡]-intro
  p {x = ⊥}     = [≡]-intro
  p {x = φ ∧ ψ} rewrite p {x = φ} rewrite p {x = ψ} = [≡]-intro
  p {x = φ ∨ ψ} rewrite p {x = φ} rewrite p {x = ψ} = [≡]-intro
  p {x = φ ⟶ ψ} rewrite p {x = φ} rewrite p {x = ψ} = [≡]-intro
  p {x = Ɐ φ}
    rewrite _⊜_.proof (substitute-equal-functions termMapper𝐒-identity) {φ}
    rewrite p {x = φ}
    = [≡]-intro
  p {x = ∃ φ}
    rewrite _⊜_.proof (substitute-equal-functions termMapper𝐒-identity) {φ}
    rewrite p {x = φ}
    = [≡]-intro

{-
test1 : ∀{t : Term(vars)}{n : 𝕟(𝐒(𝐒 vars))} → (termMapper𝐒 (introduceVar t) n ≡ introduceVar (termVar𝐒 t) n)
test1 {t = var 𝟎} {𝟎} = {!introduceVar(termVar𝐒{_}(?)) 0!}
test1 {t = var 𝟎} {𝐒 n} = {!termMapper𝐒(introduceVar(?)) 1!}
test1 {t = var (𝐒 v)}{n} = {!!}
test1 {t = func f x}{n} = {!!}

test : ∀{t}{φ : Formula(𝐒 vars)} → (substitute(introduceVar t) φ ≡ substitute0 t φ)
test {vars} {t} {P $ x} = {!!}
test {vars} {t} {⊤} = [≡]-intro
test {vars} {t} {⊥} = [≡]-intro
test {vars} {t} {φ ∧ ψ} rewrite test {vars}{t}{φ} rewrite test{vars}{t}{ψ} = [≡]-intro
test {vars} {t} {φ ∨ ψ} rewrite test {vars}{t}{φ} rewrite test{vars}{t}{ψ} = [≡]-intro
test {vars} {t} {φ ⟶ ψ} rewrite test {vars}{t}{φ} rewrite test{vars}{t}{ψ} = [≡]-intro
test {vars} {t} {Ɐ φ} = {!test{𝐒 vars}{termVar𝐒 t}{φ}!}
test {vars} {t} {∃ φ} = {!!}
-}