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

module 18-circle where

import 17-groups
open 17-groups public

{- Section 11.1 The induction principle of the circle -}

free-loops :
  { l1 : Level} (X : UU l1) → UU l1
free-loops X = Σ X (λ x → Id x x)

base-free-loop :
  { l1 : Level} {X : UU l1} → free-loops X → X
base-free-loop = pr1

loop-free-loop :
  { l1 : Level} {X : UU l1} (l : free-loops X) →
  Id (base-free-loop l) (base-free-loop l)
loop-free-loop = pr2

-- Now we characterize the identity types of free loops

Eq-free-loops :
  { l1 : Level} {X : UU l1} (l l' : free-loops X) → UU l1
Eq-free-loops (pair x l) l' =
  Σ (Id x (pr1 l')) (λ p → Id (l ∙ p) (p ∙ (pr2 l')))

reflexive-Eq-free-loops :
  { l1 : Level} {X : UU l1} (l : free-loops X) → Eq-free-loops l l
reflexive-Eq-free-loops (pair x l) = pair refl right-unit

Eq-free-loops-eq :
  { l1 : Level} {X : UU l1} (l l' : free-loops X) →
  Id l l' → Eq-free-loops l l'
Eq-free-loops-eq l .l refl = reflexive-Eq-free-loops l

abstract
  is-contr-total-Eq-free-loops :
    { l1 : Level} {X : UU l1} (l : free-loops X) →
    is-contr (Σ (free-loops X) (Eq-free-loops l))
  is-contr-total-Eq-free-loops (pair x l) =
    is-contr-total-Eq-structure
      ( λ x l' p → Id (l ∙ p) (p ∙ l'))
      ( is-contr-total-path x)
      ( pair x refl)
      ( is-contr-is-equiv'
        ( Σ (Id x x) (λ l' → Id l l'))
        ( tot (λ l' α → right-unit ∙ α))
        ( is-equiv-tot-is-fiberwise-equiv
          ( λ l' → is-equiv-concat right-unit l'))
        ( is-contr-total-path l))

abstract
  is-equiv-Eq-free-loops-eq :
    { l1 : Level} {X : UU l1} (l l' : free-loops X) →
    is-equiv (Eq-free-loops-eq l l')
  is-equiv-Eq-free-loops-eq l =
    fundamental-theorem-id l
      ( reflexive-Eq-free-loops l)
      ( is-contr-total-Eq-free-loops l)
      ( Eq-free-loops-eq l)

{- We introduce dependent free loops, which are used in the induction principle
   of the circle. -}

dependent-free-loops :
  { l1 l2 : Level} {X : UU l1} (l : free-loops X) (P : X → UU l2) → UU l2
dependent-free-loops l P =
  Σ ( P (base-free-loop l))
    ( λ p₀ → Id (tr P (loop-free-loop l) p₀) p₀)

Eq-dependent-free-loops :
  { l1 l2 : Level} {X : UU l1} (l : free-loops X) (P : X → UU l2) →
  ( p p' : dependent-free-loops l P) → UU l2
Eq-dependent-free-loops (pair x l) P (pair y p) p' =
  Σ ( Id y (pr1 p'))
    ( λ q → Id (p ∙ q) ((ap (tr P l) q) ∙ (pr2 p')))

reflexive-Eq-dependent-free-loops :
  { l1 l2 : Level} {X : UU l1} (l : free-loops X) (P : X → UU l2) →
  ( p : dependent-free-loops l P) → Eq-dependent-free-loops l P p p
reflexive-Eq-dependent-free-loops (pair x l) P (pair y p) =
  pair refl right-unit

Eq-dependent-free-loops-eq :
  { l1 l2 : Level} {X : UU l1} (l : free-loops X) (P : X → UU l2) →
  ( p p' : dependent-free-loops l P) →
  Id p p' → Eq-dependent-free-loops l P p p'
Eq-dependent-free-loops-eq l P p .p refl =
  reflexive-Eq-dependent-free-loops l P p

abstract
  is-contr-total-Eq-dependent-free-loops :
    { l1 l2 : Level} {X : UU l1} (l : free-loops X) (P : X → UU l2) →
    ( p : dependent-free-loops l P) →
    is-contr (Σ (dependent-free-loops l P) (Eq-dependent-free-loops l P p))
  is-contr-total-Eq-dependent-free-loops (pair x l) P (pair y p) =
    is-contr-total-Eq-structure
      ( λ y' p' q → Id (p ∙ q) ((ap (tr P l) q) ∙ p'))
      ( is-contr-total-path y)
      ( pair y refl)
      ( is-contr-is-equiv'
        ( Σ (Id (tr P l y) y) (λ p' → Id p p'))
        ( tot (λ p' α → right-unit ∙ α))
        ( is-equiv-tot-is-fiberwise-equiv
          ( λ p' → is-equiv-concat right-unit p'))
        ( is-contr-total-path p))

abstract
  is-equiv-Eq-dependent-free-loops-eq :
    { l1 l2 : Level} {X : UU l1} (l : free-loops X) (P : X → UU l2)
    ( p p' : dependent-free-loops l P) →
    is-equiv (Eq-dependent-free-loops-eq l P p p')
  is-equiv-Eq-dependent-free-loops-eq l P p =
    fundamental-theorem-id p
      ( reflexive-Eq-dependent-free-loops l P p)
      ( is-contr-total-Eq-dependent-free-loops l P p)
      ( Eq-dependent-free-loops-eq l P p)

eq-Eq-dependent-free-loops :
  { l1 l2 : Level} {X : UU l1} (l : free-loops X) (P : X → UU l2)
  ( p p' : dependent-free-loops l P) →
  Eq-dependent-free-loops l P p p' → Id p p'
eq-Eq-dependent-free-loops l P p p' =
  inv-is-equiv (is-equiv-Eq-dependent-free-loops-eq l P p p')

{- We now define the induction principle of the circle. -}

ev-free-loop' :
  { l1 l2 : Level} {X : UU l1} (l : free-loops X) (P : X → UU l2) →
  ( (x : X) → P x) → dependent-free-loops l P
ev-free-loop' (pair x₀ p) P f = pair (f x₀) (apd f p)

induction-principle-circle :
  { l1 : Level} (l2 : Level) {X : UU l1} (l : free-loops X) →
  UU ((lsuc l2) ⊔ l1)
induction-principle-circle l2 {X} l =
  (P : X → UU l2) → sec (ev-free-loop' l P)

{- Section 11.2 The universal property of the circle -}

{- We first state the universal property of the circle -}

ev-free-loop :
  { l1 l2 : Level} {X : UU l1} (l : free-loops X) (Y : UU l2) →
  ( X → Y) → free-loops Y
ev-free-loop l Y f = pair (f (pr1 l)) (ap f (pr2 l))

universal-property-circle :
  { l1 : Level} (l2 : Level) {X : UU l1} (l : free-loops X) → UU _
universal-property-circle l2 l =
  ( Y : UU l2) → is-equiv (ev-free-loop l Y)

{- A fairly straightforward proof of the universal property of the circle
   factors through the dependent universal property of the circle. -}

dependent-universal-property-circle :
  { l1 : Level} (l2 : Level) {X : UU l1} (l : free-loops X) →
  UU ((lsuc l2) ⊔ l1)
dependent-universal-property-circle l2 {X} l =
  ( P : X → UU l2) → is-equiv (ev-free-loop' l P)

{- We first prove that the dependent universal property of the circle follows
   from the induction principle of the circle. To show this, we have to show
   that the section of ev-free-loop' is also a retraction. This construction
   is also by the induction principle of the circle, but it requires (a minimal
   amount of) preparations. -}

Eq-subst :
  { l1 l2 : Level} {X : UU l1} {P : X → UU l2} (f g : (x : X) → P x) →
  X → UU _
Eq-subst f g x = Id (f x) (g x)

tr-Eq-subst :
  { l1 l2 : Level} {X : UU l1} {P : X → UU l2} (f g : (x : X) → P x)
  { x y : X} (p : Id x y) (q : Id (f x) (g x)) (r : Id (f y) (g y))→
  ( Id ((apd f p) ∙ r) ((ap (tr P p) q) ∙ (apd g p))) →
  ( Id (tr (Eq-subst f g) p q) r)
tr-Eq-subst f g refl q .((ap id q) ∙ refl) refl =
  inv (right-unit ∙ (ap-id q))

dependent-free-loops-htpy :
  {l1 l2 : Level} {X : UU l1} {l : free-loops X} {P : X → UU l2}
  {f g : (x : X) → P x} →
  ( Eq-dependent-free-loops l P (ev-free-loop' l P f) (ev-free-loop' l P g)) →
  ( dependent-free-loops l (λ x → Id (f x) (g x)))
dependent-free-loops-htpy {l = (pair x l)} (pair p q) =
  pair p (tr-Eq-subst _ _ l p p q)

isretr-ind-circle :
  { l1 l2 : Level} {X : UU l1} (l : free-loops X) →
  ( ind-circle : induction-principle-circle l2 l) (P : X → UU l2) →
  ( (pr1 (ind-circle P)) ∘ (ev-free-loop' l P)) ~ id
isretr-ind-circle l ind-circle P f =
  eq-htpy
    ( pr1
      ( ind-circle
        ( λ t → Id (pr1 (ind-circle P) (ev-free-loop' l P f) t) (f t)))
      ( dependent-free-loops-htpy
        ( Eq-dependent-free-loops-eq l P _ _
          ( pr2 (ind-circle P) (ev-free-loop' l P f)))))

abstract
  dependent-universal-property-induction-principle-circle :
    { l1 l2 : Level} {X : UU l1} (l : free-loops X) →
    induction-principle-circle l2 l → dependent-universal-property-circle l2 l
  dependent-universal-property-induction-principle-circle l ind-circle P =
    is-equiv-has-inverse
      ( pr1 (ind-circle P))
      ( pr2 (ind-circle P))
      ( isretr-ind-circle l ind-circle P)

{- We use the dependent universal property to derive a uniqeness property of
   dependent functions on the circle. -}

dependent-uniqueness-circle :
  { l1 l2 : Level} {X : UU l1} (l : free-loops X) →
  dependent-universal-property-circle l2 l →
  { P : X → UU l2} (k : dependent-free-loops l P) →
  is-contr
    ( Σ ( (x : X) → P x)
        ( λ h → Eq-dependent-free-loops l P (ev-free-loop' l P h) k))
dependent-uniqueness-circle l dup-circle {P} k =
  is-contr-is-equiv'
    ( fib (ev-free-loop' l P) k)
    ( tot (λ h → Eq-dependent-free-loops-eq l P (ev-free-loop' l P h) k))
    ( is-equiv-tot-is-fiberwise-equiv
      (λ h → is-equiv-Eq-dependent-free-loops-eq l P (ev-free-loop' l P h) k))
    ( is-contr-map-is-equiv (dup-circle P) k)

{- Now that we have established the dependent universal property, we can
   reduce the (non-dependent) universal property to the dependent case. We do
   so by constructing a commuting triangle relating ev-free-loop to
   ev-free-loop' via a comparison equivalence. -}

tr-const :
  {i j : Level} {A : UU i} {B : UU j} {x y : A} (p : Id x y) (b : B) →
  Id (tr (λ (a : A) → B) p b) b
tr-const refl b = refl

apd-const :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B) {x y : A}
  (p : Id x y) → Id (apd f p) ((tr-const p (f x)) ∙ (ap f p))
apd-const f refl = refl

comparison-free-loops :
  { l1 l2 : Level} {X : UU l1} (l : free-loops X) (Y : UU l2) →
  free-loops Y → dependent-free-loops l (λ x → Y)
comparison-free-loops l Y =
  tot (λ y l' → (tr-const (pr2 l) y) ∙ l')

abstract
  is-equiv-comparison-free-loops :
    { l1 l2 : Level} {X : UU l1} (l : free-loops X) (Y : UU l2) →
    is-equiv (comparison-free-loops l Y)
  is-equiv-comparison-free-loops l Y =
    is-equiv-tot-is-fiberwise-equiv
      ( λ y → is-equiv-concat (tr-const (pr2 l) y) y)

triangle-comparison-free-loops :
  { l1 l2 : Level} {X : UU l1} (l : free-loops X) (Y : UU l2) →
  ( (comparison-free-loops l Y) ∘ (ev-free-loop l Y)) ~
  ( ev-free-loop' l (λ x → Y))
triangle-comparison-free-loops (pair x l) Y f =
  eq-Eq-dependent-free-loops
    ( pair x l)
    ( λ x → Y)
    ( comparison-free-loops (pair x l) Y (ev-free-loop (pair x l) Y f))
    ( ev-free-loop' (pair x l) (λ x → Y) f)
    ( pair refl (right-unit ∙ (inv (apd-const f l))))

abstract
  universal-property-dependent-universal-property-circle :
    { l1 l2 : Level} {X : UU l1} (l : free-loops X) →
    ( dependent-universal-property-circle l2 l) →
    ( universal-property-circle l2 l)
  universal-property-dependent-universal-property-circle l dup-circle Y =
    is-equiv-right-factor
      ( ev-free-loop' l (λ x → Y))
      ( comparison-free-loops l Y)
      ( ev-free-loop l Y)
      ( htpy-inv (triangle-comparison-free-loops l Y))
      ( is-equiv-comparison-free-loops l Y)
      ( dup-circle (λ x → Y))

{- Now we get the universal property of the circle from the induction principle
   of the circle by composing the earlier two proofs. -}

abstract
  universal-property-induction-principle-circle :
    { l1 l2 : Level} {X : UU l1} (l : free-loops X) →
    induction-principle-circle l2 l → universal-property-circle l2 l
  universal-property-induction-principle-circle l =
    ( universal-property-dependent-universal-property-circle l) ∘
    ( dependent-universal-property-induction-principle-circle l)

unique-mapping-property-circle :
  { l1 : Level} (l2 : Level) {X : UU l1} (l : free-loops X) →
  UU (l1 ⊔ (lsuc l2))
unique-mapping-property-circle l2 {X} l =
  ( Y : UU l2) (l' : free-loops Y) →
    is-contr (Σ (X → Y) (λ f → Eq-free-loops (ev-free-loop l Y f) l'))

abstract
  unique-mapping-property-universal-property-circle :
    { l1 l2 : Level} {X : UU l1} (l : free-loops X) →
    universal-property-circle l2 l →
    unique-mapping-property-circle l2 l
  unique-mapping-property-universal-property-circle l up-circle Y l' =
    is-contr-is-equiv'
      ( fib (ev-free-loop l Y) l')
      ( tot (λ f → Eq-free-loops-eq (ev-free-loop l Y f) l'))
      ( is-equiv-tot-is-fiberwise-equiv
        ( λ f → is-equiv-Eq-free-loops-eq (ev-free-loop l Y f) l'))
      ( is-contr-map-is-equiv (up-circle Y) l')

{- We assume that we have a circle. -}

postulate 𝕊¹ : UU lzero

postulate base-𝕊¹ : 𝕊¹

postulate loop-𝕊¹ : Id base-𝕊¹ base-𝕊¹

free-loop-𝕊¹ : free-loops 𝕊¹
free-loop-𝕊¹ = pair base-𝕊¹ loop-𝕊¹

postulate ind-𝕊¹ : {l : Level} → induction-principle-circle l free-loop-𝕊¹

dependent-universal-property-𝕊¹ :
  {l : Level} → dependent-universal-property-circle l free-loop-𝕊¹
dependent-universal-property-𝕊¹ =
  dependent-universal-property-induction-principle-circle free-loop-𝕊¹ ind-𝕊¹

dependent-uniqueness-𝕊¹ :
  {l : Level} {P : 𝕊¹ → UU l} (k : dependent-free-loops free-loop-𝕊¹ P) →
  is-contr (Σ ((x : 𝕊¹) → P x) (λ h → Eq-dependent-free-loops free-loop-𝕊¹ P (ev-free-loop' free-loop-𝕊¹ P h) k))
dependent-uniqueness-𝕊¹ {l} {P} k =
  dependent-uniqueness-circle free-loop-𝕊¹ dependent-universal-property-𝕊¹ k

universal-property-𝕊¹ :
  {l : Level} → universal-property-circle l free-loop-𝕊¹
universal-property-𝕊¹ =
  universal-property-dependent-universal-property-circle
    free-loop-𝕊¹
    dependent-universal-property-𝕊¹

-- Section 14.3 Multiplication on the circle

{- Exercises -}

-- Exercise 11.1

{- The dependent universal property of the circle (and hence also the induction
   principle of the circle, implies that the circle is connected in the sense
   that for any family of propositions parametrized by the circle, if the
   proposition at the base holds, then it holds for any x : circle. -}

abstract
  is-connected-circle' :
    { l1 l2 : Level} {X : UU l1} (l : free-loops X) →
    ( dup-circle : dependent-universal-property-circle l2 l)
    ( P : X → UU l2) (is-prop-P : (x : X) → is-prop (P x)) →
    P (base-free-loop l) → (x : X) → P x
  is-connected-circle' l dup-circle P is-prop-P p =
    inv-is-equiv
      ( dup-circle P)
      ( pair p (center (is-prop-P _ (tr P (pr2 l) p) p)))

max_stars_repo_name: hemangandhi/HoTT-Intro

max_issues_repo_name: hemangandhi/HoTT-Intro

max_forks_repo_name: hemangandhi/HoTT-Intro


text:
open import OutsideIn.Prelude
open import OutsideIn.X
module OutsideIn.TypeSchema(x : X) where
  open X(x)
  open import Data.Vec hiding (_>>=_)

  data NameType : Set where
    Regular : NameType
    Datacon : ℕ → NameType

  data TypeSchema ( n : Set) : NameType → Set where
    ∀′_·_⇒_ : (v : ℕ) → QConstraint (n ⨁ v) → Type (n ⨁ v) → TypeSchema n Regular
    DC∀′_,_·_⇒_⟶_ : (a b : ℕ){l : ℕ} → QConstraint ((n ⨁ a) ⨁ b)
                   → Vec (Type ((n ⨁ a) ⨁ b)) l → n → TypeSchema n (Datacon l)
    DC∀_·_⟶_ : (a : ℕ){l : ℕ} → Vec (Type (n ⨁ a)) l → n → TypeSchema n (Datacon l)

  private
    module PlusN-f n = Functor (Monad.is-functor (PlusN-is-monad {n}))
    module Vec-f {n} = Functor (vec-is-functor {n})
    module Type-f    = Functor (type-is-functor)
    module QC-f      = Functor (qconstraint-is-functor)

  private
    fmap-schema : {A B : Set}{x : NameType} → (A → B) → TypeSchema A x → TypeSchema B x
    fmap-schema f (∀′ n · Q ⇒ τ) = ∀′ n · QC-f.map (pn.map f) Q ⇒ Type-f.map (pn.map f) τ
        where module pn = PlusN-f n
    fmap-schema f (DC∀′ a , b · Q ⇒ τs ⟶ K) = DC∀′ a , b · QC-f.map (pb.map (pa.map f)) Q
                                                          ⇒ map (Type-f.map (pb.map (pa.map f))) τs
                                                          ⟶ f K
        where module pa = PlusN-f a
              module pb = PlusN-f b
    fmap-schema f (DC∀ a · τs ⟶ K) = DC∀ a · map (Type-f.map (pa.map f)) τs ⟶ f K
        where module pa = PlusN-f a

    fmap-schema-id : {A : Set}{x : NameType} {f : A → A}
                   → isIdentity f → isIdentity (fmap-schema {A}{A}{x} f)
    fmap-schema-id isid {∀′ n · Q ⇒ τ} = cong₂ (∀′_·_⇒_ n) (QC-f.identity (pn.identity isid))
                                                           (Type-f.identity (pn.identity isid))
       where module pn = PlusN-f n
    fmap-schema-id isid {DC∀′ a , b · Q ⇒ τs ⟶ K}
      = cong₃ (DC∀′_,_·_⇒_⟶_ a b)
              (QC-f.identity (pb.identity (pa.identity isid)))
              (Vec-f.identity (Type-f.identity (pb.identity (pa.identity isid))))
              isid
        where module pa = PlusN-f a
              module pb = PlusN-f b
    fmap-schema-id isid {DC∀ a · τs ⟶ K}
      = cong₂ (DC∀_·_⟶_ a)
              (Vec-f.identity (Type-f.identity (pa.identity isid)))
              isid
        where module pa = PlusN-f a

    fmap-schema-comp :  {A B C : Set}{s : NameType} {f : A → B} {g : B → C} {x : TypeSchema A s}
                     → fmap-schema (g ∘ f) x ≡ fmap-schema g (fmap-schema f x)
    fmap-schema-comp {x = ∀′ n · Q ⇒ τ} = cong₂ (∀′_·_⇒_ n)
                                                (Functor.composite (qconstraint-is-functor ∘f pnf))
                                                (Functor.composite (type-is-functor ∘f pnf))
        where pnf = Monad.is-functor (PlusN-is-monad {n})
    fmap-schema-comp {x = DC∀′ a , b · Q ⇒ τs ⟶ K}
      = cong₃ (DC∀′_,_·_⇒_⟶_ a b)
              (Functor.composite (qconstraint-is-functor ∘f pbf ∘f paf ))
              (Functor.composite (vec-is-functor ∘f type-is-functor ∘f pbf ∘f paf))
              refl
        where module pa = PlusN-f a
              module pb = PlusN-f b
              paf = Monad.is-functor (PlusN-is-monad {a})
              pbf = Monad.is-functor (PlusN-is-monad {b})
    fmap-schema-comp {x = DC∀ a · τs ⟶ K}
      = cong₂ (DC∀_·_⟶_ a)
              (Functor.composite (vec-is-functor ∘f type-is-functor ∘f paf))
              refl
        where module pa = PlusN-f a
              paf = Monad.is-functor (PlusN-is-monad {a})

  type-schema-is-functor : ∀{s} → Functor (λ x → TypeSchema x s)
  type-schema-is-functor = record { map       = fmap-schema
                                  ; identity  = fmap-schema-id
                                  ; composite = fmap-schema-comp
                                  }

ext: agda

max_stars_repo_name: liamoc/outside-in

max_issues_repo_name: liamoc/outside-in

max_forks_repo_name: liamoc/outside-in


text:
{-# OPTIONS --allow-unsolved-metas #-}
open import Level
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Ordinals
module partfunc {n : Level } (O : Ordinals {n})  where

open import logic
open import Relation.Binary
open import Data.Empty
open import Data.List hiding (filter)
open import Data.Maybe
open import Relation.Binary
open import Relation.Binary.Core
open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
open import filter O

open _∧_
open _∨_
open Bool

----
--
-- Partial Function without ZF
--

record PFunc  (Dom : Set n) (Cod : Set n) : Set (suc n) where
   field
      dom : Dom → Set n
      pmap : (x : Dom ) → dom x → Cod
      meq : {x : Dom } → { p q : dom x } → pmap x p ≡ pmap x q

----
--
-- PFunc (Lift n Nat) Cod is equivalent to List (Maybe Cod)
--

data Findp : {Cod : Set n} → List (Maybe Cod) → (x : Nat) → Set where
   v0 : {Cod : Set n} → {f : List (Maybe Cod)} → ( v : Cod ) → Findp ( just v  ∷ f ) Zero
   vn : {Cod : Set n} → {f : List (Maybe Cod)} {d : Maybe Cod} → {x : Nat} → Findp f x → Findp (d ∷ f) (Suc x)

open PFunc

find : {Cod : Set n} → (f : List (Maybe Cod) ) → (x : Nat) → Findp f x → Cod
find (just v ∷ _) 0 (v0 v) = v
find (_ ∷ n) (Suc i) (vn p) = find n i p

findpeq : {Cod : Set n} → (f : List (Maybe Cod)) → {x : Nat} {p q : Findp f x } → find f x p ≡ find f x q
findpeq n {0} {v0 _} {v0 _} = refl
findpeq [] {Suc x} {()}
findpeq (just x₁ ∷ n) {Suc x} {vn p} {vn q} = findpeq n {x} {p} {q}
findpeq (nothing ∷ n) {Suc x} {vn p} {vn q} = findpeq n {x} {p} {q}

List→PFunc : {Cod : Set n} → List (Maybe Cod) → PFunc (Lift n Nat) Cod
List→PFunc fp = record { dom = λ x → Lift n (Findp fp (lower x))
                       ; pmap = λ x y → find fp (lower x) (lower y)
                       ; meq = λ {x} {p} {q} → findpeq fp {lower x} {lower p} {lower q}
                       }
----
--
-- to List (Maybe Two) is a Latice
--

_3⊆b_ : (f g : List (Maybe Two)) → Bool
[] 3⊆b [] = true
[] 3⊆b (nothing ∷ g) = [] 3⊆b g
[] 3⊆b (_ ∷ g) = true
(nothing ∷ f) 3⊆b [] = f 3⊆b []
(nothing ∷ f) 3⊆b (_ ∷ g)  = f 3⊆b g
(just i0 ∷ f) 3⊆b (just i0 ∷ g) = f 3⊆b g
(just i1 ∷ f) 3⊆b (just i1 ∷ g) = f 3⊆b g
_ 3⊆b _ = false

_3⊆_ : (f g : List (Maybe Two)) → Set
f 3⊆ g  = (f 3⊆b g) ≡ true

_3∩_ : (f g : List (Maybe Two)) → List (Maybe Two)
[] 3∩ (nothing ∷ g) = nothing ∷ ([] 3∩ g)
[] 3∩ g  = []
(nothing ∷ f) 3∩ [] = nothing ∷ f 3∩ []
f 3∩ [] = []
(just i0 ∷ f) 3∩ (just i0 ∷ g) = just i0 ∷ (  f 3∩ g )
(just i1 ∷ f) 3∩ (just i1 ∷ g) = just i1 ∷ (  f 3∩ g )
(_ ∷ f) 3∩ (_ ∷ g)   = nothing  ∷ ( f 3∩ g )

3∩⊆f : { f g : List (Maybe Two) } → (f 3∩ g ) 3⊆ f
3∩⊆f {[]} {[]} = refl
3∩⊆f {[]} {just _ ∷ g} = refl
3∩⊆f {[]} {nothing ∷ g} = 3∩⊆f {[]} {g}
3∩⊆f {just _ ∷ f} {[]} = refl
3∩⊆f {nothing ∷ f} {[]} = 3∩⊆f {f} {[]}
3∩⊆f {just i0 ∷ f} {just i0 ∷ g} = 3∩⊆f {f} {g}
3∩⊆f {just i1 ∷ f} {just i1 ∷ g} =  3∩⊆f {f} {g}
3∩⊆f {just i0 ∷ f} {just i1 ∷ g} =   3∩⊆f {f} {g}
3∩⊆f {just i1 ∷ f} {just i0 ∷ g} =    3∩⊆f {f} {g}
3∩⊆f {nothing ∷ f} {just _ ∷ g} = 3∩⊆f {f} {g}
3∩⊆f {just i0  ∷ f} {nothing ∷ g} = 3∩⊆f {f} {g}
3∩⊆f {just i1 ∷ f} {nothing ∷ g} =  3∩⊆f {f} {g}
3∩⊆f {nothing ∷ f} {nothing ∷ g} = 3∩⊆f {f} {g}

3∩sym : { f g : List (Maybe Two) } → (f 3∩ g ) ≡ (g 3∩ f )
3∩sym {[]} {[]} = refl
3∩sym {[]} {just _ ∷ g} = refl
3∩sym {[]} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {[]} {g})
3∩sym {just _ ∷ f} {[]} = refl
3∩sym {nothing ∷ f} {[]} = cong (λ k → nothing ∷ k) (3∩sym {f} {[]})
3∩sym {just i0 ∷ f} {just i0 ∷ g} = cong (λ k → just i0 ∷ k) (3∩sym {f} {g})
3∩sym {just i0 ∷ f} {just i1 ∷ g} =  cong (λ k → nothing ∷ k) (3∩sym {f} {g})
3∩sym {just i1 ∷ f} {just i0 ∷ g} =  cong (λ k → nothing ∷ k) (3∩sym {f} {g})
3∩sym {just i1 ∷ f} {just i1 ∷ g} =  cong (λ k → just i1 ∷ k) (3∩sym {f} {g})
3∩sym {just i0 ∷ f} {nothing ∷ g} =  cong (λ k → nothing ∷ k) (3∩sym {f} {g})
3∩sym {just i1 ∷ f} {nothing ∷ g} =  cong (λ k → nothing ∷ k) (3∩sym {f} {g})
3∩sym {nothing ∷ f} {just i0 ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g})
3∩sym {nothing ∷ f} {just i1 ∷ g} =  cong (λ k → nothing ∷ k) (3∩sym {f} {g})
3∩sym {nothing ∷ f} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g})

3⊆-[] : { h : List (Maybe Two) } → [] 3⊆ h
3⊆-[] {[]} = refl
3⊆-[] {just _ ∷ h} = refl
3⊆-[] {nothing ∷ h} = 3⊆-[] {h}

3⊆trans : { f g h : List (Maybe Two) } → f 3⊆ g → g 3⊆ h → f 3⊆ h
3⊆trans {[]} {[]} {[]} f<g g<h = refl
3⊆trans {[]} {[]} {just _ ∷ h} f<g g<h = refl
3⊆trans {[]} {[]} {nothing ∷ h} f<g g<h = 3⊆trans {[]} {[]} {h} refl g<h
3⊆trans {[]} {nothing ∷ g} {[]} f<g g<h = refl
3⊆trans {[]} {just _ ∷ g} {just _ ∷ h} f<g g<h = refl
3⊆trans {[]} {nothing ∷ g} {just _ ∷ h} f<g g<h = refl
3⊆trans {[]} {nothing ∷ g} {nothing ∷ h} f<g g<h = 3⊆trans {[]} {g} {h} f<g g<h
3⊆trans {nothing ∷ f} {[]} {[]} f<g g<h = f<g
3⊆trans {nothing ∷ f} {[]} {just _ ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g (3⊆-[] {h})
3⊆trans {nothing ∷ f} {[]} {nothing ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g g<h
3⊆trans {nothing ∷ f} {nothing ∷ g} {[]} f<g g<h = 3⊆trans {f} {g} {[]} f<g g<h
3⊆trans {nothing ∷ f} {nothing ∷ g} {just _ ∷ h} f<g g<h =  3⊆trans {f} {g} {h} f<g g<h
3⊆trans {nothing ∷ f} {nothing ∷ g} {nothing ∷ h} f<g g<h =  3⊆trans {f} {g} {h} f<g g<h
3⊆trans {[]} {just i0 ∷ g} {[]} f<g ()
3⊆trans {[]} {just i1 ∷ g} {[]} f<g ()
3⊆trans {[]} {just x ∷ g} {nothing ∷ h} f<g g<h = 3⊆-[] {h}
3⊆trans {just i0 ∷ f} {[]} {h} () g<h
3⊆trans {just i1 ∷ f} {[]} {h} () g<h
3⊆trans {just x ∷ f} {just i0 ∷ g} {[]} f<g ()
3⊆trans {just x ∷ f} {just i1 ∷ g} {[]} f<g ()
3⊆trans {just i0 ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h
3⊆trans {just i1 ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h
3⊆trans {just x ∷ f} {just i0 ∷ g} {nothing ∷ h} f<g ()
3⊆trans {just x ∷ f} {just i1 ∷ g} {nothing ∷ h} f<g ()
3⊆trans {just i0 ∷ f} {nothing ∷ g} {_} () g<h
3⊆trans {just i1 ∷ f} {nothing ∷ g} {_} () g<h
3⊆trans {nothing ∷ f} {just i0 ∷ g} {[]} f<g ()
3⊆trans {nothing ∷ f} {just i1 ∷ g} {[]} f<g ()
3⊆trans {nothing ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g g<h =  3⊆trans {f} {g} {h} f<g g<h
3⊆trans {nothing ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g g<h =  3⊆trans {f} {g} {h} f<g g<h
3⊆trans {nothing ∷ f} {just i0 ∷ g} {nothing ∷ h} f<g ()
3⊆trans {nothing ∷ f} {just i1 ∷ g} {nothing ∷ h} f<g ()

3⊆∩f : { f g h : List (Maybe Two) }  → f 3⊆ g → f 3⊆ h → f 3⊆  (g 3∩ h )
3⊆∩f {[]} {[]} {[]} f<g f<h = refl
3⊆∩f {[]} {[]} {x ∷ h} f<g f<h = 3⊆-[] {[] 3∩ (x ∷ h)}
3⊆∩f {[]} {x ∷ g} {h} f<g f<h = 3⊆-[] {(x ∷ g) 3∩ h}
3⊆∩f {nothing ∷ f} {[]} {[]} f<g f<h = 3⊆∩f {f} {[]} {[]} f<g f<h
3⊆∩f {nothing ∷ f} {[]} {just _ ∷ h} f<g f<h = f<g
3⊆∩f {nothing ∷ f} {[]} {nothing ∷ h} f<g f<h = 3⊆∩f {f} {[]} {h} f<g f<h
3⊆∩f {just i0 ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h
3⊆∩f {just i1 ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h
3⊆∩f {nothing ∷ f} {just _ ∷ g} {[]} f<g f<h = f<h
3⊆∩f {nothing ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h
3⊆∩f {nothing ∷ f} {just i0 ∷ g} {just i1 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h
3⊆∩f {nothing ∷ f} {just i1 ∷ g} {just i0 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h
3⊆∩f {nothing ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h
3⊆∩f {nothing ∷ f} {just i0 ∷ g} {nothing ∷ h} f<g f<h =   3⊆∩f {f} {g} {h} f<g f<h
3⊆∩f {nothing ∷ f} {just i1 ∷ g} {nothing ∷ h} f<g f<h =   3⊆∩f {f} {g} {h} f<g f<h
3⊆∩f {nothing ∷ f} {nothing ∷ g} {[]} f<g f<h = 3⊆∩f {f} {g} {[]} f<g f<h
3⊆∩f {nothing ∷ f} {nothing ∷ g} {just _ ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h
3⊆∩f {nothing ∷ f} {nothing ∷ g} {nothing ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h

3↑22 : (f : Nat → Two) (i j : Nat) → List (Maybe Two)
3↑22 f Zero j = []
3↑22 f (Suc i) j = just (f j) ∷ 3↑22 f i (Suc j)

_3↑_ : (Nat → Two) → Nat → List (Maybe Two)
_3↑_ f i = 3↑22 f i 0

3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (_3↑_ f x)  3⊆ (_3↑_ f y)
3↑< {f} {x} {y} x<y = lemma x y 0 x<y where
     lemma : (x y i : Nat) → x ≤ y → (3↑22 f x i ) 3⊆ (3↑22 f y i )
     lemma 0 y i z≤n with f i
     lemma Zero Zero i z≤n | i0 = refl
     lemma Zero (Suc y) i z≤n | i0 = 3⊆-[]  {3↑22 f (Suc y) i}
     lemma Zero Zero i z≤n | i1 = refl
     lemma Zero (Suc y) i z≤n | i1 = 3⊆-[]  {3↑22 f (Suc y) i}
     lemma (Suc x) (Suc y) i (s≤s x<y) with f i
     lemma (Suc x) (Suc y) i (s≤s x<y) | i0 = lemma x y (Suc i) x<y
     lemma (Suc x) (Suc y) i (s≤s x<y) | i1 = lemma x y (Suc i) x<y

Finite3b : (p : List (Maybe Two) ) → Bool
Finite3b [] = true
Finite3b (just _ ∷ f) = Finite3b f
Finite3b (nothing ∷ f) = false

finite3cov : (p : List (Maybe Two) ) → List (Maybe Two)
finite3cov [] = []
finite3cov (just y ∷ x) = just y ∷ finite3cov x
finite3cov (nothing ∷ x) = just i0 ∷ finite3cov x

Dense-3 : F-Dense (List (Maybe Two) ) (λ x → One) _3⊆_ _3∩_
Dense-3 = record {
       dense =  λ x → Finite3b x ≡ true
    ;  d⊆P = OneObj
    ;  dense-f = λ x → finite3cov x
    ;  dense-d = λ {p} d → lemma1 p
    ;  dense-p = λ {p} d → lemma2 p
  } where
      lemma1 : (p : List (Maybe Two) ) → Finite3b (finite3cov p) ≡ true
      lemma1 [] = refl
      lemma1 (just i0 ∷ p) = lemma1 p
      lemma1 (just i1 ∷ p) = lemma1 p
      lemma1 (nothing ∷ p) = lemma1 p
      lemma2 : (p : List (Maybe Two)) → p 3⊆ finite3cov p
      lemma2 [] = refl
      lemma2 (just i0 ∷ p) = lemma2 p
      lemma2 (just i1 ∷ p) = lemma2 p
      lemma2 (nothing ∷ p) = lemma2 p

-- min  = Data.Nat._⊓_
-- m≤m⊔n  = Data.Nat._⊔_
-- open import Data.Nat.Properties

max_stars_repo_name: shinji-kono/zf-in-agda

max_issues_repo_name: shinji-kono/zf-in-agda

max_forks_repo_name: shinji-kono/zf-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Pointwise lifting of a predicate to a binary tree
------------------------------------------------------------------------

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

module Data.Tree.Binary.Relation.Unary.All where

open import Level
open import Data.Tree.Binary as Tree using (Tree; leaf; node)
open import Relation.Unary

private
  variable
    a b p q : Level
    A : Set a
    B : Set b

data All {A : Set a} (P : A → Set p) : Tree A → Set (a ⊔ p) where
  leaf : All P leaf
  node : ∀ {l m r} → All P l → P m → All P r → All P (node l m r)

module _ {P : A → Set p} {Q : A → Set q} where

  map : ∀[ P ⇒ Q ] → ∀[ All P ⇒ All Q ]
  map f leaf         = leaf
  map f (node l m r) = node (map f l) (f m) (map f r)


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

--
-- Implementation of Sets using lists
--

open import Prelude

module Sets {i} (A : Set i) (eqdecA : eqdec A) where
  valid : list A → Set i
  valid l = ∀ x → has-all-paths (x ∈-list l)

  set = Σ (list A) (λ l → valid l)

  valid-nil : valid nil
  valid-nil _ ()

  Ø : set
  Ø = nil , valid-nil

  valid-singleton : ∀ (x : A) → valid (nil :: x)
  valid-singleton x y (inr p) (inr q) = ap inr (is-prop-has-all-paths (eqdec-is-set eqdecA y x) p q)

  singleton : ∀ A → set
  singleton x = (nil :: x) , valid-singleton x

  add-carrier : list A → A → list A
  add-carrier l a with dec-∈-list eqdecA a l
  ...             | inl _ = l
  ...             | inr _ = l :: a

  add-valid : ∀ (s : set) a → valid (add-carrier (fst s) a)
  add-valid (l , valid-l) a x b b' with dec-∈-list eqdecA a l
  ...                                     | inl x∈l = valid-l x b b'
  ...                                     | inr x∉l with eqdecA x a
  add-valid (l , valid-l) a .a (inl x∈l) b' | inr x∉l | inl idp = ⊥-elim (x∉l x∈l)
  add-valid (l , valid-l) a .a (inr _) (inl x∈l) | inr x∉l | inl idp = ⊥-elim (x∉l x∈l)
  add-valid (l , valid-l) a .a (inr p) (inr q) | inr x∉l | inl idp = ap inr (is-prop-has-all-paths (eqdec-is-set eqdecA a a) p q)
  add-valid (l , valid-l) a x (inl x∈l) (inl x∈'l) | inr x∉l | inr _ = ap inl (valid-l x x∈l x∈'l)
  add-valid (l , valid-l) a x (inl x∈l) (inr x=a) | inr x∉l | inr x≠a = ⊥-elim (x≠a x=a)
  add-valid (l , valid-l) a x (inr x=a) b' | inr x∉l | inr x≠a = ⊥-elim (x≠a x=a)

  add : ∀ (s : set) → A → set
  add s a = add-carrier (fst s) a , add-valid s a

  _∈-set_ : A → set → Set i
  a ∈-set s = a ∈-list (fst s)

  has-all-paths-∈-set : ∀ a s → has-all-paths (a ∈-set s)
  has-all-paths-∈-set a s = snd s a

  is-prop-∈-set : ∀ a s → is-prop (a ∈-set s)
  is-prop-∈-set a s = has-all-paths-is-prop (has-all-paths-∈-set a s)

  add+ : set → list A → set
  add+ s nil = s
  add+ s (l :: a) = add (add+ s l) a

  -- -- Very inefficient implementation of the union of sets
  -- _∪-set_ : set → set → set
  -- s ∪-set s' = add+ s (fst s')

  set-of-list : list A → set
  set-of-list l = add+ Ø l

  -- -- being in the list or in its set are logically equivalent
  -- -- but being in the set is a proposition
  -- -- achieves the construction of propositional truncation in a reduced way
  ∈-set-∈-list : ∀ a l → a ∈-set set-of-list l → a ∈-list l
  ∈-set-∈-list a (l :: b) a∈s with dec-∈-list eqdecA b (fst (add+ Ø l))
  ...                          | inl _ = inl (∈-set-∈-list a l a∈s)
  ...                          | inr _ with eqdecA a b
  ...                                   | inl idp = inr idp
  ∈-set-∈-list a (l :: b) (inl a∈s) | inr _ | inr _ = inl (∈-set-∈-list a l a∈s)
  ∈-set-∈-list a (l :: b) (inr idp) | inr _ | inr b≠b = inl (⊥-elim (b≠b idp))

  ∈-list-∈-set : ∀ a l → a ∈-list l → a ∈-set (set-of-list l)
  ∈-list-∈-set a (l :: b) a∈l+ with eqdecA a b
  ∈-list-∈-set a (l :: b) (inr a=b)  | inr a≠b = ⊥-elim (a≠b a=b)
  ∈-list-∈-set a (l :: b) (inl a∈l)  | inr a≠b with dec-∈-list eqdecA b (fst (add+ Ø l))
  ...                                            | inl _ = ∈-list-∈-set a l a∈l
  ...                                            | inr _ = inl (∈-list-∈-set a l a∈l)
  ∈-list-∈-set a (l :: b) a∈l+       | inl idp with dec-∈-list eqdecA b (fst (add+ Ø l))
  ...                                           | inl a∈l = a∈l
  ...                                           | inr _ = inr idp
  -- Note that these are not *really* sets : the order matters
  -- In particular the identity types are not correct

  _∪-set_ : set → set → set
  (s , _) ∪-set (s' , _) = set-of-list (s ++ s')

  _⊂_ : set → set → Set i
  A ⊂ B = ∀ x → x ∈-set A → x ∈-set B

  has-all-paths-→ : ∀ {i} (A B : Set i) → has-all-paths B → has-all-paths (A → B)
  has-all-paths-→ A B paths-B f g = funext f g (λ x → paths-B (f x) (g x))

  has-all-paths-∀ : ∀ {i} (A : Set i) (B : A → Set i) → (∀ a → has-all-paths (B a)) → has-all-paths (∀ a →  B a)
  has-all-paths-∀ A B paths-B f g = funext-dep f g λ a → paths-B a (f a) (g a)

  is-prop-→ : ∀ {i} A B →  is-prop {i} B → is-prop (A → B)
  is-prop-→ A B prop-B = has-all-paths-is-prop (has-all-paths-→ A B (is-prop-has-all-paths prop-B))

  is-prop-∀ : ∀ {i} (A : Set i) (B : A →  Set i) →  (∀ a → is-prop (B a)) → is-prop (∀ a → B a)
  is-prop-∀ A B prop-B = has-all-paths-is-prop (has-all-paths-∀ A B (λ a → is-prop-has-all-paths (prop-B a)))

  is-prop-⊂ : ∀ A B → is-prop (A ⊂ B)
  is-prop-⊂ A B = is-prop-∀ _ _ λ a → is-prop-→ _ _ (is-prop-∈-set a B)

  _≗_ : set → set → Set i
  A ≗ B = (A ⊂ B) × (B ⊂ A)

  has-all-paths-≗ : ∀ A B → has-all-paths (A ≗ B)
  has-all-paths-≗ A B (A⊂B , B⊂A) (A⊂'B , B⊂'A) = ,= (is-prop-has-all-paths (is-prop-⊂ A B) A⊂B A⊂'B) ((is-prop-has-all-paths (is-prop-⊂ B A) B⊂A B⊂'A))

  is-prop-≗ : ∀ A B → is-prop (A ≗ B)
  is-prop-≗ A B = has-all-paths-is-prop (has-all-paths-≗ A B)

  dec-∈ : ∀ A a → dec (a ∈-set A)
  dec-∈ (A , _) a with dec-∈-list eqdecA a A
  ... | inl a∈A = inl a∈A
  ... | inr a∉A = inr a∉A

  ∈++₁ : ∀ l l' (a : A) → a ∈-list l → a ∈-list (l ++ l')
  ∈++₁ l nil a x = x
  ∈++₁ l (l' :: a₁) a x = inl (∈++₁ l l' a x)

  ∈++₂ : ∀ l l' (a : A) → a ∈-list l' → a ∈-list (l ++ l')
  ∈++₂ l (l' :: a₁) a (inl a∈l') = inl (∈++₂ l l' a a∈l')
  ∈++₂ l (l' :: a₁) a (inr idp) = inr idp

  ∈++ : ∀ l l' (a : A) → a ∈-list (l ++ l') → (a ∈-list l) + (a ∈-list l')
  ∈++ l nil a x = inl x
  ∈++ l (l' :: a₁) a (inl x) with ∈++ l l' a x
  ... | inl a∈l = inl a∈l
  ... | inr a∈l' = inr (inl a∈l')
  ∈++ l (l' :: a₁) a (inr p) = inr (inr p)

  ∈-∪₁ : ∀ {A B a} → a ∈-set A → (a ∈-set (A ∪-set B))
  ∈-∪₁ {A , _} {B = nil , _} {a} a∈A = ∈-list-∈-set a (A ++ nil) a∈A
  ∈-∪₁ {A , _} {(B :: b) , _} {a} a∈A = ∈-list-∈-set a (A ++ (B :: b)) (inl (∈++₁ A B a a∈A))

  ∈-∪₂ : ∀ {A B a} → a ∈-set B  → (a ∈-set (A ∪-set B))
  ∈-∪₂ {A , _} {B = nil , _} {a} ()
  ∈-∪₂ {A , _} {(B :: b) , _} {a} (inl a∈B) = ∈-list-∈-set a (A ++ (B :: b)) (inl (∈++₂ A B a a∈B))
  ∈-∪₂ {A , _} {(B :: b) , _} {a} (inr idp) = ∈-list-∈-set a (A ++ (B :: b)) (inr idp)

  ∉-∪ : ∀ {A B a} → ¬ (a ∈-set A) → ¬ (a ∈-set B) → ¬ (a ∈-set (A ∪-set B))
  ∉-∪ {A , _} {B , _} {a} a∉A a∉B a∈A∪B with ∈++ A B a (∈-set-∈-list _ _ a∈A∪B)
  ... | inl x = a∉A x
  ... | inr x = a∉B x

  ∈-∪ : ∀ {A B a} →  a ∈-set (A ∪-set B) → (a ∈-set A) + (a ∈-set B)
  ∈-∪ {A , _} {B , _} {a} a∈A∪B with ∈++ A B a (∈-set-∈-list _ _ a∈A∪B)
  ... | inl x = inl x
  ... | inr x = inr x

  ⊂-∪ : ∀ {A B C D} → A ⊂ B → C ⊂ D → (A ∪-set C) ⊂ (B ∪-set D)
  ⊂-∪ {A} {B} {C} {D} A⊂B C⊂D a a∈A∪C with dec-∈ A a | dec-∈ C a
  ... | inl a∈A | _ = ∈-∪₁ {B} {D} {a} (A⊂B _ a∈A)
  ... | inr a∉A | inl a∈C = ∈-∪₂ {B} {D} {a} (C⊂D _ a∈C)
  ... | inr a∉A | inr a∉C = ⊥-elim (∉-∪ {A} {C} {a} a∉A a∉C a∈A∪C)

  ∪-factor : ∀ A B C → (A ∪-set (B ∪-set C)) ≗ ((A ∪-set B) ∪-set (A ∪-set C))
  fst (∪-factor A B C) x x∈A∪B∪C with ∈-∪ {A} {B ∪-set C} {x} x∈A∪B∪C
  ... | inl x∈A = ∈-∪₁ {A ∪-set B} {A ∪-set C} {x} (∈-∪₁ {A} {B} {x} x∈A)
  ... | inr x∈A∪B with ∈-∪ {B} {C} {x} x∈A∪B
  ... | inl x∈B = ∈-∪₁ {A ∪-set B} {A ∪-set C} {x} (∈-∪₂ {A} {B} {x} x∈B)
  ... | inr x∈C = ∈-∪₂ {A ∪-set B} {A ∪-set C} {x} (∈-∪₂ {A} {C} {x} x∈C)
  snd (∪-factor A B C) x x∈A∪B∪A∪C with ∈-∪ {A ∪-set B} {A ∪-set C} {x} x∈A∪B∪A∪C
  snd (∪-factor A B C) x x∈A∪B∪A∪C | inl x∈A∪B with ∈-∪ {A} {B} {x} x∈A∪B
  ... | inl x∈A = ∈-∪₁ {A} {B ∪-set C} {x} x∈A
  ... | inr x∈B = ∈-∪₂ {A} {B ∪-set C} {x} (∈-∪₁ {B} {C} {x} x∈B)
  snd (∪-factor A B C) x x∈A∪B∪A∪C | inr x∈A∪C with ∈-∪ {A} {C} {x} x∈A∪C
  ... | inl x∈A = ∈-∪₁ {A} {B ∪-set C} {x} x∈A
  ... | inr x∈C = ∈-∪₂ {A} {B ∪-set C} {x} (∈-∪₂ {B} {C} {x} x∈C)

  ≗-⊂ : ∀ {A B C} → A ≗ B → B ⊂ C → A ⊂ C
  ≗-⊂ (A⊂B , _) B⊂C _ a∈A = B⊂C _ (A⊂B _ a∈A)

  ⊂-trans : ∀ {A B C} → A ⊂ B → B ⊂ C → A ⊂ C
  ⊂-trans A⊂B B⊂C _ a∈A = B⊂C _ (A⊂B _ a∈A)

  ∈-singleton : ∀ a → a ∈-set (singleton a)
  ∈-singleton a = inr idp

  ∈-Ø : ∀ {x} → ¬ (x ∈-set Ø)
  ∈-Ø ()

  A∪B⊂A∪B∪C : ∀ A B C → (A ∪-set B) ⊂ (A ∪-set (B ∪-set C))
  A∪B⊂A∪B∪C A B C x x∈A∪B with ∈-∪ {A} {B} x∈A∪B
  ... | inl x∈A = ∈-∪₁ {A} {B ∪-set C} x∈A
  ... | inr x∈B = ∈-∪₂ {A} {B ∪-set C} (∈-∪₁ {B} {C} x∈B)

max_stars_repo_name: thibautbenjamin/catt-formalization

max_issues_repo_name: ThiBen/catt-formalization

max_forks_repo_name: ThiBen/catt-formalization


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

module Algebra.Construct.Free.Semilattice.Relation.Unary.Membership where

open import Prelude hiding (⊥; ⊤)
open import Algebra.Construct.Free.Semilattice.Eliminators
open import Algebra.Construct.Free.Semilattice.Definition
open import Cubical.Foundations.HLevels
open import Data.Empty.UniversePolymorphic
open import HITs.PropositionalTruncation.Sugar
open import HITs.PropositionalTruncation.Properties
open import HITs.PropositionalTruncation
open import Data.Unit.UniversePolymorphic
open import Algebra.Construct.Free.Semilattice.Relation.Unary.Any.Def

private
  variable p : Level

infixr 5 _∈_
_∈_ : {A : Type a} → A → 𝒦 A → Type a
x ∈ xs = ◇ (_≡ x) xs

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
{-# OPTIONS --cubical --save-metas #-}

open import Agda.Builtin.IO
open import Agda.Builtin.String
open import Agda.Builtin.Unit

open import Erased-cubical-Pattern-matching-Cubical
open import Erased-cubical-Pattern-matching-Erased

postulate
  putStr : String → IO ⊤

{-# FOREIGN GHC import qualified Data.Text.IO #-}
{-# COMPILE GHC putStr = Data.Text.IO.putStr #-}
{-# COMPILE JS putStr =
    function (x) {
      return function(cb) {
        process.stdout.write(x); cb(0); }; } #-}

main : IO ⊤
main = putStr (f c₁)


text:
------------------------------------------------------------------------------
-- Unary naturales numbers
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOTC.Data.Nat.UnaryNumbers where

open import FOTC.Base

------------------------------------------------------------------------------

0'  = zero
1'  = succ₁ 0'
2'  = succ₁ 1'
3'  = succ₁ 2'
4'  = succ₁ 3'
5'  = succ₁ 4'
6'  = succ₁ 5'
7'  = succ₁ 6'
8'  = succ₁ 7'
9'  = succ₁ 8'

{-# ATP definitions 0' 1' 2' 3' 4' 5' 6' 7' 8' 9' #-}

10' = succ₁ 9'
11' = succ₁ 10'
12' = succ₁ 11'
13' = succ₁ 12'
14' = succ₁ 13'
15' = succ₁ 14'
16' = succ₁ 15'
17' = succ₁ 16'
18' = succ₁ 17'
19' = succ₁ 18'

{-# ATP definition 10' 11' 12' 13' 14' 15' 16' 17' 18' 19' #-}

20' = succ₁ 19'
21' = succ₁ 20'
22' = succ₁ 21'
23' = succ₁ 22'
24' = succ₁ 23'
25' = succ₁ 24'
26' = succ₁ 25'
27' = succ₁ 26'
28' = succ₁ 27'
29' = succ₁ 28'

{-# ATP definition 20' 21' 22' 23' 24' 25' 26' 27' 28' 29' #-}

30' = succ₁ 29'
31' = succ₁ 30'
32' = succ₁ 31'
33' = succ₁ 32'
34' = succ₁ 33'
35' = succ₁ 34'
36' = succ₁ 35'
37' = succ₁ 36'
38' = succ₁ 37'
39' = succ₁ 38'

{-# ATP definition 30' 31' 32' 33' 34' 35' 36' 37' 38' 39' #-}

40' = succ₁ 39'
41' = succ₁ 40'
42' = succ₁ 41'
43' = succ₁ 42'
44' = succ₁ 43'
45' = succ₁ 44'
46' = succ₁ 45'
47' = succ₁ 46'
48' = succ₁ 47'
49' = succ₁ 48'

{-# ATP definition 40' 41' 42' 43' 44' 45' 46' 47' 48' 49' #-}

50' = succ₁ 49'
51' = succ₁ 50'
52' = succ₁ 51'
53' = succ₁ 52'
54' = succ₁ 53'
55' = succ₁ 54'
56' = succ₁ 55'
57' = succ₁ 56'
58' = succ₁ 57'
59' = succ₁ 58'

{-# ATP definition 50' 51' 52' 53' 54' 55' 56' 57' 58' 59' #-}

60' = succ₁ 59'
61' = succ₁ 60'
62' = succ₁ 61'
63' = succ₁ 62'
64' = succ₁ 63'
65' = succ₁ 64'
66' = succ₁ 65'
67' = succ₁ 66'
68' = succ₁ 67'
69' = succ₁ 68'

{-# ATP definition 60' 61' 62' 63' 64' 65' 66' 67' 68' 69' #-}

70' = succ₁ 69'
71' = succ₁ 70'
72' = succ₁ 71'
73' = succ₁ 72'
74' = succ₁ 73'
75' = succ₁ 74'
76' = succ₁ 75'
77' = succ₁ 76'
78' = succ₁ 77'
79' = succ₁ 78'

{-# ATP definition 70' 71' 72' 73' 74' 75' 76' 77' 78' 79' #-}

80' = succ₁ 79'
81' = succ₁ 80'
82' = succ₁ 81'
83' = succ₁ 82'
84' = succ₁ 83'
85' = succ₁ 84'
86' = succ₁ 85'
87' = succ₁ 86'
88' = succ₁ 87'
89' = succ₁ 88'

{-# ATP definition 80' 81' 82' 83' 84' 85' 86' 87' 88' 89' #-}

90' = succ₁ 89'
91' = succ₁ 90'
92' = succ₁ 91'
93' = succ₁ 92'
94' = succ₁ 93'
95' = succ₁ 94'
96' = succ₁ 95'
97' = succ₁ 96'
98' = succ₁ 97'
99' = succ₁ 98'

{-# ATP definition 90' 91' 92' 93' 94' 95' 96' 97' 98' 99' #-}

100' = succ₁ 99'
101' = succ₁ 100'
102' = succ₁ 101'
103' = succ₁ 102'
104' = succ₁ 103'
105' = succ₁ 104'
106' = succ₁ 105'
107' = succ₁ 106'
108' = succ₁ 107'
109' = succ₁ 108'

{-# ATP definition 100' 101' 102' 103' 104' 105' 106' 107' 108' 109' #-}

110' = succ₁ 109'
111' = succ₁ 110'
{-# ATP definition 110' 111' #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --universe-polymorphism #-}
module Support.FinSet where

open import Support
open import Support.Nat

unbound : ∀ {n} (m : Fin n) → ℕ
unbound zero = zero
unbound {suc n} (suc y) = suc (unbound {n} y)

.Fin-is-bounded : ∀ (n : ℕ) (m : Fin n) → (unbound m < n)
Fin-is-bounded .(suc n) (zero {n}) = Z<Sn
Fin-is-bounded .(suc n) (suc {n} y) = raise< (Fin-is-bounded n y)

enlarge : ∀ {a} (b : Fin (suc a)) (c : Fin (unbound b)) → Fin a
enlarge {zero} zero ()
enlarge {zero} (suc ()) c
enlarge {suc a′} zero ()
enlarge {suc a′} (suc b′) zero = zero
enlarge {suc a′} (suc b′) (suc c′) = suc (enlarge b′ c′)

widen-by : ∀ {a} {b} (a≤b : a < suc b) (c : Fin a) → Fin b
widen-by Z<Sn ()
widen-by (raise< Z<Sn) zero = zero
widen-by (raise< (raise< n<m)) zero = zero
widen-by (raise< Z<Sn) (suc ())
widen-by (raise< (raise< n<m)) (suc y') = suc (widen-by (raise< n<m) y')

widen-+ : (b : ℕ) → ∀ {a} (c : Fin a) → Fin (a + b)
widen-+ b zero = zero
widen-+ b (suc y) = suc (widen-+ b y)

shift : (a : ℕ) → ∀ {b} (c : Fin b) → Fin (a + b)
shift zero c = c
shift (suc y) c = suc (shift y c)

_bounded-by_ : (m : ℕ) → ∀ {n} (m<n : m < n) → Fin n
.0 bounded-by Z<Sn = zero
.(suc n) bounded-by (raise< {n} n<m) = suc (n bounded-by n<m)

unbound-unbounds-bounded-by : ∀ (m n : ℕ) (m<n : m < n) → unbound (m bounded-by m<n) ≣ m
unbound-unbounds-bounded-by .0 .(suc n) (Z<Sn {n}) = ≣-refl
unbound-unbounds-bounded-by .(suc n) .(suc m) (raise< {n} {m} n<m) = ≣-cong suc (unbound-unbounds-bounded-by n m n<m)

_lessen_ : (n : ℕ) → (m : Fin (suc n)) → ℕ
n lessen zero = n
.0 lessen suc {zero} ()
.(suc y) lessen suc {suc y} y' = y lessen y'

lessen-is-subtraction₁ : ∀ (n : ℕ) (m : Fin (suc n)) → (unbound m + (n lessen m)) ≣ n
lessen-is-subtraction₁ n zero = ≣-refl
lessen-is-subtraction₁ .0 (suc {zero} ())
lessen-is-subtraction₁ .(suc y) (suc {suc y} y') = ≣-cong suc (lessen-is-subtraction₁ y y')

lessen-is-subtraction₂ : ∀ (n m : ℕ) → ((n + m) lessen (n bounded-by (+-is-nondecreasingʳ n m)) ≣ m)
lessen-is-subtraction₂ zero m = ≣-refl
lessen-is-subtraction₂ (suc y) m = lessen-is-subtraction₂ y m

_split_ : ∀ {n} (k : Fin n) (m : Fin (suc n)) → Either (Fin (unbound m)) (Fin (n lessen m))
k split zero = inr k
zero split suc y = inl zero
suc y split suc y' = left suc (y split y')

_chops_ : (n : ℕ) → ∀ {m} (k : Fin (n + m)) → Either (Fin n) (Fin m)
0 chops k = inr k
suc n chops zero = inl zero
suc n chops suc k = left suc (n chops k)

rejoin-chops : (n m : ℕ) (k : Fin (n + m)) → either₀ (widen-+ m) (shift n) (n chops k) ≣ k
rejoin-chops zero _ _ = ≣-refl
rejoin-chops (suc _) _ zero = ≣-refl
rejoin-chops (suc n') m (suc k') with n' chops k' | rejoin-chops n' m k'
rejoin-chops (suc _) _ (suc ._) | inl _ | ≣-refl = ≣-refl
rejoin-chops (suc _) _ (suc ._) | inr _ | ≣-refl = ≣-refl

chop-widen-+ : (n m : ℕ) (k : Fin n) → n chops widen-+ m k ≣ inl k
chop-widen-+ zero _ ()
chop-widen-+ (suc n') _ zero = ≣-refl
chop-widen-+ (suc n') m (suc k') with n' chops widen-+ m k' | chop-widen-+ n' m k'
chop-widen-+ (suc n') m (suc ._) | inl k' | ≣-refl = ≣-refl
chop-widen-+ (suc n') m (suc _) | inr _ | ()

chop-shift : (n m : ℕ) (k : Fin m) → n chops shift n k ≣ inr k
chop-shift zero m k = ≣-refl
chop-shift (suc n') m k = ≣-cong (left suc) (chop-shift n' m k)

_cat₀_ : ∀ {ℓ} {n m} {A : Set ℓ} (f : Fin n → A) (g : Fin m → A) → Fin (n + m) → A
_cat₀_ {n = n} {m} f g i = either₀ f g (n chops i)

∙-dist-cat₀ : ∀ {ℓ ℓ′} {n m} {A : Set ℓ} {A′ : Set ℓ′} (f : Fin n → A) (g : Fin m → A) (h : A → A′) {i : Fin (n + m)} → (h ∙ (f cat₀ g)) i ≣ ((h ∙ f) cat₀ (h ∙ g)) i
∙-dist-cat₀ {n = n} {A′ = A′} f g h {i} = answer
  where
  open ≣-reasoning A′
  split-i = n chops i
  answer = begin
      ((h ∙ (f cat₀ g)) i)
    ≈⟨ ≣-refl ⟩
      (h ((f cat₀ g) i))
    ≈⟨ ≣-cong h ≣-refl ⟩
      h (either₀ f g split-i)
    ≈⟨ ≣-refl ⟩
      (h ∙ either₀ f g) split-i
    ≈⟨ ∙-dist-either₀ f g h {split-i} ⟩
      either₀ (h ∙ f) (h ∙ g) split-i
    ≈⟨ ≣-refl ⟩
      ((h ∙ f) cat₀ (h ∙ g)) i
    ∎

_cat_ : ∀ {ℓ} {n m} {A : Fin n → Set ℓ} {B : Fin m → Set ℓ} (f : (i : Fin n) → A i) (g : (j : Fin m) → B j) → (k : Fin (n + m)) → (A cat₀ B) k
_cat_ {n = n} f g i = either f g (n chops i)

_cat′_ : ∀ {ℓ} {n m} {A : Fin (n + m) → Set ℓ} (f : (i : Fin n) → A (widen-+ m i)) (g : (j : Fin m) → A (shift n j)) → (k : Fin (n + m)) → A k
_cat′_ {n = n} {m = m} {A = T} f g k = ≣-subst T (rejoin-chops n m k) (either′ {A = T ∙ either₀ (widen-+ m) (shift n)} f g (n chops k))

_✂_ : ∀ {n} (m : Fin (suc n)) {ℓ} {A : Set ℓ} (f : Fin n → A) → (Fin (unbound m) → A) × (Fin (n lessen m) → A)
_✂_ {n = n} m f = f ∙ enlarge m , f ∙ (≣-subst Fin (lessen-is-subtraction₁ n m) ∙ shift (unbound m))

_✂₀′_ : (m : ℕ) → ∀ {ℓ} {A : Set ℓ} {n} (f : Fin (m + n) → A) → (Fin m → A) × (Fin n → A)
_✂₀′_ m {n = n} f = f ∙ widen-+ n , f ∙ shift m

_✂′_ : (m : ℕ) → ∀ {ℓ} {n} {A : Fin (m + n) → Set ℓ} (f : (k : Fin (m + n)) → A k) → uncurry₀ _×_ (⟨ (λ Aˡ → (i : Fin m) → Aˡ i) , (λ Aʳ → (j : Fin n) → Aʳ j) ⟩ (m ✂₀′ A))
_✂′_ m {n = n} f = f ∙ widen-+ n , f ∙ shift m

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
------------------------------------------------------------------------------
-- Miscellaneous properties
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOTC.Program.SortList.Properties.MiscellaneousI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Bool
open import FOTC.Data.Bool.PropertiesI
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.List.PropertiesI
open import FOTC.Data.Nat.List.Type
open import FOTC.Data.Nat.Type
open import FOTC.Data.List
open import FOTC.Data.List.PropertiesI
open import FOTC.Program.SortList.Properties.Totality.BoolI
open import FOTC.Program.SortList.SortList

------------------------------------------------------------------------------
-- This is a weird result but recall that "the relation ≤ between
-- lists is only an ordering if nil is excluded" (Burstall 1969,
-- p. 46).
-- xs≤[] : ∀ {is} → ListN is → OrdList is → LE-Lists is []
-- xs≤[] lnnil                     _       = ≤-Lists-[] []
-- xs≤[] (lncons {i} {is} Ni LNis) LOconsL =
--   begin
--     ≤-Lists (i ∷ is) []
--       ≡⟨ ≤-Lists-∷ i is [] ⟩
--     ≤-ItemList i [] && ≤-Lists is []
--       ≡⟨ subst (λ t → ≤-ItemList i [] && ≤-Lists is [] ≡ t && ≤-Lists is [])
--                (≤-ItemList-[] i)
--                refl
--       ⟩
--     true && ≤-Lists is []
--       ≡⟨ subst (λ t → true && ≤-Lists is [] ≡ true && t)
--                (xs≤[] LNis (subList-OrdList Ni LNis LOconsL))
--                refl
--       ⟩
--     true && true
--       ≡⟨ &&-tt ⟩
--     true
--   ∎

x≤ys++zs→x≤zs : ∀ {i js ks} → N i → ListN js → ListN ks →
                ≤-ItemList i (js ++ ks) → ≤-ItemList i ks
x≤ys++zs→x≤zs {i} {ks = ks} Ni lnnil LNks  i≤[]++ks =
  subst (≤-ItemList i) (++-leftIdentity ks) i≤[]++ks
x≤ys++zs→x≤zs {i} {ks = ks} Ni (lncons {j} {js} Nj LNjs) LNks i≤j∷js++ks =
  x≤ys++zs→x≤zs Ni LNjs LNks lemma₂
  where
  lemma₁ : le i j && le-ItemList i (js ++ ks) ≡ true
  lemma₁ =
    le i j && le-ItemList i (js ++ ks)
      ≡⟨ sym (le-ItemList-∷ i j (js ++ ks)) ⟩
    le-ItemList i (j ∷ (js ++ ks))
      ≡⟨ subst (λ t → le-ItemList i (j ∷ (js ++ ks)) ≡ le-ItemList i t)
               (sym (++-∷ j js ks))
               refl
      ⟩
    le-ItemList i ((j ∷ js) ++ ks) ≡⟨ i≤j∷js++ks ⟩
    true ∎

  lemma₂ : ≤-ItemList i (js ++ ks)
  lemma₂ = &&-list₂-t₂ (le-Bool Ni Nj)
                       (le-ItemList-Bool Ni (++-ListN LNjs LNks))
                       lemma₁

xs++ys-OrdList→xs≤ys : ∀ {is js} → ListN is → ListN js →
                       OrdList (is ++ js) → ≤-Lists is js
xs++ys-OrdList→xs≤ys {js = js} lnnil LNjs OLis++js = le-Lists-[] js
xs++ys-OrdList→xs≤ys {js = js} (lncons {i} {is} Ni LNis) LNjs OLis++js =
  le-Lists (i ∷ is) js
    ≡⟨ le-Lists-∷ i is js ⟩
  le-ItemList i js && le-Lists is js
    ≡⟨ subst (λ t → le-ItemList i js && le-Lists is js ≡
                    t && le-Lists is js)
             (x≤ys++zs→x≤zs Ni LNis LNjs lemma₁)
             refl
    ⟩
  true && le-Lists is js
    ≡⟨ subst (λ t → true && le-Lists is js ≡ true && t)
             (xs++ys-OrdList→xs≤ys LNis LNjs lemma₂)  --IH.
             refl
    ⟩
  true && true
    ≡⟨ t&&x≡x true ⟩
  true ∎
  where
  lemma₀ : le-ItemList i (is ++ js) && ordList (is ++ js) ≡ true
  lemma₀ = trans (sym (ordList-∷ i (is ++ js)))
                 (trans (subst (λ t → ordList (i ∷ is ++ js) ≡ ordList t)
                               (sym (++-∷ i is js))
                               refl)
                 OLis++js)

  helper₁ : Bool (le-ItemList i (is ++ js))
  helper₁ = le-ItemList-Bool Ni (++-ListN LNis LNjs)

  helper₂ : Bool (ordList (is ++ js))
  helper₂ = ordList-Bool (++-ListN LNis LNjs)

  lemma₁ : le-ItemList i (is ++ js) ≡ true
  lemma₁ = &&-list₂-t₁ helper₁ helper₂ lemma₀

  lemma₂ : ordList (is ++ js) ≡ true
  lemma₂ = &&-list₂-t₂ helper₁ helper₂ lemma₀

x≤ys→x≤zs→x≤ys++zs : ∀ {i js ks} → N i → ListN js → ListN ks →
                     ≤-ItemList i js →
                     ≤-ItemList i ks →
                     ≤-ItemList i (js ++ ks)
x≤ys→x≤zs→x≤ys++zs {i} {ks = ks} Ni lnnil LNks _ i≤k =
  subst (≤-ItemList i) (sym (++-leftIdentity ks)) i≤k
x≤ys→x≤zs→x≤ys++zs {i} {ks = ks} Ni (lncons {j} {js} Nj LNjs) LNks i≤j∷js i≤k =
  le-ItemList i ((j ∷ js) ++ ks)
    ≡⟨ subst (λ t → le-ItemList i ((j ∷ js) ++ ks) ≡
                    le-ItemList i t)
             (++-∷ j js ks)
             refl
    ⟩
  le-ItemList i (j ∷ (js ++ ks))
    ≡⟨ le-ItemList-∷ i j (js ++ ks) ⟩
  le i j && le-ItemList i (js ++ ks)
    ≡⟨ subst₂ (λ t₁ t₂ → le i j && le-ItemList i (js ++ ks) ≡ t₁ && t₂)
              (&&-list₂-t₁ helper₁ helper₂ helper₃)
              (x≤ys→x≤zs→x≤ys++zs Ni LNjs LNks
                                  (&&-list₂-t₂ helper₁ helper₂ helper₃)
                                  i≤k)
              refl
    ⟩
  true && true
    ≡⟨ t&&x≡x true ⟩
  true ∎
  where
  helper₁ : Bool (le i j)
  helper₁ = le-Bool Ni Nj

  helper₂ : Bool (le-ItemList i js)
  helper₂ = le-ItemList-Bool Ni LNjs

  helper₃ : le i j && (le-ItemList i js) ≡ true
  helper₃ = trans (sym (le-ItemList-∷ i j js)) i≤j∷js

xs≤ys→xs≤zs→xs≤ys++zs : ∀ {is js ks} → ListN is → ListN js → ListN ks →
                        ≤-Lists is js →
                        ≤-Lists is ks →
                        ≤-Lists is (js ++ ks)
xs≤ys→xs≤zs→xs≤ys++zs lnnil LNjs LNks _ _ = le-Lists-[] _
xs≤ys→xs≤zs→xs≤ys++zs {js = js} {ks} (lncons {i} {is} Ni LNis)
                      LNjs LNks i∷is≤js i∷is≤ks =
  le-Lists (i ∷ is) (js ++ ks)
    ≡⟨ le-Lists-∷ i is (js ++ ks)  ⟩
  le-ItemList i (js ++ ks) && le-Lists is (js ++ ks)
    ≡⟨ subst (λ t → le-ItemList i (js ++ ks) && le-Lists is (js ++ ks) ≡
                    t                       && le-Lists is (js ++ ks))
             (x≤ys→x≤zs→x≤ys++zs Ni LNjs LNks
                                 (&&-list₂-t₁ helper₁ helper₂ helper₃)
                                 (&&-list₂-t₁ helper₄ helper₅ helper₆))
             refl
    ⟩
  true && le-Lists is (js ++ ks)
    ≡⟨ subst (λ t → true && le-Lists is (js ++ ks) ≡ true && t)
             (xs≤ys→xs≤zs→xs≤ys++zs LNis LNjs LNks
                                    (&&-list₂-t₂ helper₁ helper₂ helper₃)
                                    (&&-list₂-t₂ helper₄ helper₅ helper₆))
             refl
    ⟩
  true && true
    ≡⟨ t&&x≡x true ⟩
  true ∎
  where
  helper₁ = le-ItemList-Bool Ni LNjs
  helper₂ = le-Lists-Bool LNis LNjs
  helper₃ = trans (sym (le-Lists-∷ i is js)) i∷is≤js

  helper₄ = le-ItemList-Bool Ni LNks
  helper₅ = le-Lists-Bool LNis LNks
  helper₆ = trans (sym (le-Lists-∷ i is ks)) i∷is≤ks

xs≤zs→ys≤zs→xs++ys≤zs : ∀ {is js ks} → ListN is → ListN js → ListN ks →
                        ≤-Lists is ks →
                        ≤-Lists js ks →
                        ≤-Lists (is ++ js) ks
xs≤zs→ys≤zs→xs++ys≤zs {js = js} {ks} lnnil LNjs LNks is≤ks js≤ks =
  subst (λ t → ≤-Lists t ks)
        (sym (++-leftIdentity js))
        js≤ks
xs≤zs→ys≤zs→xs++ys≤zs {js = js} {ks}
                      (lncons {i} {is} Ni LNis) LNjs LNks i∷is≤ks js≤ks =
  le-Lists ((i ∷ is) ++ js) ks
    ≡⟨ subst (λ t → le-Lists ((i ∷ is) ++ js) ks ≡ le-Lists t ks)
             (++-∷ i is js)
             refl
    ⟩
    le-Lists (i ∷ (is ++ js)) ks
    ≡⟨ le-Lists-∷ i (is ++ js) ks ⟩
  le-ItemList i ks && le-Lists (is ++ js) ks
    ≡⟨ subst₂ (λ x y → le-ItemList i ks && le-Lists (is ++ js) ks ≡ x && y)
              ≤-ItemList-i-ks
              ≤-Lists-is++js-ks
              refl
    ⟩
  true && true
    ≡⟨ t&&x≡x true ⟩
  true ∎
  where
  helper₁ = le-ItemList-Bool Ni LNks
  helper₂ = le-Lists-Bool LNis LNks
  helper₃ = trans (sym (le-Lists-∷ i is ks)) i∷is≤ks

  ≤-ItemList-i-ks : ≤-ItemList i ks
  ≤-ItemList-i-ks = &&-list₂-t₁ helper₁ helper₂ helper₃

  ≤-Lists-is++js-ks : ≤-Lists (is ++ js) ks
  ≤-Lists-is++js-ks =
    xs≤zs→ys≤zs→xs++ys≤zs LNis LNjs LNks
                          (&&-list₂-t₂ helper₁ helper₂ helper₃)
                          js≤ks

------------------------------------------------------------------------------
-- References
--
-- Burstall, R. M. (1969). Proving properties of programs by
-- structural induction. The Computer Journal 12.1, pp. 41–48.


text:
-- We use Kalmar's lemma to show completeness. See
-- https://iep.utm.edu/prop-log/
-- http://comet.lehman.cuny.edu/mendel/Adlogic/sem5.pdf

{-# OPTIONS --without-K --safe #-}
module Kalmar where

-- imports from stdlib.
import Data.Empty as DE
open import Data.Bool using (Bool ; not ; false ; true)

open import Data.Nat using (ℕ ; _≟_)
open import Data.Nat.Properties using (≡-decSetoid)

open import Data.Product renaming (_,_ to _,'_) using (_×_)

open import Data.List using (List ; map ; _++_ ; deduplicate ; _∷_ ; [])
open import Data.List.Relation.Unary.Unique.DecSetoid ≡-decSetoid using (Unique ; [] ; _∷_)
open import Data.List.Membership.DecPropositional _≟_ renaming (_∈_ to _∈ℕ_) using (_∉_)

open import Relation.Nullary as RN using (yes ; no)
open import Data.List.Relation.Unary.Any using (Any ; here ; there)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong₂)

-- imports from my files.
open import PropLogic

-- ----------------------------------------------------------------------
-- Inspect.

-- When "f x" evaluates to some "y", pattern matching on "Inspect (f
-- x)" gives "y" and the proof that "f x ≡ y". We use this vesion of
-- inspect instead of the one in PropositionalEquality for convenience.
data Inspect {A : Set}(x : A) : Set where
  it : (y : A) -> x ≡ y -> Inspect x

inspect : {A : Set}(x : A) -> Inspect x
inspect x = it x refl

-- ----------------------------------------------------------------------
-- Definitons and lemmas.

-- Fix a formula by possibly negating it such that under the given
-- assignment, the fixed formula is true.
fix-formula : Assign -> Formula -> Formula
fix-formula a f with interp a f
... | true =  f
... | false = ¬ f

-- Fix a symbol by possibly negating it such that under the given
-- assignment, the fixed symbol is true. We call a natural number a
-- "symbol". (Recall P n is the nth propositional symbol)
fix-sym : Assign -> ℕ -> Formula
fix-sym a n with a n
... | true = P n
... | false = ¬ (P n)

-- Given an assignment and a list of symbols, return a context
-- consisting of "fixed symbols". We call a list of natural numbers
-- "symbol context" or "sctx". (recall context is a list of
-- formulas)
fix-sctx : Assign -> List ℕ -> Context
fix-sctx a = map (fix-sym a)

-- Given an assignment "a", and a symbol "v", return an new
-- assignment that negate "a v", and is the same as "a" in all other
-- symbols.
negate-assign-at : Assign -> ℕ -> (ℕ -> Bool)
negate-assign-at a m n with m ≟ n
... | no ¬p = a n
... | yes p = not (a n)

-- Lemmas about negate-assign-at.
lemma1-negate-assign-at : ∀ {a m n} -> RN.¬ (m ≡ n) -> negate-assign-at a m n ≡ a n
lemma1-negate-assign-at {a} {m} {n} neq with (m ≟ n)
... | yes p  = DE.⊥-elim (neq p)
... | no _ = refl

lemma2-negate-assign-at : ∀ {a m n} -> (m ≡ n) -> negate-assign-at a m n ≡ not (a n)
lemma2-negate-assign-at {a} {m} {.m} refl with m ≟ m
... | no ¬p = DE.⊥-elim (¬p refl)
... | yes p = refl

lemma-fix-sym : ∀ {a m n} -> RN.¬ m ≡ n -> fix-sym (negate-assign-at a m) n ≡ fix-sym a n
lemma-fix-sym {a} {m} {n} neq rewrite lemma1-negate-assign-at {a} {m} {n} neq = refl

lemma-fix-sym-neg : ∀ {a n} -> (a n ≡ false) -> fix-sym (negate-assign-at a n) n ≡ (P n)
lemma-fix-sym-neg {a} {n} eq with  lemma2-negate-assign-at {a} {n} {n} refl
... | hyp rewrite hyp  | eq = refl

lemma-fix-sym-pos : ∀ {a n} -> (a n ≡ true) -> fix-sym (negate-assign-at a n) n ≡ ¬ (P n)
lemma-fix-sym-pos {a} {n} eq with  lemma2-negate-assign-at {a} {n} {n} refl
... | hyp rewrite hyp  | eq = refl

-- A lemma about fix-sctx.
lemma-fix-sctx : ∀ {a ns n} -> n ∉ ns -> fix-sctx (negate-assign-at a n) ns ≡ fix-sctx a ns
lemma-fix-sctx {a} {Empty} {n} nin = refl
lemma-fix-sctx {a} {ns , x} {n} nin = cong₂ _,_ (lemma-fix-sctx n∉ns) (lemma-fix-sym claim)
  where
    open import Data.List.Relation.Unary.Any using (there ; here)
    n∉ns : n ∉ ns
    n∉ns = λ x₁ → nin (there x₁)
    claim : RN.¬ n ≡ x
    claim = λ x₁ → nin (here x₁)

-- Given a formula, return the list of all the symbol in it
-- (allowing repeation).
syms-of-formula : Formula -> List ℕ
syms-of-formula (P x) = x ∷ []
syms-of-formula (A ∧ B) = (syms-of-formula A) ++ (syms-of-formula B)
syms-of-formula (A ⇒ B) = (syms-of-formula A) ++ (syms-of-formula B)
syms-of-formula ⊥ = []
syms-of-formula ⊤ = []
syms-of-formula (¬ f) = syms-of-formula f
syms-of-formula (A ∨ B) = (syms-of-formula A) ++ (syms-of-formula B)

-- De Morgan's law.
demorg : ∀ {Γ A B} -> Γ ⊢ (¬ A) ∧ (¬ B) -> Γ ⊢ ¬ (A ∨ B)
demorg der = ¬-intro (∨-elim (assump ∈-base) (¬-elim (∧-elim1 (weakening der (λ z → ∈-step (∈-step z)))) (assump ∈-base)) ((¬-elim (∧-elim2 (weakening der (λ z → ∈-step (∈-step z)))) (assump ∈-base))))

demorg1 : ∀ {Γ A B} -> Γ ⊢ (¬ A) ∨ (¬ B) -> Γ ⊢ ¬ (A ∧ B)
demorg1 der = ¬-intro (∨-elim (weakening der ∈-step) (¬-elim (assump ∈-base) (∧-elim1 (assump (∈-step ∈-base)))) ((¬-elim (assump ∈-base) (∧-elim2 (assump (∈-step ∈-base))))))

-- Implication with a null hypothesis is always syntactically valid.
null-hyp : ∀ {Γ A B} -> Γ ⊢ (¬ A) -> Γ ⊢ A ⇒ B
null-hyp der = ⇒-intro (⊥-elim (¬-elim (weakening der ∈-step) (assump ∈-base)))

-- Implication with a null conclusion is always syntactically invalid.
null-conclusion : ∀ {Γ A B} -> Γ ⊢ A -> Γ ⊢ (¬ B) -> Γ ⊢ ¬ (A ⇒ B)
null-conclusion der1 der2 = ¬-intro (¬-elim (weakening der2 ∈-step) (⇒-elim (assump ∈-base) (weakening der1 ∈-step)))

-- Double negation of "A" is valid if "A" is valid.
double-negate : ∀ {Γ A} -> Γ ⊢ A -> Γ ⊢ ¬ (¬ A)
double-negate der = ¬-intro (¬-elim (assump ∈-base) (weakening der ∈-step))

-- ----------------------------------------------------------------------
-- List containment.

-- In file "Logic", membership and context containment are defined
-- similarly but differently from the one in stdlib. we have to do a
-- translation.
infix 3 _⊂_
_⊂_ : List ℕ ->  List ℕ -> Set
xs ⊂ ys = ∀ {x} -> x ∈ℕ xs -> x ∈ℕ ys

-- Lemma: membership is functorial.
lemma-fix-sym-∈ : ∀ {ρ} {x} {ys} -> x ∈ℕ ys -> fix-sym ρ x ∈ fix-sctx ρ ys
lemma-fix-sym-∈ {ρ} {x} {.(_ , x₁)} (here {x₁} px) rewrite px = ∈-base
lemma-fix-sym-∈ {ρ} {x} {.(xs , x₁)} (there {x₁} {xs} hyp) = ∈-step (lemma-fix-sym-∈ hyp)

-- Lemma: removing the head element preserves containment.
lemma-⊂-rh : ∀ {x : ℕ} {xs ys} -> (x ∷ xs) ⊂ ys -> xs ⊂ ys
lemma-⊂-rh {x} {.(_ , _)} {ys} sub (here px) rewrite px = sub (there (here refl))
lemma-⊂-rh {x} {.(_ , _)} {ys} sub (there hyp) = sub (there (there hyp))

-- Lemma: List containment is functorial.
lemma-map : ∀ {ρ xs ys} -> xs ⊂ ys -> fix-sctx ρ xs ⊆ fix-sctx ρ ys
lemma-map {ρ} {Empty} {ys} sub = λ {()}
lemma-map {ρ} {xs , x} {ys} sub = λ { ∈-base → lemma-fix-sym-∈ (sub (here refl)) ; (∈-step x₁) → lemma-map (lemma-⊂-rh sub) x₁}

-- ----------------------------------------------------------------------
-- Kalmar's Lemma.

mutual
  -- We use aux to abstract over similar codes.
  aux : ∀ ρ F G ->
    let Γ = fix-sctx ρ (syms-of-formula F ++ syms-of-formula G) in
    Γ ⊢ (fix-formula ρ F) × Γ ⊢ (fix-formula ρ G)
  aux ρ F G = let vl = syms-of-formula F in let vr = syms-of-formula G in
      weakening (lemma-Kalmar {F} ρ) (lemma-map {ρ} {vl} {vl ++ vr} ∈-++⁺ˡ)
      ,' weakening (lemma-Kalmar {G} ρ) (lemma-map {ρ} {vr} {vl ++ vr} (∈-++⁺ʳ vl {ys = vr}))
      where
        open import Data.List.Membership.Propositional.Properties using (∈-++⁺ˡ ; ∈-++⁺ʳ)

  lemma-Kalmar : ∀ {F} ρ -> fix-sctx ρ (syms-of-formula F) ⊢ fix-formula ρ F
  lemma-Kalmar {P x} ρ  with ρ x
  ... | true =  assump ∈-base
  ... | false = assump ∈-base
  lemma-Kalmar {F ∧ F₁} ρ with inspect (interp ρ F) | inspect (interp ρ F₁) | aux ρ F F₁
  ... | it false x | it false x₁ | iha ,' ihb rewrite x | x₁ = demorg1 (∨-intro2 ihb)
  ... | it false x | it true x₁ | iha ,' ihb rewrite x | x₁ = demorg1 (∨-intro1 iha)
  ... | it true x | it false x₁ | iha ,' ihb rewrite x | x₁ = demorg1 (∨-intro2 ihb)
  ... | it true x | it true x₁ | iha ,' ihb rewrite x | x₁ = ∧-intro iha ihb
  lemma-Kalmar {F ⇒ F₁} ρ with inspect (interp ρ F) | inspect (interp ρ F₁) | aux ρ F F₁
  ... | it true x | it true x₁ | iha ,' ihb rewrite x | x₁  = ⇒-intro (weakening ihb ∈-step)
  ... | it false x | it true x₁ | iha ,' ihb rewrite x | x₁  = ⇒-intro (weakening ihb ∈-step)
  ... | it true x | it false x₁ | iha ,' ihb rewrite x | x₁  = null-conclusion iha ihb
  ... | it false x | it false x₁ | iha ,' ihb rewrite x | x₁  = null-hyp iha
  lemma-Kalmar {F ∨ F₁} ρ with inspect (interp ρ F) | inspect (interp ρ F₁) | aux ρ F F₁
  ... | it true x | it true x₁ | iha ,' ihb rewrite x | x₁  = ∨-intro1 iha
  ... | it false x | it true x₁ | iha ,' ihb rewrite x | x₁  = ∨-intro2 ihb
  ... | it true x | it false x₁ | iha ,' ihb rewrite x | x₁  = ∨-intro1 iha
  ... | it false x | it false x₁ | iha ,' ihb rewrite x | x₁  = demorg (∧-intro iha ihb)
  lemma-Kalmar  {⊥} ρ = ¬-intro (assump ∈-base)
  lemma-Kalmar  {⊤} ρ = ⊤-intro
  lemma-Kalmar  {¬ F}  ρ with inspect (interp ρ F) | lemma-Kalmar {F} ρ
  ... | it false x | ih rewrite x = ih
  ... | it true x | ih rewrite x = double-negate ih

-- ----------------------------------------------------------------------
-- Unique symbol context.

-- The idea is that the deduplicated symbol context is as strong as
-- the original one. For the former, we can make two assignments such
-- that they only differs at one symbol, i.e. the head symbol. Then by
-- using ∨-elim we can reduce the symbol context by removing the head.

-- Lemma: "symbol context version" of weakening.
weakening-sym : ∀ {ρ xs ys F} -> xs ⊂ ys -> fix-sctx ρ xs ⊢ F -> fix-sctx ρ ys ⊢ F
weakening-sym {ρ} {xs} {ys} {F} sub hyp = weakening hyp (lemma-map sub)

-- Lemma: Deduplicated symbol ctx is as strong as the original ctx.
lemma-dedup : ∀ {ρ xs F} ->  fix-sctx ρ xs ⊢ F -> fix-sctx ρ (deduplicate _≟_ xs) ⊢ F
lemma-dedup {xs = xs} = weakening-sym λ x → ∈-deduplicate⁺ _≟_ {xs} x
 where
   open import Data.List.Membership.Propositional.Properties using (∈-deduplicate⁺)

-- law of excluded middle is derivable.
ex-mid : ∀ {A} -> Empty ⊢ (¬ A) ∨ A
ex-mid {A} = ∨-elim step (∨-intro1 (¬-intro (⇒-elim (assump (∈-step ∈-base)) (assump ∈-base)))) (∨-intro2 (double-negation (⇒-intro (⇒-elim (assump (∈-step ∈-base)) (¬-intro (⇒-elim (assump (∈-step ∈-base)) (assump ∈-base)))))))
  where
    demorgan : ∀ {A B} -> Empty ⊢ ((A ∧ B) ⇒ ⊥) ⇒ (A ⇒ ⊥) ∨ (B ⇒ ⊥)
    demorgan = ⇒-intro (double-negation (⇒-intro (⇒-elim (assump ∈-base) (∨-intro1 (⇒-intro (⇒-elim (assump (∈-step ∈-base)) (∨-intro2 (⇒-intro (⇒-elim (assump (∈-step (∈-step (∈-step ∈-base)))) (∧-intro (assump (∈-step ∈-base)) (assump ∈-base)))))))))))
    step : Empty ⊢ ((A ⇒ ⊥) ∨ ((¬ A) ⇒ ⊥))
    step = ⇒-elim (demorgan {A} {¬ A}) (⇒-intro (¬-elim (∧-elim2 (assump ∈-base)) (∧-elim1 (assump ∈-base))))
-- ∨-elim instantiated using excluded middle.
∨-elim-exmid : ∀ {Γ A B} -> Γ , ¬ A ⊢ B -> Γ , A ⊢ B -> Γ ⊢ B
∨-elim-exmid {Γ} {A} {b} d e = ∨-elim (weakening ex-mid lemma-⊆-empty) d e

-- Lemma: Removing one symbol from symbol context.
lemma-sctx-reduce : ∀ {ρ ns n F} -> (n ∉ ns) ->
  fix-sctx ρ (n ∷ ns) ⊢ F ->
  fix-sctx (negate-assign-at ρ n) (n ∷ ns) ⊢ F ->
  fix-sctx ρ ns ⊢ F
lemma-sctx-reduce {ρ} {ns} {n} {F} nin h1 h2 with inspect (ρ n)
... | it false pf rewrite (lemma-fix-sctx {a = ρ} nin) | lemma-fix-sym-neg {ρ} {n} pf | pf = ∨-elim-exmid h1 h2
... | it true pf rewrite (lemma-fix-sctx {a = ρ} nin) | lemma-fix-sym-pos {ρ} {n} pf | pf = ∨-elim-exmid h2 h1

-- lemma: if the symbol ctx is unique, we can repeatedly use
-- lemma-sctx-reduce to get an Empty context.
lemma-unique-ctx-reduce : ∀ {F} {ns : List ℕ} -> Unique (ns) -> (∀ ρ -> fix-sctx ρ ns ⊢ F) -> Empty ⊢ F
lemma-unique-ctx-reduce {F} {.Empty} [] hyp = hyp (λ _ → false)
lemma-unique-ctx-reduce {F} {.(xs , x₁)} (_∷_ {x = x₁} {xs = xs} x uns) hyp = ih
  where
    open import Data.List.Relation.Unary.All
    open import Function
    anyAll : ∀ {ys : List ℕ} {Pd : ℕ -> Set} -> Any Pd ys -> RN.¬ (All (RN.¬_ ∘ Pd) ys)
    anyAll {.(_ , _)} {Pd} (here px) (px₁ ∷ all₁) = px₁ px
    anyAll {.(xs , _)} {Pd} (there {xs = xs} any₁) (px ∷ all₁) = anyAll {xs} {Pd} any₁ all₁
    x₁∉xs : x₁ ∉ xs
    x₁∉xs h = anyAll h x
    ih : Empty ⊢ F
    ih = lemma-unique-ctx-reduce {F} {xs} uns λ ρ → lemma-sctx-reduce {ρ} {xs} {x₁} {F} x₁∉xs (hyp ρ) (hyp (negate-assign-at ρ x₁))

-- ----------------------------------------------------------------------
-- Completeness.

-- lemma-Kalmar instantiated with semantical entailment.
lemma-Kalmar-⊧ : ∀ {ρ F} -> Empty ⊧ F -> fix-sctx ρ (syms-of-formula F) ⊢ F
lemma-Kalmar-⊧ {ρ} {F} st with lemma-Kalmar {F} ρ | st ρ refl
... | kal | Ft rewrite Ft = kal

-- lemma-dedup instantiated with semantical entailment.
lemma-dedup-⊧ : ∀ {F} -> Empty ⊧ F -> (∀ ρ -> fix-sctx ρ (deduplicate _≟_  (syms-of-formula F)) ⊢ F)
lemma-dedup-⊧ st = λ ρ → lemma-dedup (lemma-Kalmar-⊧ (λ ρ _ → st ρ refl))

-- | Completeness in empty context.
completeness-empty : ∀ {F} -> Empty ⊧ F -> Empty ⊢ F
completeness-empty {F} st = lemma-unique-ctx-reduce (deduplicate-! ≡-decSetoid (syms-of-formula F)) (lemma-dedup-⊧ {F} st)
  where
    open import Data.List.Relation.Unary.Unique.DecSetoid.Properties using (deduplicate-!)

-- | completeness-property.
completeness : ∀ Γ A -> Γ ⊧ A -> Γ ⊢ A
completeness Empty A hyp = completeness-empty {A} hyp
completeness (Γ , B) A hyp = ⇒-elim (weakening (completeness Γ (B ⇒ A) (lemma-⇒-intro Γ B A hyp)) ∈-step) (assump ∈-base)

max_stars_repo_name: onestruggler/Kalmar

max_issues_repo_name: onestruggler/Kalmar

max_forks_repo_name: onestruggler/Kalmar


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.ZCohomology.Groups.Sn where

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.Groups.Unit
open import Cubical.ZCohomology.Groups.Connected
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.Groups.Prelims

open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws

open import Cubical.HITs.Pushout
open import Cubical.HITs.Sn
open import Cubical.HITs.S1
open import Cubical.HITs.Susp
open import Cubical.HITs.SetTruncation renaming (rec to sRec ; elim to sElim ; elim2 to sElim2 ; map to sMap)
open import Cubical.HITs.PropositionalTruncation renaming (rec to pRec ; elim to pElim ; elim2 to pElim2 ; ∥_∥ to ∥_∥₁ ; ∣_∣ to ∣_∣₁) hiding (map)

open import Cubical.Data.Bool
open import Cubical.Data.Sigma
open import Cubical.Data.Int renaming (_+_ to _+ℤ_; +-comm to +ℤ-comm ; +-assoc to +ℤ-assoc)
open import Cubical.Data.Nat
open import Cubical.HITs.Truncation renaming (elim to trElim ; map to trMap ; rec to trRec)
open import Cubical.Data.Unit

open import Cubical.Homotopy.Connected

open import Cubical.Algebra.Group

infixr 31 _□_
_□_ : _
_□_ = compGroupIso

open GroupEquiv
open vSES
open GroupIso
open GroupHom
open BijectionIso

Sn-connected : (n : ℕ) (x : typ (S₊∙ (suc n))) → ∥ pt (S₊∙ (suc n)) ≡ x ∥₁
Sn-connected zero = toPropElim (λ _ → propTruncIsProp) ∣ refl ∣₁
Sn-connected (suc zero) = suspToPropElim base (λ _ → propTruncIsProp) ∣ refl ∣₁
Sn-connected (suc (suc n)) = suspToPropElim north (λ _ → propTruncIsProp) ∣ refl ∣₁

H⁰-Sⁿ≅ℤ : (n : ℕ) → GroupIso (coHomGr 0 (S₊ (suc n))) intGroup
H⁰-Sⁿ≅ℤ zero = H⁰-connected base (Sn-connected 0)
H⁰-Sⁿ≅ℤ (suc n) = H⁰-connected north (Sn-connected (suc n))

-- -- ----------------------------------------------------------------------

--- We will need to switch between Sⁿ defined using suspensions and using pushouts
--- in order to apply Mayer Vietoris.

S1Iso : Iso S¹ (Pushout {A = Bool} (λ _ → tt) λ _ → tt)
S1Iso = S¹IsoSuspBool ⋄ invIso PushoutSuspIsoSusp

coHomPushout≅coHomSn : (n m : ℕ) → GroupIso (coHomGr m (S₊ (suc n)))
                                             (coHomGr m (Pushout {A = S₊ n} (λ _ → tt) λ _ → tt))
coHomPushout≅coHomSn zero m =
  Iso+Hom→GrIso (setTruncIso (domIso S1Iso))
                (sElim2 (λ _ _ → isSet→isGroupoid setTruncIsSet _ _) (λ _ _ → refl))
coHomPushout≅coHomSn (suc n) m =
  Iso+Hom→GrIso (setTruncIso (domIso (invIso PushoutSuspIsoSusp)))
                (sElim2 (λ _ _ → isSet→isGroupoid setTruncIsSet _ _) (λ _ _ → refl))

-------------------------- H⁰(S⁰) -----------------------------
S0→Int : (a : Int × Int) → S₊ 0 → Int
S0→Int a true = fst a
S0→Int a false = snd a

H⁰-S⁰≅ℤ×ℤ : GroupIso (coHomGr 0 (S₊ 0)) (dirProd intGroup intGroup)
fun (map H⁰-S⁰≅ℤ×ℤ) = sRec (isSet× isSetInt isSetInt) λ f → (f true) , (f false)
isHom (map H⁰-S⁰≅ℤ×ℤ) = sElim2 (λ _ _ → isSet→isGroupoid (isSet× isSetInt isSetInt) _ _)
                                λ a b → refl
inv H⁰-S⁰≅ℤ×ℤ a = ∣ S0→Int a ∣₂
rightInv H⁰-S⁰≅ℤ×ℤ _ = refl
leftInv H⁰-S⁰≅ℤ×ℤ = sElim (λ _ → isSet→isGroupoid setTruncIsSet _ _)
                           λ f → cong ∣_∣₂ (funExt (λ {true → refl ; false → refl}))

------------------------- H¹(S⁰) ≅ 0 -------------------------------

private
  Hⁿ-S0≃Kₙ×Kₙ : (n : ℕ) → Iso (S₊ 0 → coHomK (suc n)) (coHomK (suc n) × coHomK (suc n))
  Iso.fun (Hⁿ-S0≃Kₙ×Kₙ n) f = (f true) , (f false)
  Iso.inv (Hⁿ-S0≃Kₙ×Kₙ n) (a , b) true = a
  Iso.inv (Hⁿ-S0≃Kₙ×Kₙ n) (a , b) false = b
  Iso.rightInv (Hⁿ-S0≃Kₙ×Kₙ n) a = refl
  Iso.leftInv (Hⁿ-S0≃Kₙ×Kₙ n) b = funExt λ {true → refl ; false → refl}

  isContrHⁿ-S0 : (n : ℕ) → isContr (coHom (suc n) (S₊ 0))
  isContrHⁿ-S0 n = isContrRetract (Iso.fun (setTruncIso (Hⁿ-S0≃Kₙ×Kₙ n)))
                                  (Iso.inv (setTruncIso (Hⁿ-S0≃Kₙ×Kₙ n)))
                                  (Iso.leftInv (setTruncIso (Hⁿ-S0≃Kₙ×Kₙ n)))
                                  (isContrHelper n)
    where
    isContrHelper : (n : ℕ) → isContr (∥ (coHomK (suc n) × coHomK (suc n)) ∥₂)
    fst (isContrHelper zero) = ∣ (0₁ , 0₁) ∣₂
    snd (isContrHelper zero) = sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                                  λ y → elim2 {B = λ x y → ∣ (0₁ , 0₁) ∣₂ ≡ ∣(x , y) ∣₂ }
                                  (λ _ _ → isOfHLevelPlus {n = 2} 2 setTruncIsSet _ _)
                                  (toPropElim2 (λ _ _ → setTruncIsSet _ _) refl) (fst y) (snd y)
    isContrHelper (suc zero) = ∣ (0₂ , 0₂) ∣₂
                          , sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                                  λ y → elim2 {B = λ x y → ∣ (0₂ , 0₂) ∣₂ ≡ ∣(x , y) ∣₂ }
                                  (λ _ _ → isOfHLevelPlus {n = 2} 3 setTruncIsSet _ _)
                                  (suspToPropElim2 base (λ _ _ → setTruncIsSet _ _) refl) (fst y) (snd y)
    isContrHelper (suc (suc n)) = ∣ (0ₖ (3 + n) , 0ₖ (3 + n)) ∣₂
                          , sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                                  λ y → elim2 {B = λ x y → ∣ (0ₖ (3 + n) , 0ₖ (3 + n)) ∣₂ ≡ ∣(x , y) ∣₂ }
                                  (λ _ _ → isProp→isOfHLevelSuc (4 + n) (setTruncIsSet _ _))
                                  (suspToPropElim2 north (λ _ _ → setTruncIsSet _ _) refl) (fst y) (snd y)

H¹-S⁰≅0 : (n : ℕ) → GroupIso (coHomGr (suc n) (S₊ 0)) trivialGroup
H¹-S⁰≅0 n = IsoContrGroupTrivialGroup (isContrHⁿ-S0 n)

------------------------- H²(S¹) ≅ 0 -------------------------------

Hⁿ-S¹≅0 : (n : ℕ) → GroupIso (coHomGr (2 + n) (S₊ 1)) trivialGroup
Hⁿ-S¹≅0 n = IsoContrGroupTrivialGroup
            (isOfHLevelRetractFromIso 0 helper
              (_ , helper2))
  where
  helper : Iso ⟨ coHomGr (2 + n) (S₊ 1)⟩ ∥ Σ (hLevelTrunc (4 + n) (S₊ (2 + n))) (λ x → ∥ x ≡ x ∥₂) ∥₂
  helper = compIso (setTruncIso IsoFunSpaceS¹) IsoSetTruncateSndΣ

  helper2 : (x : ∥ Σ (hLevelTrunc (4 + n) (S₊ (2 + n))) (λ x → ∥ x ≡ x ∥₂) ∥₂) → ∣ ∣ north ∣ , ∣ refl ∣₂ ∣₂ ≡ x
  helper2 =
    sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
          (uncurry
            (trElim (λ _ → isOfHLevelΠ (4 + n) λ _ → isProp→isOfHLevelSuc (3 + n) (setTruncIsSet _ _))
              (suspToPropElim (ptSn (suc n)) (λ _ → isPropΠ λ _ → setTruncIsSet _ _)
                (sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                       λ p
                    → cong ∣_∣₂ (ΣPathP (refl , isContr→isProp helper3 _ _))))))
    where
    helper4 : isConnected (n + 3) (hLevelTrunc (4 + n) (S₊ (2 + n)))
    helper4 = subst (λ m → isConnected m (hLevelTrunc (4 + n) (S₊ (2 + n)))) (+-comm 3 n)
                    (isOfHLevelRetractFromIso 0 (invIso (truncOfTruncIso (3 + n) 1)) (sphereConnected (2 + n)))

    helper3 : isContr ∥ ∣ north ∣ ≡ ∣ north ∣ ∥₂
    helper3 = isOfHLevelRetractFromIso 0 setTruncTrunc2Iso
                                         (isConnectedPath 2 (isConnectedSubtr 3 n helper4) _ _)

-- --------------- H¹(Sⁿ), n ≥ 1 --------------------------------------------

H¹-Sⁿ≅0 : (n : ℕ) → GroupIso (coHomGr 1 (S₊ (2 + n))) trivialGroup
H¹-Sⁿ≅0 zero = IsoContrGroupTrivialGroup isContrH¹S²
  where
  isContrH¹S² : isContr ⟨ coHomGr 1 (S₊ 2) ⟩
  isContrH¹S² = ∣ (λ _ → ∣ base ∣) ∣₂
              , coHomPointedElim 0 north (λ _ → setTruncIsSet _ _)
                   λ f p → cong ∣_∣₂ (funExt λ x → sym p ∙∙ sym (spoke f north) ∙∙ spoke f x)
H¹-Sⁿ≅0 (suc n) = IsoContrGroupTrivialGroup isContrH¹S³⁺ⁿ
  where
  anIso : Iso ⟨ coHomGr 1 (S₊ (3 + n)) ⟩ ∥ (S₊ (3 + n) → hLevelTrunc (4 + n) (coHomK 1)) ∥₂
  anIso =
    setTruncIso
      (codomainIso
        (invIso (truncIdempotentIso (4 + n) (isOfHLevelPlus' {n = 1 + n} 3 (isOfHLevelTrunc 3)))))

  isContrH¹S³⁺ⁿ-ish : (f : (S₊ (3 + n) → hLevelTrunc (4 + n) (coHomK 1)))
                   → ∣ (λ _ → ∣ ∣ base ∣ ∣) ∣₂ ≡ ∣ f ∣₂
  isContrH¹S³⁺ⁿ-ish f = ind (f north) refl
    where
    ind : (x : hLevelTrunc (4 + n) (coHomK 1))
       → x ≡ f north
       → ∣ (λ _ → ∣ ∣ base ∣ ∣) ∣₂ ≡ ∣ f ∣₂
    ind = trElim (λ _ → isOfHLevelΠ (4 + n) λ _ → isOfHLevelPlus' {n = (3 + n)} 1 (setTruncIsSet _ _))
              (trElim (λ _ → isOfHLevelΠ 3 λ _ → isOfHLevelPlus {n = 1} 2 (setTruncIsSet _ _))
              (toPropElim (λ _ → isPropΠ λ _ → setTruncIsSet _ _)
              λ p → cong ∣_∣₂ (funExt λ x → p ∙∙ sym (spoke f north) ∙∙ spoke f x)))
  isContrH¹S³⁺ⁿ : isContr ⟨ coHomGr 1 (S₊ (3 + n)) ⟩
  isContrH¹S³⁺ⁿ =
    isOfHLevelRetractFromIso 0
      anIso
      (∣ (λ _ → ∣ ∣ base ∣ ∣) ∣₂
      , sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _) isContrH¹S³⁺ⁿ-ish)

--------- H¹(S¹) ≅ ℤ -------
{-
Idea :
H¹(S¹) := ∥ S¹ → K₁ ∥₂
        ≃ ∥ S¹ → S¹ ∥₂
        ≃ ∥ S¹ × ℤ ∥₂
        ≃ ∥ S¹ ∥₂ × ∥ ℤ ∥₂
        ≃ ℤ
-}
coHom1S1≃ℤ : GroupIso (coHomGr 1 (S₊ 1)) intGroup
coHom1S1≃ℤ = theIso
  where
  F = Iso.fun S¹→S¹≡S¹×Int
  F⁻ = Iso.inv S¹→S¹≡S¹×Int

  theIso : GroupIso (coHomGr 1 (S₊ 1)) intGroup
  fun (map theIso) = sRec isSetInt (λ f → snd (F f))
  isHom (map theIso) =
    coHomPointedElimS¹2 _ (λ _ _ → isSetInt _ _)
      λ p q → (λ i → winding (guy ∣ base ∣ (cong S¹map (help p q i))))
            ∙∙ (λ i → winding (guy ∣ base ∣ (congFunct S¹map p q i)))
            ∙∙ winding-hom (guy ∣ base ∣ (cong S¹map p))
                           (guy ∣ base ∣ (cong S¹map q))

    where
    guy = basechange2⁻ ∘ S¹map
    help : (p q : Path (coHomK 1) ∣ base ∣ ∣ base ∣) → cong₂ _+ₖ_ p q ≡ p ∙ q
    help p q = cong₂Funct _+ₖ_ p q ∙ (λ i → cong (λ x → rUnitₖ 1 x i) p ∙ cong (λ x → lUnitₖ 1 x i) q)
  inv theIso a = ∣ (F⁻ (base , a)) ∣₂
  rightInv theIso a = cong snd (Iso.rightInv S¹→S¹≡S¹×Int (base , a))
  leftInv theIso = sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                          λ f → cong ((sRec setTruncIsSet ∣_∣₂)
                                        ∘ sRec setTruncIsSet λ x → ∣ F⁻ (x , (snd (F f))) ∣₂)
                                      (Iso.inv PathIdTrunc₀Iso (isConnectedS¹ (fst (F f))))
                              ∙ cong ∣_∣₂ (Iso.leftInv S¹→S¹≡S¹×Int f)

---------------------------- Hⁿ(Sⁿ) ≅ ℤ , n ≥ 1 -------------------
{-
The proof of the inductive step below is a compact version of the following equations. Let n ≥ 1.
Hⁿ⁺¹(Sⁿ⁺¹) := ∥ Sⁿ⁺¹ → Kₙ₊₁ ∥₂
           ≅ ∥ Σ[ (a , b) ∈ Kₙ₊₁ ] (Sⁿ → a ≡ b) ∥₂       (characterisation of functions from suspensions)
           ≅ ∥ Kₙ₊₁ × Kₙ₊₁ × (Sⁿ → ΩKₙ₊₁) ∥₂             (base change in ΩKₙ₊₁)
           ≅ ∥ Kₙ₊₁ ∥₂ × ∥ Kₙ₊₁ ∥₂ × ∥ (Sⁿ → ΩKₙ₊₁) ∥₂
           ≅ ∥ Sⁿ → ΩKₙ₊₁ ∥₂                             (connectivity of Kₙ₊₁)
           ≅ ∥ Sⁿ → Kₙ ∥₂                                (ΩKₙ₊₁ ≃ Kₙ)
          := Hⁿ(Sⁿ)
           ≅ ℤ                                           (ind. hyp)

The inverse function Hⁿ(Sⁿ) → Hⁿ⁺¹(Sⁿ⁺¹) is just the function d from Mayer-Vietoris.
However, we can construct d⁻¹ directly in this case, thus avoiding computationally
heavier proofs concerning exact sequences. -}

Hⁿ-Sⁿ≅ℤ : (n : ℕ) → GroupIso (coHomGr (suc n) (S₊ (suc n))) intGroup
Hⁿ-Sⁿ≅ℤ zero = coHom1S1≃ℤ
Hⁿ-Sⁿ≅ℤ (suc n) = invGroupIso helper □ invGroupIso (coHom≅coHomΩ (suc n) _) □ (Hⁿ-Sⁿ≅ℤ n)
  where
  basePointInd : (p : _) (a : _)
    → (p (ptSn (suc n)) ≡ refl) → sym (rCancelₖ (2 + n) ∣ north ∣)
                                 ∙∙ (λ i →  (elimFunSⁿ (suc n) n p) ((merid a ∙ sym (merid (ptSn (suc n)))) i) +ₖ ∣ north ∣)
                                 ∙∙ rCancelₖ (2 + n) ∣ north ∣
                               ≡ p a
  basePointInd p a prefl =
        cong (λ z → sym z ∙∙ ((λ i →  (elimFunSⁿ (suc n) n p) ((merid a ∙ sym (merid (ptSn (suc n)))) i) +ₖ ∣ north ∣)) ∙∙ z)
             (transportRefl refl)
     ∙∙ sym (rUnit _)
     ∙∙ (λ j i → rUnitₖ (2 + n) (elimFunSⁿ (suc n) n p ((merid a ∙ sym (merid (ptSn (suc n)))) i)) j)
     ∙∙ congFunct (elimFunSⁿ (suc n) n p) (merid a) (sym (merid (ptSn (suc n))))
     ∙∙ (cong (p a ∙_) (cong sym prefl)
     ∙ sym (rUnit (p a)))

  helper : GroupIso (coHomGrΩ (suc n) (S₊ (suc n))) (coHomGr (2 + n) (S₊ (2 + n)))
  fun (map helper) = sMap λ f → λ { north → ∣ north ∣
                                   ; south → ∣ north ∣
                                   ; (merid a i) → f a i}
  isHom (map helper) =
    sElim2 (λ _ _ → isOfHLevelPath 2 setTruncIsSet _ _)
           λ f g → cong ∣_∣₂ (funExt λ { north → refl
                                       ; south → refl
                                       ; (merid a i) j → ∙≡+₂ n (f a) (g a) j i})
  inv helper = sMap λ f x → sym (rCancelₖ (2 + n) (f north))
                          ∙∙ (λ i → f ((merid x ∙ sym (merid (ptSn (suc n)))) i) -ₖ f north)
                          ∙∙ rCancelₖ (2 + n) (f north)
  rightInv helper =
    coHomPointedElimSⁿ (suc n) n (λ _ → setTruncIsSet _ _)
      λ p → trRec (isProp→isOfHLevelSuc n (setTruncIsSet _ _))
                   (λ prefl → cong ∣_∣₂ (funExt λ {north → refl
                                                 ; south → refl
                                                 ; (merid a i) j → basePointInd p a prefl j i}))
                   (Iso.fun (PathIdTruncIso _)
                            (isOfHLevelSuc 0 (isConnectedPathKn _ ∣ north ∣ ∣ north ∣)
                            (∣ p (ptSn (suc n)) ∣) ∣ refl ∣))
  leftInv helper =
    sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
          λ f → (trRec (isProp→isOfHLevelSuc n (setTruncIsSet _ _))
                        (λ frefl → cong ∣_∣₂ (funExt λ x → basePointInd f x frefl))
                        ((Iso.fun (PathIdTruncIso _)
                            (isOfHLevelSuc 0 (isConnectedPathKn _ ∣ north ∣ ∣ north ∣)
                            (∣ f (ptSn (suc n)) ∣) ∣ refl ∣))))

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
id : Set → Set
id A = A

F : Set → Set → Set
F _*_ = G
  where
  G : Set → Set
  G _*_ = id _*_

G : Set → Set → Set
G _*_ = λ _*_ → id _*_

H : Set → Set → Set
H = λ _*_ _*_ → id _*_

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Cubical.Algebra.Base public
open import Cubical.Algebra.Definitions public
open import Cubical.Algebra.Structures public
open import Cubical.Algebra.Bundles public

open import Cubical.Classes public


text:
open import agdaExamples public
open import Blockchain public
open import Crypto public
open import examples public
open import lambdaCalculus
open import Ledger public
open import proofsTXTree public
open import RawTransactions public
open import RawTXTree public
open import Transactions public
open import TXTree public
open import Utils public

max_stars_repo_name: guilhermehas/crypto-agda

max_issues_repo_name: guilhermehas/cripto-agda

max_forks_repo_name: guilhermehas/cripto-agda


text:
------------------------------------------------------------------------
-- Parallel substitutions (defined using an inductive family)
------------------------------------------------------------------------

open import Data.Universe.Indexed

module deBruijn.Substitution.Data
  {i u e} {Uni : IndexedUniverse i u e} where

import deBruijn.Context; open deBruijn.Context Uni
open import Function as F using (_$_)
open import Level using (_⊔_)
import Relation.Binary.PropositionalEquality as P

open P.≡-Reasoning

-- This module reexports some other modules.

open import deBruijn.Substitution.Data.Application public
open import deBruijn.Substitution.Data.Basics      public
open import deBruijn.Substitution.Data.Map         public
open import deBruijn.Substitution.Data.Simple      public

------------------------------------------------------------------------
-- Instantiations and code for facilitating instantiations

-- Renamings (variable substitutions).

module Renaming where

  -- Variables support all of the operations above.

  simple : Simple Var
  simple = record
    { weaken     = weaken∋
    ; var        = [id]
    ; weaken-var = λ _ → P.refl
    }

  application : Application Var Var
  application = record { app = app∋ }

  application₁ : Application₁ Var
  application₁ = record
    { simple        = simple
    ; application₂₂ = record
      { application₂₁ = record
        { application  = application
        ; trans-weaken = λ _ → P.refl
        ; trans-var    = λ _ → P.refl
        ; var-/⊢       = λ _ _ → P.refl
        }
      ; var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆ = λ _ _ hyp → hyp
      ; /⊢-wk                 = Simple./∋-wk simple
      }
    }

  open Application₁ application₁ public hiding (simple; application)

  ≅-∋-⇒-≅-⊢ : ∀ {Γ₁ σ₁} {x₁ : Γ₁ ∋ σ₁}
                {Γ₂ σ₂} {x₂ : Γ₂ ∋ σ₂} →
              x₁ ≅-∋ x₂ → Term-like._≅-⊢_ Var x₁ x₂
  ≅-∋-⇒-≅-⊢ P.refl = P.refl

  ≅-⊢-⇒-≅-∋ : ∀ {Γ₁ σ₁} {x₁ : Γ₁ ∋ σ₁}
                {Γ₂ σ₂} {x₂ : Γ₂ ∋ σ₂} →
              Term-like._≅-⊢_ Var x₁ x₂ → x₁ ≅-∋ x₂
  ≅-⊢-⇒-≅-∋ P.refl = P.refl

-- A translation of T₁'s to T₂'s, plus a bit more.

record _↦_ {t₁} (T₁ : Term-like t₁)
           {t₂} (T₂ : Term-like t₂) : Set (i ⊔ u ⊔ e ⊔ t₁ ⊔ t₂) where
  field
    -- Translates T₁'s to T₂'s.
    trans : [ T₁ ⟶⁼ T₂ ]

    -- Simple substitutions for T₁'s.
    simple : Simple T₁

  open Simple simple public

  open Term-like T₁ renaming (⟦_⟧ to ⟦_⟧₁)
  open Term-like T₂ renaming (⟦_⟧ to ⟦_⟧₂)

  /̂∋-⟦⟧⇨ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (x : Γ ∋ σ) (ρ : Sub T₁ ρ̂) →
           x /̂∋ ⟦ ρ ⟧⇨ ≅-Value ⟦ trans · (x /∋ ρ) ⟧₂
  /̂∋-⟦⟧⇨ x ρ = begin
    [ x /̂∋ ⟦ ρ ⟧⇨           ]  ≡⟨ corresponds (app∋ ρ) x ⟩
    [ ⟦ x /∋ ρ ⟧₁           ]  ≡⟨ corresponds trans (x /∋ ρ) ⟩
    [ ⟦ trans · (x /∋ ρ) ⟧₂ ]  ∎

-- "Term" substitutions.

-- For simplicity I have chosen to use the universe level (i ⊔ u ⊔ e)
-- here; this is the level of Var. The code could perhaps be made more
-- general.

record Substitution₁ (T : Term-like (i ⊔ u ⊔ e))
                     : Set (Level.suc (i ⊔ u ⊔ e)) where

  open Term-like T

  field
    -- Takes variables to terms.
    var : [ Var ⟶⁼ T ]

    -- Applies substitutions, which contain things which can be
    -- translated to terms, to terms.
    app′ : {T′ : Term-like (i ⊔ u ⊔ e)} → T′ ↦ T →
           ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Sub T′ ρ̂ → [ T ⟶ T ] ρ̂

    -- A property relating app′ and var.
    app′-var :
      ∀ {T′ : Term-like (i ⊔ u ⊔ e)} {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ}
      (T′↦T : T′ ↦ T) (x : Γ ∋ σ) (ρ : Sub T′ ρ̂) →
      app′ T′↦T ρ · (var · x) ≅-⊢ _↦_.trans T′↦T · (x /∋ ρ)

  -- Variables can be translated into terms.

  private

    Var-↦′ : Var ↦ T
    Var-↦′ = record
      { trans  = var
      ; simple = Renaming.simple
      }

  -- Renamings can be applied to terms.

  app-renaming : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Sub Var ρ̂ → [ T ⟶ T ] ρ̂
  app-renaming = app′ Var-↦′

  -- This gives us a way to define the weakening operation.

  simple : Simple T
  simple = record
    { weaken     = app-renaming Renaming.wk
    ; var        = var
    ; weaken-var = weaken-var
    }
    where
    abstract
      weaken-var : ∀ {Γ σ τ} (x : Γ ∋ τ) →
                   app-renaming (Renaming.wk[_] σ) · (var · x) ≅-⊢
                   var · suc[ σ ] x
      weaken-var x = begin
        [ app-renaming Renaming.wk · (var · x) ]  ≡⟨ app′-var Var-↦′ x Renaming.wk ⟩
        [ var · (x /∋ Renaming.wk)             ]  ≡⟨ ·-cong (var ∎-⟶) (Renaming./∋-wk x) ⟩
        [ var · suc x                          ]  ∎

  -- A translation of T′'s to T's, plus a bit more.

  record Translation-from (T′ : Term-like (i ⊔ u ⊔ e))
                          : Set (i ⊔ u ⊔ e) where

    field
      translation : T′ ↦ T

    open _↦_ translation
      using (trans)
      renaming (simple to simple′; var to var′; weaken[_] to weaken′[_])

    field
      trans-weaken : ∀ {Γ σ τ} (t : Term-like._⊢_ T′ Γ τ) →
                     trans · (weaken′[ σ ] · t) ≅-⊢
                     Simple.weaken[_] simple σ · (trans · t)
      trans-var    : ∀ {Γ σ} (x : Γ ∋ σ) →
                     trans · (var′ · x) ≅-⊢ var · x

    -- An Application₂₁ record.

    application₂₁ : Application₂₁ simple′ simple trans
    application₂₁ = record
      { application  = record { app = app′ translation }
      ; trans-weaken = trans-weaken
      ; trans-var    = trans-var
      ; var-/⊢       = app′-var translation
      }

    open _↦_ translation public
    open Application₂₁ application₂₁ public
      hiding (trans-weaken; trans-var)

  -- Variables can be translated into terms.

  Var-↦ : Translation-from Var
  Var-↦ = record
    { translation  = Var-↦′
    ; trans-weaken = trans-weaken
    ; trans-var    = λ _ → P.refl
    }
    where
    abstract
      trans-weaken :
        ∀ {Γ σ τ} (x : Γ ∋ τ) →
        var · suc[ σ ] x ≅-⊢
        Simple.weaken[_] simple σ · (var · x)
      trans-weaken x = P.sym $ Simple.weaken-var simple x

  -- Terms can be translated into terms.

  no-translation : Translation-from T
  no-translation = record
    { translation  = record { trans = [id]; simple = simple }
    ; trans-weaken = λ _ → P.refl
    ; trans-var    = λ _ → P.refl
    }

record Substitution₂ (T : Term-like (i ⊔ u ⊔ e))
                     : Set (Level.suc (i ⊔ u ⊔ e)) where

  open Term-like T

  field
    substitution₁ : Substitution₁ T

  open Substitution₁ substitution₁

  field
    -- Lifts equalities valid for all variables and liftings to
    -- arbitrary terms.
    var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆′ :
      {T₁ T₂ : Term-like (i ⊔ u ⊔ e)}
      (T₁↦T : Translation-from T₁) (T₂↦T : Translation-from T₂) →

      let open Translation-from T₁↦T
            using () renaming (_↑⁺⋆_ to _↑⁺⋆₁_; _/⊢⋆_ to _/⊢⋆₁_)
          open Translation-from T₂↦T
            using () renaming (_↑⁺⋆_ to _↑⁺⋆₂_; _/⊢⋆_ to _/⊢⋆₂_) in

      ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρs₁ : Subs T₁ ρ̂) (ρs₂ : Subs T₂ ρ̂) →
      (∀ Γ⁺ {σ} (x : Γ ++⁺ Γ⁺ ∋ σ) →
         var · x /⊢⋆₁ ρs₁ ↑⁺⋆₁ Γ⁺ ≅-⊢ var · x /⊢⋆₂ ρs₂ ↑⁺⋆₂ Γ⁺) →
      ∀ Γ⁺ {σ} (t : Γ ++⁺ Γ⁺ ⊢ σ) →
      t /⊢⋆₁ ρs₁ ↑⁺⋆₁ Γ⁺ ≅-⊢ t /⊢⋆₂ ρs₂ ↑⁺⋆₂ Γ⁺

  -- Given a well-behaved translation from something with simple
  -- substitutions one can define an Application₂₂ record.

  application₂₂ :
    {T′ : Term-like (i ⊔ u ⊔ e)} (T′↦T : Translation-from T′) →
    let open Translation-from T′↦T
          using (trans) renaming (simple to simple′) in
    Application₂₂ simple′ simple trans
  application₂₂ T′↦T = record
    { application₂₁         = Translation-from.application₂₁ T′↦T
    ; var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆ = var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆′ T′↦T T′↦T
    ; /⊢-wk                 = /⊢-wk
    }
    where
    open Translation-from T′↦T
      using ()
      renaming ( _↑⁺_ to _↑⁺′_; _↑⁺⋆_ to _↑⁺⋆′_
               ; wk to wk′; wk[_] to wk′[_]
               ; _/⊢_ to _/⊢′_; _/⊢⋆_ to _/⊢⋆′_
               )
    open Translation-from Var-↦
      using ()
      renaming ( _↑⁺_ to _↑⁺-renaming_; _↑⁺⋆_ to _↑⁺⋆-renaming_
               ; _/⊢_ to _/⊢-renaming_; _/⊢⋆_ to _/⊢⋆-renaming_
               )

    abstract
      /⊢-wk : ∀ {Γ σ τ} (t : Γ ⊢ τ) →
              t /⊢′ wk′[ σ ] ≅-⊢ t /⊢-renaming Renaming.wk[_] σ
      /⊢-wk =
        var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆′ T′↦T Var-↦ (ε ▻ wk′) (ε ▻ Renaming.wk)
          (λ Γ⁺ x → begin
             [ var · x /⊢⋆′ (ε ▻ wk′) ↑⁺⋆′ Γ⁺                         ]  ≡⟨ Translation-from./⊢⋆-ε-▻-↑⁺⋆ T′↦T Γ⁺ (var · x) wk′ ⟩
             [ var · x /⊢′ wk′ ↑⁺′ Γ⁺                                 ]  ≡⟨ Translation-from.var-/⊢-wk-↑⁺ T′↦T Γ⁺ x ⟩
             [ var · (lift weaken∋ Γ⁺ · x)                            ]  ≡⟨ P.sym $ Translation-from.var-/⊢-wk-↑⁺ Var-↦ Γ⁺ x ⟩
             [ var · x /⊢-renaming Renaming.wk ↑⁺-renaming Γ⁺         ]  ≡⟨ P.sym $ Translation-from./⊢⋆-ε-▻-↑⁺⋆
                                                                                Var-↦ Γ⁺ (var · x) Renaming.wk ⟩
             [ var · x /⊢⋆-renaming (ε ▻ Renaming.wk) ↑⁺⋆-renaming Γ⁺ ]  ∎)
          ε

  -- An Application₂₂ record for renamings.

  application₂₂-renaming : Application₂₂ Renaming.simple simple var
  application₂₂-renaming = application₂₂ Var-↦

  -- We can apply substitutions to terms.

  application₁ : Application₁ T
  application₁ = record
    { simple        = simple
    ; application₂₂ = application₂₂ no-translation
    }

  open Application₁ application₁ public
    hiding (var; simple; application₂₂)
  open Substitution₁ substitution₁ public

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
module Issue493 where

module M where
  postulate A B C : Set

module M₁ = M renaming (B to Y) hiding (A)
module M₂ = M using (A) using (B)
module M₃ = M hiding (A) hiding (B)

open M using (A) public