From 9ab446b96574a2efff1b2148d35684ab7a1bc554 Mon Sep 17 00:00:00 2001 From: Rahul Chhabra Date: Tue, 19 Dec 2023 00:36:30 +0530 Subject: [PATCH] Delete tex directory --- tex/Realizability/Assembly.tex | 679 ------------------------------- tex/agda.sty | 722 --------------------------------- tex/index.tex | 9 - 3 files changed, 1410 deletions(-) delete mode 100644 tex/Realizability/Assembly.tex delete mode 100644 tex/agda.sty delete mode 100644 tex/index.tex diff --git a/tex/Realizability/Assembly.tex b/tex/Realizability/Assembly.tex deleted file mode 100644 index b593f96..0000000 --- a/tex/Realizability/Assembly.tex +++ /dev/null @@ -1,679 +0,0 @@ -{-# OPTIONS --cubical --allow-unsolved-metas #-} -open import Cubical.Core.Everything -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.HLevels -open import Cubical.Foundations.Isomorphism -open import Cubical.Foundations.Function -open import Cubical.Foundations.Equiv -open import Cubical.Data.Unit -open import Cubical.Data.Empty -open import Cubical.Data.Sigma -open import Cubical.Data.Sum hiding (map) -open import Cubical.HITs.PropositionalTruncation renaming (map to ∥∥map ; map2 to ∥∥map2) -open import Cubical.HITs.PropositionalTruncation.Monad -open import Cubical.HITs.SetCoequalizer renaming (rec to setCoequalizerRec ; elimProp to setCoequalizerElimProp) -open import Cubical.Relation.Binary -open import Cubical.Categories.Category -open import Cubical.Categories.Limits.Terminal -open import Cubical.Categories.Limits.Initial -open import Cubical.Categories.Limits.BinProduct -open import Cubical.Categories.Limits.Coequalizers -open import Cubical.Categories.Regular.Base -open import Cubical.Reflection.RecordEquiv -open import Cubical.Functions.Surjection -open import Cubical.Functions.Image - -open import Realizability.CombinatoryAlgebra -open import Realizability.Choice - -module Realizability.Assembly {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where - open CombinatoryAlgebra ca - open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a) - - record Assembly (X : Type ℓ) : Type (ℓ-suc ℓ) where - infix 25 _⊩_ - field - isSetX : isSet X - _⊩_ : A → X → Type ℓ - ⊩isPropValued : ∀ a x → isProp (a ⊩ x) - ⊩surjective : ∀ x → ∃[ a ∈ A ] a ⊩ x - - open Assembly - unitAssembly : Assembly Unit* - unitAssembly .isSetX = isSetUnit* - unitAssembly ._⊩_ a x = Unit* - unitAssembly .⊩isPropValued a x = isPropUnit* - unitAssembly .⊩surjective x = ∣ s ⨾ k ⨾ k , tt* ∣₁ - - emptyAssembly : Assembly ⊥* - emptyAssembly .isSetX = isProp→isSet isProp⊥* - emptyAssembly ._⊩_ a x = ⊥* - emptyAssembly .⊩isPropValued a x = isProp⊥* - emptyAssembly .⊩surjective x = ∣ s ⨾ k ⨾ k , x ∣₁ - - module _ {X Y : Type ℓ} {xs : Assembly X} {ys : Assembly Y} (t : A) (f : X → Y) where - - tracks : Type ℓ - tracks = ∀ (x : X) (aₓ : A) → (aₓ ⊩X x) → (t ⨾ aₓ) ⊩Y (f x) where - _⊩X_ = xs ._⊩_ - _⊩Y_ = ys ._⊩_ - - isPropTracks : isProp tracks - isPropTracks = isPropΠ λ x → - isPropΠ λ aₓ → - isPropΠ λ aₓ⊩x → - ys .⊩isPropValued (t ⨾ aₓ) (f x) - - record AssemblyMorphism {X Y : Type ℓ} (as : Assembly X) (bs : Assembly Y) : Type ℓ where - open Assembly as renaming (_⊩_ to _⊩X_) - open Assembly bs renaming (_⊩_ to _⊩Y_) - field - map : X → Y - tracker : ∃[ t ∈ A ] ((x : X) (aₓ : A) → (aₓ ⊩X x) → (t ⨾ aₓ) ⊩Y (map x)) - open AssemblyMorphism - - unquoteDecl AssemblyMorphismIsoΣ = declareRecordIsoΣ AssemblyMorphismIsoΣ (quote AssemblyMorphism) - - module _ {X Y : Type ℓ} (xs : Assembly X) (ys : Assembly Y) where - - AssemblyMorphismΣ : Type ℓ - AssemblyMorphismΣ = Σ[ map ∈ (X → Y) ] ∃[ t ∈ A ] ((x : X) (aₓ : A) → (aₓ ⊩X x) → (t ⨾ aₓ) ⊩Y (map x)) where - _⊩X_ = xs ._⊩_ - _⊩Y_ = ys ._⊩_ - - isSetAssemblyMorphismΣ : isSet AssemblyMorphismΣ - isSetAssemblyMorphismΣ = isSetΣ (isSet→ (ys .isSetX)) (λ map → isProp→isSet squash₁) - - AssemblyMorphism≡Σ = isoToPath (AssemblyMorphismIsoΣ {as = xs} {bs = ys}) - - isSetAssemblyMorphism : isSet (AssemblyMorphism xs ys) - isSetAssemblyMorphism = subst (λ t → isSet t) (sym AssemblyMorphism≡Σ) isSetAssemblyMorphismΣ - - AssemblyMorphismΣ≡ : {X Y : Type ℓ} - {xs : Assembly X} - {ys : Assembly Y} - (f g : AssemblyMorphismΣ xs ys) - → f .fst ≡ g .fst - → f ≡ g - AssemblyMorphismΣ≡ f g = Σ≡Prop λ _ → squash₁ - - module _ {X Y : Type ℓ} - {xs : Assembly X} - {ys : Assembly Y} - (f g : AssemblyMorphism xs ys) where - -- Necessary to please the constraint solver - theIso = AssemblyMorphismIsoΣ {X} {Y} {as = xs} {bs = ys} - thePath = AssemblyMorphismΣ≡ {X = X} {Y = Y} {xs = xs} {ys = ys} - open Iso - AssemblyMorphism≡ : (f .map ≡ g .map) → f ≡ g - AssemblyMorphism≡ fmap≡gmap i = theIso .inv (thePath (theIso .fun f) (theIso .fun g) (fmap≡gmap) i) - - identityMorphism : {X : Type ℓ} (as : Assembly X) → AssemblyMorphism as as - identityMorphism as .map x = x - identityMorphism as .tracker = ∣ Id , (λ x aₓ aₓ⊩x → subst (λ y → (as ⊩ y) x) (sym (Ida≡a aₓ)) aₓ⊩x) ∣₁ - - compositeMorphism : {X Y Z : Type ℓ} {xs : Assembly X} {ys : Assembly Y} {zs : Assembly Z} - → (f : AssemblyMorphism xs ys) - → (g : AssemblyMorphism ys zs) - → AssemblyMorphism xs zs - compositeMorphism f g .map x = g .map (f .map x) - compositeMorphism {X} {Y} {Z} {xs} {ys} {zs} f g .tracker = ∥∥map2 untruncated (f .tracker) (g .tracker) where - open Assembly xs renaming (_⊩_ to _⊩X_) - open Assembly ys renaming (_⊩_ to _⊩Y_) - open Assembly zs renaming (_⊩_ to _⊩Z_) - module _ (fTracker : Σ[ f~ ∈ A ] tracks {xs = xs} {ys = ys} f~ (f .map)) - (gTracker : Σ[ g~ ∈ A ] tracks {xs = ys} {ys = zs} g~ (g .map)) where - - f~ = fTracker .fst - f~tracks = fTracker .snd - - g~ = gTracker .fst - g~tracks = gTracker .snd - - easierVariant : ∀ x aₓ aₓ⊩x → (g~ ⨾ (f~ ⨾ aₓ)) ⊩Z g .map (f .map x) - easierVariant x aₓ aₓ⊩x = g~tracks (f .map x) (f~ ⨾ aₓ) (f~tracks x aₓ aₓ⊩x) - - goal : ∀ (x : X) (aₓ : A) (aₓ⊩x : aₓ ⊩X x) - → (B g~ f~ ⨾ aₓ) ⊩Z (compositeMorphism f g .map x) - goal x aₓ aₓ⊩x = subst (λ y → y ⊩Z g .map (f .map x)) - (sym (Ba≡gfa g~ f~ aₓ)) - (easierVariant x aₓ aₓ⊩x) - - untruncated : Σ[ t ∈ A ] - ((x : X) (aₓ : A) - → aₓ ⊩X x - → (t ⨾ aₓ) ⊩Z (compositeMorphism f g) .map x) - untruncated = B g~ f~ , goal - - infixl 23 _⊚_ - _⊚_ : {X Y Z : Type ℓ} → {xs : Assembly X} {ys : Assembly Y} {zs : Assembly Z} - → AssemblyMorphism xs ys - → AssemblyMorphism ys zs - → AssemblyMorphism xs zs - f ⊚ g = compositeMorphism f g - - module _ {X Y : Type ℓ} (xs : Assembly X) (ys : Assembly Y) where - ⊚idL : ∀ (f : AssemblyMorphism xs ys) → identityMorphism xs ⊚ f ≡ f - ⊚idL f = AssemblyMorphism≡ (identityMorphism xs ⊚ f) f (funExt λ x → refl) - - ⊚idR : ∀ (f : AssemblyMorphism ys xs) → f ⊚ identityMorphism xs ≡ f - ⊚idR f = AssemblyMorphism≡ (f ⊚ identityMorphism xs) f (funExt λ x → refl) - - module _ {X Y Z W : Type ℓ} - (xs : Assembly X) - (ys : Assembly Y) - (zs : Assembly Z) - (ws : Assembly W) - (f : AssemblyMorphism xs ys) - (g : AssemblyMorphism ys zs) - (h : AssemblyMorphism zs ws) where - - ⊚assoc : (f ⊚ g) ⊚ h ≡ f ⊚ (g ⊚ h) - ⊚assoc = AssemblyMorphism≡ ((f ⊚ g) ⊚ h) (f ⊚ (g ⊚ h)) (∘-assoc (h .map) (g .map) (f .map)) - open Category - - ASM : Category (ℓ-suc ℓ) ℓ - ASM .ob = Σ[ X ∈ Type ℓ ] Assembly X - ASM .Hom[_,_] x y = AssemblyMorphism (x .snd) (y .snd) - ASM .id {x} = identityMorphism (x .snd) - ASM ._⋆_ f g = f ⊚ g - ASM .⋆IdL {x} {y} f = ⊚idL (x .snd) (y .snd) f - ASM .⋆IdR {x} {y} f = ⊚idR (y .snd) (x .snd) f - ASM .⋆Assoc {x} {y} {z} {w} f g h = ⊚assoc (x .snd) (y .snd) (z .snd) (w .snd) f g h - ASM .isSetHom {x} {y} f g = isSetAssemblyMorphism (x .snd) (y .snd) f g - - -- Some constructions on assemblies - infixl 23 _⊗_ - _⊗_ : {A B : Type ℓ} → Assembly A → Assembly B → Assembly (A × B) - (as ⊗ bs) .isSetX = isSetΣ (as .isSetX) (λ _ → bs .isSetX) - (as ⊗ bs) ._⊩_ r (a , b) = (as ._⊩_ (pr₁ ⨾ r) a) × (bs ._⊩_ (pr₂ ⨾ r) b) - (as ⊗ bs) .⊩isPropValued r (a , b) = isPropΣ (as .⊩isPropValued (pr₁ ⨾ r) a) - (λ _ → bs .⊩isPropValued (pr₂ ⨾ r) b) - (as ⊗ bs) .⊩surjective (a , b) = do - (b~ , b~realizes) ← bs .⊩surjective b - (a~ , a~realizes) ← as .⊩surjective a - return - ( pair ⨾ a~ ⨾ b~ - , subst (λ x → as ._⊩_ x a) (sym (pr₁pxy≡x a~ b~)) a~realizes - , subst (λ x → bs ._⊩_ x b) (sym (pr₂pxy≡y a~ b~)) b~realizes - ) - - ⟪_,_⟫ : {X Y Z W : Type ℓ} - {xs : Assembly X} - {ys : Assembly Y} - {zs : Assembly Z} - {ws : Assembly W} - (f : AssemblyMorphism xs ys) - (g : AssemblyMorphism zs ws) - → AssemblyMorphism (xs ⊗ zs) (ys ⊗ ws) - ⟪ f , g ⟫ .map (x , z) = f .map x , g .map z - ⟪_,_⟫ {ys = ys} {ws = ws} f g .tracker = (do - (f~ , f~tracks) ← f .tracker - (g~ , g~tracks) ← g .tracker - return (s ⨾ (s ⨾ (k ⨾ pair) ⨾ (s ⨾ (k ⨾ f~) ⨾ (s ⨾ (k ⨾ pr₁) ⨾ Id))) ⨾ (s ⨾ (k ⨾ g~) ⨾ (s ⨾ (k ⨾ pr₂) ⨾ Id)) - , λ xz r r⊩xz → - ( subst (λ y → ys ._⊩_ y (f .map (xz .fst))) - (sym (subst _ - (sym (t⨾r≡pair_fg f~ g~ r)) - (pr₁pxy≡x (f~ ⨾ (pr₁ ⨾ r)) (g~ ⨾ (pr₂ ⨾ r))))) - (f~tracks (xz .fst) (pr₁ ⨾ r) (r⊩xz .fst))) - , subst (λ y → ws ._⊩_ y (g .map (xz .snd))) - (sym (subst _ - (sym (t⨾r≡pair_fg f~ g~ r)) - (pr₂pxy≡y (f~ ⨾ (pr₁ ⨾ r)) (g~ ⨾ (pr₂ ⨾ r))))) - (g~tracks (xz .snd) (pr₂ ⨾ r) (r⊩xz .snd)))) - where - module _ (f~ g~ r : A) where - subf≡fprr : ∀ f pr → (s ⨾ (k ⨾ f) ⨾ (s ⨾ (k ⨾ pr) ⨾ Id) ⨾ r) ≡ (f ⨾ (pr ⨾ r)) - subf≡fprr f pr = - s ⨾ (k ⨾ f) ⨾ (s ⨾ (k ⨾ pr) ⨾ Id) ⨾ r - ≡⟨ sabc≡ac_bc _ _ _ ⟩ - (k ⨾ f ⨾ r) ⨾ (s ⨾ (k ⨾ pr) ⨾ Id ⨾ r) - ≡⟨ cong (λ x → x ⨾ _) (kab≡a f r) ⟩ - f ⨾ (s ⨾ (k ⨾ pr) ⨾ Id ⨾ r) - ≡⟨ cong (λ x → f ⨾ x) (sabc≡ac_bc _ _ _) ⟩ - f ⨾ (k ⨾ pr ⨾ r ⨾ (Id ⨾ r)) - ≡⟨ cong (λ x → f ⨾ (x ⨾ (Id ⨾ r))) (kab≡a _ _ ) ⟩ - f ⨾ (pr ⨾ (Id ⨾ r)) - ≡⟨ cong (λ x → f ⨾ (pr ⨾ x)) (Ida≡a r) ⟩ - f ⨾ (pr ⨾ r) - ∎ - t⨾r≡pair_fg : - s ⨾ (s ⨾ (k ⨾ pair) ⨾ (s ⨾ (k ⨾ f~) ⨾ (s ⨾ (k ⨾ pr₁) ⨾ Id))) ⨾ (s ⨾ (k ⨾ g~) ⨾ (s ⨾ (k ⨾ pr₂) ⨾ Id)) ⨾ r - ≡ pair ⨾ (f~ ⨾ (pr₁ ⨾ r)) ⨾ (g~ ⨾ (pr₂ ⨾ r)) - t⨾r≡pair_fg = - s ⨾ (s ⨾ (k ⨾ pair) ⨾ (s ⨾ (k ⨾ f~) ⨾ (s ⨾ (k ⨾ pr₁) ⨾ Id))) ⨾ (s ⨾ (k ⨾ g~) ⨾ (s ⨾ (k ⨾ pr₂) ⨾ Id)) ⨾ r - ≡⟨ sabc≡ac_bc _ _ _ ⟩ - s ⨾ (k ⨾ pair) ⨾ (s ⨾ (k ⨾ f~) ⨾ (s ⨾ (k ⨾ pr₁) ⨾ Id)) ⨾ r ⨾ (s ⨾ (k ⨾ g~) ⨾ (s ⨾ (k ⨾ pr₂) ⨾ Id) ⨾ r) - ≡⟨ cong (λ x → x ⨾ (s ⨾ (k ⨾ g~) ⨾ (s ⨾ (k ⨾ pr₂) ⨾ Id) ⨾ r)) (sabc≡ac_bc _ _ _) ⟩ - k ⨾ pair ⨾ r ⨾ (s ⨾ (k ⨾ f~) ⨾ (s ⨾ (k ⨾ pr₁) ⨾ Id) ⨾ r) ⨾ (s ⨾ (k ⨾ g~) ⨾ (s ⨾ (k ⨾ pr₂) ⨾ Id) ⨾ r) - ≡⟨ cong (λ x → x ⨾ (s ⨾ (k ⨾ f~) ⨾ (s ⨾ (k ⨾ pr₁) ⨾ Id) ⨾ r) ⨾ (s ⨾ (k ⨾ g~) ⨾ (s ⨾ (k ⨾ pr₂) ⨾ Id) ⨾ r)) - (kab≡a pair r) ⟩ - pair ⨾ (s ⨾ (k ⨾ f~) ⨾ (s ⨾ (k ⨾ pr₁) ⨾ Id) ⨾ r) ⨾ (s ⨾ (k ⨾ g~) ⨾ (s ⨾ (k ⨾ pr₂) ⨾ Id) ⨾ r) - ≡⟨ cong₂ (λ x y → pair ⨾ x ⨾ y) (subf≡fprr f~ pr₁) (subf≡fprr g~ pr₂) ⟩ - pair ⨾ (f~ ⨾ (pr₁ ⨾ r)) ⨾ (g~ ⨾ (pr₂ ⨾ r)) - ∎ - - - - - π₁ : {A B : Type ℓ} {as : Assembly A} {bs : Assembly B} → AssemblyMorphism (as ⊗ bs) as - π₁ .map (a , b) = a - π₁ .tracker = ∣ pr₁ , (λ (a , b) p (goal , _) → goal) ∣₁ - - π₂ : {A B : Type ℓ} {as : Assembly A} {bs : Assembly B} → AssemblyMorphism (as ⊗ bs) bs - π₂ .map (a , b) = b - π₂ .tracker = ∣ pr₂ , (λ (a , b) p (_ , goal) → goal) ∣₁ - - ⟨_,_⟩ : {X Y Z : Type ℓ} - → {xs : Assembly X} {ys : Assembly Y} {zs : Assembly Z} - → AssemblyMorphism zs xs - → AssemblyMorphism zs ys - → AssemblyMorphism zs (xs ⊗ ys) - ⟨ f , g ⟩ .map z = f .map z , g .map z - ⟨_,_⟩ {X} {Y} {Z} {xs} {ys} {zs} f g .tracker = ∥∥map2 untruncated (f .tracker) (g .tracker) where - module _ - ((f~ , f~tracks) : Σ[ f~ ∈ A ] tracks {xs = zs} {ys = xs} f~ (f .map)) - ((g~ , g~tracks) : Σ[ g~ ∈ A ] tracks {xs = zs} {ys = ys} g~ (g .map)) where - - _⊩X_ = xs ._⊩_ - _⊩Y_ = ys ._⊩_ - _⊩Z_ = zs ._⊩_ - - t = s ⨾ (s ⨾ (k ⨾ pair) ⨾ (s ⨾ (k ⨾ f~) ⨾ Id)) ⨾ (s ⨾ (k ⨾ g~) ⨾ Id) - untruncated : Σ[ t ∈ A ] (∀ z zᵣ zᵣ⊩z → ((pr₁ ⨾ (t ⨾ zᵣ)) ⊩X (f .map z)) × ((pr₂ ⨾ (t ⨾ zᵣ)) ⊩Y (g .map z))) - untruncated = t , λ z zᵣ zᵣ⊩z → goal₁ z zᵣ zᵣ⊩z , goal₂ z zᵣ zᵣ⊩z where - module _ (z : Z) (zᵣ : A) (zᵣ⊩z : zᵣ ⊩Z z) where - - pr₁⨾tracker⨾zᵣ≡f~⨾zᵣ : pr₁ ⨾ (t ⨾ zᵣ) ≡ f~ ⨾ zᵣ - pr₁⨾tracker⨾zᵣ≡f~⨾zᵣ = - pr₁ ⨾ (s ⨾ (s ⨾ (k ⨾ pair) ⨾ (s ⨾ (k ⨾ f~) ⨾ Id)) ⨾ (s ⨾ (k ⨾ g~) ⨾ Id) ⨾ zᵣ) - ≡⟨ cong (λ x → pr₁ ⨾ x) (sabc≡ac_bc _ _ _) ⟩ - pr₁ ⨾ (s ⨾ (k ⨾ pair) ⨾ (s ⨾ (k ⨾ f~) ⨾ Id) ⨾ zᵣ ⨾ (s ⨾ (k ⨾ g~) ⨾ Id ⨾ zᵣ)) - ≡⟨ cong (λ x → pr₁ ⨾ (x ⨾ (s ⨾ (k ⨾ g~) ⨾ Id ⨾ zᵣ))) (sabc≡ac_bc _ _ _) ⟩ - pr₁ ⨾ (k ⨾ pair ⨾ zᵣ ⨾ (s ⨾ (k ⨾ f~) ⨾ Id ⨾ zᵣ) ⨾ (s ⨾ (k ⨾ g~) ⨾ Id ⨾ zᵣ)) - ≡⟨ cong (λ x → pr₁ ⨾ (x ⨾ (s ⨾ (k ⨾ f~) ⨾ Id ⨾ zᵣ) ⨾ (s ⨾ (k ⨾ g~) ⨾ Id ⨾ zᵣ))) (kab≡a _ _) ⟩ - pr₁ ⨾ (pair ⨾ (s ⨾ (k ⨾ f~) ⨾ Id ⨾ zᵣ) ⨾ (s ⨾ (k ⨾ g~) ⨾ Id ⨾ zᵣ)) - ≡⟨ pr₁pxy≡x _ _ ⟩ - s ⨾ (k ⨾ f~) ⨾ Id ⨾ zᵣ - ≡⟨ sabc≡ac_bc _ _ _ ⟩ - k ⨾ f~ ⨾ zᵣ ⨾ (Id ⨾ zᵣ) - ≡⟨ cong (λ x → x ⨾ (Id ⨾ zᵣ)) (kab≡a _ _) ⟩ - f~ ⨾ (Id ⨾ zᵣ) - ≡⟨ cong (λ x → f~ ⨾ x) (Ida≡a _) ⟩ - f~ ⨾ zᵣ - ∎ - - pr₂⨾tracker⨾zᵣ≡g~⨾zᵣ : pr₂ ⨾ (t ⨾ zᵣ) ≡ g~ ⨾ zᵣ - pr₂⨾tracker⨾zᵣ≡g~⨾zᵣ = - pr₂ ⨾ (s ⨾ (s ⨾ (k ⨾ pair) ⨾ (s ⨾ (k ⨾ f~) ⨾ Id)) ⨾ (s ⨾ (k ⨾ g~) ⨾ Id) ⨾ zᵣ) - ≡⟨ cong (λ x → pr₂ ⨾ x) (sabc≡ac_bc _ _ _) ⟩ - pr₂ ⨾ (s ⨾ (k ⨾ pair) ⨾ (s ⨾ (k ⨾ f~) ⨾ Id) ⨾ zᵣ ⨾ (s ⨾ (k ⨾ g~) ⨾ Id ⨾ zᵣ)) - ≡⟨ cong (λ x → pr₂ ⨾ (x ⨾ (s ⨾ (k ⨾ g~) ⨾ Id ⨾ zᵣ))) (sabc≡ac_bc _ _ _) ⟩ - pr₂ ⨾ (k ⨾ pair ⨾ zᵣ ⨾ (s ⨾ (k ⨾ f~) ⨾ Id ⨾ zᵣ) ⨾ (s ⨾ (k ⨾ g~) ⨾ Id ⨾ zᵣ)) - ≡⟨ cong (λ x → pr₂ ⨾ (x ⨾ (s ⨾ (k ⨾ f~) ⨾ Id ⨾ zᵣ) ⨾ (s ⨾ (k ⨾ g~) ⨾ Id ⨾ zᵣ))) (kab≡a _ _) ⟩ - pr₂ ⨾ (pair ⨾ (s ⨾ (k ⨾ f~) ⨾ Id ⨾ zᵣ) ⨾ (s ⨾ (k ⨾ g~) ⨾ Id ⨾ zᵣ)) - ≡⟨ pr₂pxy≡y _ _ ⟩ - s ⨾ (k ⨾ g~) ⨾ Id ⨾ zᵣ - ≡⟨ sabc≡ac_bc _ _ _ ⟩ - k ⨾ g~ ⨾ zᵣ ⨾ (Id ⨾ zᵣ) - ≡⟨ cong (λ x → x ⨾ (Id ⨾ zᵣ)) (kab≡a _ _) ⟩ - g~ ⨾ (Id ⨾ zᵣ) - ≡⟨ cong (λ x → g~ ⨾ x) (Ida≡a _) ⟩ - g~ ⨾ zᵣ - ∎ - goal₁ : (pr₁ ⨾ (t ⨾ zᵣ)) ⊩X (f .map z) - goal₁ = subst (λ y → y ⊩X (f .map z)) (sym pr₁⨾tracker⨾zᵣ≡f~⨾zᵣ) (f~tracks z zᵣ zᵣ⊩z) - - goal₂ : (pr₂ ⨾ (t ⨾ zᵣ)) ⊩Y (g .map z) - goal₂ = subst (λ y → y ⊩Y (g .map z)) (sym pr₂⨾tracker⨾zᵣ≡g~⨾zᵣ) (g~tracks z zᵣ zᵣ⊩z) - -- Not sure if this is correct but okay let us see - infixl 23 _⊕_ - _⊕_ : {A B : Type ℓ} → Assembly A → Assembly B → Assembly (A ⊎ B) - (as ⊕ bs) .isSetX = isSet⊎ (as .isSetX) (bs .isSetX) - (as ⊕ bs) ._⊩_ r (inl a) = ∃[ aᵣ ∈ A ] (as ._⊩_ aᵣ a) × (r ≡ pair ⨾ true ⨾ aᵣ) - (as ⊕ bs) ._⊩_ r (inr b) = ∃[ bᵣ ∈ A ] (bs ._⊩_ bᵣ b) × (r ≡ pair ⨾ false ⨾ bᵣ) - (as ⊕ bs) .⊩isPropValued r (inl a) = squash₁ - (as ⊕ bs) .⊩isPropValued r (inr b) = squash₁ - (as ⊕ bs) .⊩surjective (inl a) = - do - (a~ , a~realizes) ← as .⊩surjective a - return ( pair ⨾ true ⨾ a~ - , ∣ a~ - , a~realizes - , refl ∣₁ - ) - (as ⊕ bs) .⊩surjective (inr b) = - do - (b~ , b~realizes) ← bs .⊩surjective b - return ( pair ⨾ false ⨾ b~ - , ∣ b~ - , b~realizes - , refl ∣₁ - ) - - κ₁ : {A B : Type ℓ} {as : Assembly A} {bs : Assembly B} → AssemblyMorphism as (as ⊕ bs) - κ₁ .map = inl - κ₁ .tracker = ∣ pair ⨾ true , (λ x aₓ aₓ⊩x → ∣ aₓ , aₓ⊩x , refl ∣₁) ∣₁ - - κ₂ : {A B : Type ℓ} {as : Assembly A} {bs : Assembly B} → AssemblyMorphism bs (as ⊕ bs) - κ₂ .map b = inr b - κ₂ .tracker = ∣ pair ⨾ false , (λ x bₓ bₓ⊩x → ∣ bₓ , bₓ⊩x , refl ∣₁) ∣₁ - module _ {A B : Type ℓ} {as : Assembly A} {bs : Assembly B} (f g : AssemblyMorphism as bs) where - _⊩A_ = as ._⊩_ - equalizer : Assembly (Σ[ a ∈ A ] f .map a ≡ g .map a) - equalizer .isSetX = isSetΣ (as .isSetX) λ x → isProp→isSet (bs .isSetX (f .map x) (g .map x)) - equalizer ._⊩_ r (a , fa≡ga) = as ._⊩_ r a - equalizer .⊩isPropValued r (a , fa≡ga) = as .⊩isPropValued r a - equalizer .⊩surjective (a , fa≡ga) = as .⊩surjective a - - ιequalizer : AssemblyMorphism equalizer as - ιequalizer .map (a , fa≡ga) = a - ιequalizer .tracker = ∣ Id , (λ x aₓ aₓ⊩x → subst (λ y → y ⊩A (x .fst)) (sym (Ida≡a aₓ)) aₓ⊩x) ∣₁ - - equalizerFactors : ((Z , zs) : Σ[ Z ∈ Type ℓ ] (Assembly Z)) - → (ι' : AssemblyMorphism zs as) - → (ι' ⊚ f ≡ ι' ⊚ g) - → ∃![ ! ∈ AssemblyMorphism zs equalizer ] (! ⊚ ιequalizer ≡ ι') - equalizerFactors (Z , zs) ι' ι'f≡ι'g = - uniqueExists (λ where - .map z → ι' .map z , λ i → ι'f≡ι'g i .map z - .tracker → ι' .tracker) - (AssemblyMorphism≡ _ _ refl) - (λ ! → isSetAssemblyMorphism _ _ (! ⊚ ιequalizer) ι') - λ !' !'⊚ι≡ι' → AssemblyMorphism≡ _ _ - (funExt λ z → Σ≡Prop (λ x → bs .isSetX (f .map x) (g .map x)) - (λ i → !'⊚ι≡ι' (~ i) .map z)) - - -- Exponential objects - _⇒_ : {A B : Type ℓ} → (as : Assembly A) → (bs : Assembly B) → Assembly (AssemblyMorphism as bs) - (as ⇒ bs) .isSetX = isSetAssemblyMorphism as bs - (as ⇒ bs) ._⊩_ r f = tracks {xs = as} {ys = bs} r (f .map) - _⇒_ {A} {B} as bs .⊩isPropValued r f = isPropTracks {X = A} {Y = B} {xs = as} {ys = bs} r (f .map) - (as ⇒ bs) .⊩surjective f = f .tracker - - -- What a distinguished gentleman - eval : {X Y : Type ℓ} → (xs : Assembly X) → (ys : Assembly Y) → AssemblyMorphism ((xs ⇒ ys) ⊗ xs) ys - eval xs ys .map (f , x) = f .map x - eval {X} {Y} xs ys .tracker = - ∣(s ⨾ (s ⨾ (k ⨾ pr₁) ⨾ Id) ⨾ (s ⨾ (k ⨾ pr₂) ⨾ Id)) - , (λ (f , x) r r⊩fx → subst - (λ y → y ⊩Y (f .map x)) - (sym (tracker⨾r≡pr₁r⨾pr₂r (f , x) r r⊩fx)) - (pr₁r⨾pr₂rTracks (f , x) r r⊩fx)) - ∣₁ where - _⊩Y_ = ys ._⊩_ - module _ (fx : (AssemblyMorphism xs ys) × X) - (r : A) - (r⊩fx : ((xs ⇒ ys) ⊗ xs) ._⊩_ r (fx .fst , fx .snd)) where - f = fx .fst - x = fx .snd - - pr₁r⨾pr₂rTracks : (pr₁ ⨾ r ⨾ (pr₂ ⨾ r)) ⊩Y (f .map x) - pr₁r⨾pr₂rTracks = r⊩fx .fst x (pr₂ ⨾ r) (r⊩fx .snd) - - tracker⨾r≡pr₁r⨾pr₂r : s ⨾ (s ⨾ (k ⨾ pr₁) ⨾ Id) ⨾ (s ⨾ (k ⨾ pr₂) ⨾ Id) ⨾ r ≡ (pr₁ ⨾ r) ⨾ (pr₂ ⨾ r) - tracker⨾r≡pr₁r⨾pr₂r = - s ⨾ (s ⨾ (k ⨾ pr₁) ⨾ Id) ⨾ (s ⨾ (k ⨾ pr₂) ⨾ Id) ⨾ r - ≡⟨ sabc≡ac_bc _ _ _ ⟩ - (s ⨾ (k ⨾ pr₁) ⨾ Id ⨾ r) ⨾ (s ⨾ (k ⨾ pr₂) ⨾ Id ⨾ r) - ≡⟨ cong (λ x → x ⨾ (s ⨾ (k ⨾ pr₂) ⨾ Id ⨾ r)) (sabc≡ac_bc _ _ _) ⟩ - (k ⨾ pr₁ ⨾ r ⨾ (Id ⨾ r)) ⨾ (s ⨾ (k ⨾ pr₂) ⨾ Id ⨾ r) - ≡⟨ cong (λ x → (k ⨾ pr₁ ⨾ r ⨾ (Id ⨾ r)) ⨾ x) (sabc≡ac_bc _ _ _) ⟩ - (k ⨾ pr₁ ⨾ r ⨾ (Id ⨾ r)) ⨾ (k ⨾ pr₂ ⨾ r ⨾ (Id ⨾ r)) - ≡⟨ cong (λ x → (x ⨾ (Id ⨾ r)) ⨾ (k ⨾ pr₂ ⨾ r ⨾ (Id ⨾ r))) (kab≡a _ _) ⟩ - (pr₁ ⨾ (Id ⨾ r)) ⨾ (k ⨾ pr₂ ⨾ r ⨾ (Id ⨾ r)) - ≡⟨ cong (λ x → (pr₁ ⨾ x) ⨾ (k ⨾ pr₂ ⨾ r ⨾ (Id ⨾ r))) (Ida≡a r) ⟩ - (pr₁ ⨾ r) ⨾ (k ⨾ pr₂ ⨾ r ⨾ (Id ⨾ r)) - ≡⟨ cong (λ x → (pr₁ ⨾ r) ⨾ (x ⨾ (Id ⨾ r))) (kab≡a _ _) ⟩ - (pr₁ ⨾ r) ⨾ (pr₂ ⨾ (Id ⨾ r)) - ≡⟨ cong (λ x → (pr₁ ⨾ r) ⨾ (pr₂ ⨾ x)) (Ida≡a r) ⟩ - (pr₁ ⨾ r) ⨾ (pr₂ ⨾ r) - ∎ - -- With major constructions done we start the universal properties - module _ {X Y : Type ℓ} (xs : Assembly X) (ys : Assembly Y) where - theπ₁ = π₁ {A = X} {B = Y} {as = xs} {bs = ys} - theπ₂ = π₂ {A = X} {B = Y} {as = xs} {bs = ys} - isBinProduct⊗ : ((Z , zs) : Σ[ Z ∈ Type ℓ ] Assembly Z) - → (f : AssemblyMorphism zs xs) - → (g : AssemblyMorphism zs ys) - → ∃![ fg ∈ AssemblyMorphism zs (xs ⊗ ys) ] (fg ⊚ theπ₁ ≡ f) × (fg ⊚ theπ₂ ≡ g) - isBinProduct⊗ (Z , zs) f g = - uniqueExists - {B = λ fg → (fg ⊚ theπ₁ ≡ f) × (fg ⊚ theπ₂ ≡ g)} - ⟨ f , g ⟩ - ( AssemblyMorphism≡ (⟨ f , g ⟩ ⊚ theπ₁) f (funExt (λ x → refl)) - , AssemblyMorphism≡ (⟨ f , g ⟩ ⊚ theπ₂) g (funExt (λ x → refl))) - (λ fg → isProp× - (isSetAssemblyMorphism zs xs (fg ⊚ theπ₁) f) - (isSetAssemblyMorphism zs ys (fg ⊚ theπ₂) g)) - -- TODO : Come up with a prettier proof - λ fg (fgπ₁≡f , fgπ₂≡g) → sym ((lemma₂ fg fgπ₁≡f fgπ₂≡g) ∙ (lemma₁ fg fgπ₁≡f fgπ₂≡g)) where - module _ (fg : AssemblyMorphism zs (xs ⊗ ys)) - (fgπ₁≡f : fg ⊚ theπ₁ ≡ f) - (fgπ₂≡g : fg ⊚ theπ₂ ≡ g) where - lemma₁ : ⟨ fg ⊚ theπ₁ , fg ⊚ theπ₂ ⟩ ≡ ⟨ f , g ⟩ - lemma₁ = AssemblyMorphism≡ - ⟨ fg ⊚ theπ₁ , fg ⊚ theπ₂ ⟩ - ⟨ f , g ⟩ - (λ i z → (fgπ₁≡f i .map z) , (fgπ₂≡g i .map z)) - - lemma₂ : fg ≡ ⟨ fg ⊚ theπ₁ , fg ⊚ theπ₂ ⟩ - lemma₂ = AssemblyMorphism≡ - fg - ⟨ fg ⊚ theπ₁ , fg ⊚ theπ₂ ⟩ - (funExt λ x → ΣPathP (refl , refl)) - - module _ where - open BinProduct - ASMBinProducts : BinProducts ASM - ASMBinProducts (X , xs) (Y , ys) .binProdOb = (X × Y) , (xs ⊗ ys) - ASMBinProducts (X , xs) (Y , ys) .binProdPr₁ = π₁ {as = xs} {bs = ys} - ASMBinProducts (X , xs) (Y , ys) .binProdPr₂ = π₂ {as = xs} {bs = ys} - ASMBinProducts (X , xs) (Y , ys) .univProp {z} f g = isBinProduct⊗ xs ys z f g - - isTerminalUnitAssembly : ((Z , zs) : Σ[ Z ∈ Type ℓ ] (Assembly Z)) → isContr (AssemblyMorphism zs unitAssembly) - isTerminalUnitAssembly (Z , zs) = - inhProp→isContr (λ where - .map → (λ _ → tt*) - .tracker → ∣ k ⨾ Id , (λ _ _ _ → tt*) ∣₁) - λ f g → AssemblyMorphism≡ f g refl - - ASMTerminal : Terminal ASM - ASMTerminal = (Unit* , unitAssembly) , isTerminalUnitAssembly - - isInitialUnitAssembly : ((Z , zs) : Σ[ Z ∈ Type ℓ ] (Assembly Z)) → isContr (AssemblyMorphism emptyAssembly zs) - isInitialUnitAssembly (Z , zs) = - inhProp→isContr (λ where - .map → λ () - .tracker → ∣ Id , (λ x aₓ aₓ⊩x → rec* x) ∣₁) - λ f g → AssemblyMorphism≡ _ _ (funExt λ x → rec* x) - - ASMInitial : Initial ASM - ASMInitial = (⊥* , emptyAssembly) , isInitialUnitAssembly - - module _ {X Y Z : Type ℓ} - {xs : Assembly X} - {ys : Assembly Y} - {zs : Assembly Z} - (f : AssemblyMorphism (zs ⊗ xs) ys) where - theEval = eval {X} {Y} xs ys - ⇒isExponential : ∃![ g ∈ AssemblyMorphism zs (xs ⇒ ys) ] - ⟪ g , identityMorphism xs ⟫ ⊚ theEval ≡ f - ⇒isExponential = uniqueExists (λ where - .map z → λ where - .map x → f .map (z , x) - .tracker → do - (f~ , f~tracks) ← f .tracker - (z~ , z~realizes) ← zs .⊩surjective z - return ( (s ⨾ (k ⨾ f~) ⨾ (s ⨾ (k ⨾ (pair ⨾ z~)) ⨾ Id) - , λ x aₓ aₓ⊩x - → subst (λ k → k ⊩Y (f .map (z , x))) - (sym (eq f~ f~tracks z (z~ , z~realizes) x aₓ aₓ⊩x)) - (pair⨾z~⨾aₓtracks f~ f~tracks z (z~ , z~realizes) x aₓ aₓ⊩x))) - .tracker → do - (f~ , f~tracker) ← f .tracker - -- λ* x. λ* y. f~ ⨾ (pair ⨾ x ⨾ y) - return ({!!} , (λ z zᵣ zᵣ⊩z x xᵣ xᵣ⊩x → {!!}))) - (AssemblyMorphism≡ _ _ (funExt (λ (z , x) → refl))) - (λ g → isSetAssemblyMorphism _ _ (⟪ g , identityMorphism xs ⟫ ⊚ theEval) f) - λ g g×id⊚eval≡f → AssemblyMorphism≡ _ _ - (funExt (λ z → AssemblyMorphism≡ _ _ - (funExt (λ x → λ i → g×id⊚eval≡f (~ i) .map (z , x))))) where - _⊩X_ = xs ._⊩_ - _⊩Y_ = ys ._⊩_ - _⊩Z_ = zs ._⊩_ - _⊩Z×X_ = (zs ⊗ xs) ._⊩_ - Z×X = Z × X - module _ (f~ : A) - (f~tracks : (∀ (zx : Z×X) (r : A) (rRealizes : (r ⊩Z×X zx)) → ((f~ ⨾ r) ⊩Y (f .map zx)))) - (z : Z) - (zRealizer : Σ[ z~ ∈ A ] (z~ ⊩Z z)) - (x : X) - (aₓ : A) - (aₓ⊩x : aₓ ⊩X x) where - z~ : A - z~ = zRealizer .fst - z~realizes = zRealizer .snd - - eq : s ⨾ (k ⨾ f~) ⨾ (s ⨾ (k ⨾ (pair ⨾ z~)) ⨾ Id) ⨾ aₓ ≡ f~ ⨾ (pair ⨾ z~ ⨾ aₓ) - eq = - s ⨾ (k ⨾ f~) ⨾ (s ⨾ (k ⨾ (pair ⨾ z~)) ⨾ Id) ⨾ aₓ - ≡⟨ sabc≡ac_bc _ _ _ ⟩ - (k ⨾ f~ ⨾ aₓ) ⨾ (s ⨾ (k ⨾ (pair ⨾ z~)) ⨾ Id ⨾ aₓ) - ≡⟨ cong (λ x → x ⨾ (s ⨾ (k ⨾ (pair ⨾ z~)) ⨾ Id ⨾ aₓ)) (kab≡a f~ aₓ) ⟩ - f~ ⨾ (s ⨾ (k ⨾ (pair ⨾ z~)) ⨾ Id ⨾ aₓ) - ≡⟨ cong (λ x → f~ ⨾ x) (sabc≡ac_bc _ _ _) ⟩ - f~ ⨾ ((k ⨾ (pair ⨾ z~) ⨾ aₓ) ⨾ (Id ⨾ aₓ)) - ≡⟨ cong (λ x → f~ ⨾ (x ⨾ (Id ⨾ aₓ))) (kab≡a (pair ⨾ z~) aₓ) ⟩ - f~ ⨾ (pair ⨾ z~ ⨾ (Id ⨾ aₓ)) - ≡⟨ cong (λ x → f~ ⨾ (pair ⨾ z~ ⨾ x)) (Ida≡a aₓ) ⟩ - f~ ⨾ (pair ⨾ z~ ⨾ aₓ) - ∎ - - pair⨾z~⨾aₓtracks : (f~ ⨾ (pair ⨾ z~ ⨾ aₓ)) ⊩Y (f .map (z , x)) - pair⨾z~⨾aₓtracks = - f~tracks - (z , x) - (pair ⨾ z~ ⨾ aₓ) - ( (subst (λ y → y ⊩Z z) (sym (pr₁pxy≡x z~ aₓ)) z~realizes) - , (subst (λ y → y ⊩X x) (sym (pr₂pxy≡y z~ aₓ)) aₓ⊩x)) - -- ASM has coequalizers - module _ - {X Y : Type ℓ} - (xs : Assembly X) - (ys : Assembly Y) - (f g : AssemblyMorphism xs ys) - where - private - _⊩X_ = xs ._⊩_ - _⊩Y_ = ys ._⊩_ - - _⊩coeq_ : (a : A) (x : SetCoequalizer (f .map) (g .map)) → hProp ℓ - a ⊩coeq x = - setCoequalizerRec - isSetHProp - (λ y → (∃[ y' ∈ Y ] (inc {f = f .map} {g = g .map} y ≡ inc y') × (a ⊩Y y')) , squash₁) - (λ x i → (∃[ y' ∈ Y ] (coeq {f = f .map} {g = g .map} x i ≡ inc y') × (a ⊩Y y')) , squash₁) - x - - coequalizer : Assembly (SetCoequalizer (f .map) (g .map)) - ⊩coeqSurjective : (x : SetCoequalizer (f .map) (g .map)) → ∃[ a ∈ A ] ((a ⊩coeq x) .fst) - - coequalizer .isSetX = squash - coequalizer ._⊩_ a x = (a ⊩coeq x) .fst - coequalizer .⊩isPropValued a x = (a ⊩coeq x) .snd - coequalizer .⊩surjective x = ⊩coeqSurjective x - - ⊩coeqSurjective x = - setCoequalizerElimProp - {C = λ b → ∃[ a ∈ A ] ((a ⊩coeq b) .fst)} - (λ x → squash₁) - (λ b → do - (b~ , b~realizes) ← ys .⊩surjective b - return (b~ , b~⊩coeq_inc_b b b~ b~realizes)) - x where - b~⊩coeq_inc_b : (b : Y) (b~ : A) (b~realizes : b~ ⊩Y b) → (b~ ⊩coeq inc b) .fst - b~⊩coeq_inc_b b b~ b~realizes = ∣ b , refl , b~realizes ∣₁ - {- - Coequalziers have a map E ← Y ⇇ X - -} - ιcoequalizer : AssemblyMorphism ys coequalizer - ιcoequalizer .map = inc - ιcoequalizer .tracker = ∣ Id , (λ y yᵣ yᵣ⊩y → subst (λ r → (r ⊩coeq inc y) .fst) (sym (Ida≡a yᵣ)) ∣ y , refl , yᵣ⊩y ∣₁) ∣₁ - - coequalizerFactors : ((Z , zs) : Σ[ Z ∈ Type ℓ ] Assembly Z) - → (ι' : AssemblyMorphism ys zs) - → (f ⊚ ι' ≡ g ⊚ ι') - → ∃![ ! ∈ AssemblyMorphism coequalizer zs ] (ιcoequalizer ⊚ ! ≡ ι') - coequalizerFactors (Z , zs) ι' f⊚ι'≡g⊚ι' = - uniqueExists (λ where - .map → setCoequalizerRec (zs .isSetX) (ι' .map) λ x → λ i → f⊚ι'≡g⊚ι' i .map x - .tracker → {!!}) - (AssemblyMorphism≡ _ _ (funExt λ x → refl)) - (λ ! → isSetAssemblyMorphism ys zs (ιcoequalizer ⊚ !) ι') - λ ! ιcoequalizer⊚!≡ι' → AssemblyMorphism≡ _ _ - (funExt λ x → - setCoequalizerElimProp - {C = λ x → setCoequalizerRec (zs .isSetX) (ι' .map) (λ x₁ i → f⊚ι'≡g⊚ι' i .map x₁) x ≡ ! .map x} - (λ x → zs .isSetX _ _) (λ y → λ i → ιcoequalizer⊚!≡ι' (~ i) .map y) x) - open Coequalizer - open IsCoequalizer - - ιIsCoequalizer : IsCoequalizer {C = ASM} f g ιcoequalizer - ιIsCoequalizer .glues = AssemblyMorphism≡ _ _ (funExt λ x → SetCoequalizer.coeq x) - ιIsCoequalizer .univProp q qGlues = coequalizerFactors _ q qGlues - - ASMCoequalizer : Coequalizer {C = ASM} f g - ASMCoequalizer .coapex = (SetCoequalizer (f .map) (g .map)) , coequalizer - Coequalizer.coeq ASMCoequalizer = ιcoequalizer - ASMCoequalizer .isCoequalizer = ιIsCoequalizer - -- ASM is regular - module _ - {X Y : Type ℓ} - (xs : Assembly X) - (ys : Assembly Y) - (e : AssemblyMorphism xs ys) - where - _⊩X_ = xs ._⊩_ - _⊩Y_ = ys ._⊩_ - _⊩X×X_ = (xs ⊗ xs) ._⊩_ - - -- First, isSurjection(e .map) and surjective tracking - -- together create a regular epi in ASM - - tracksSurjection : (a : A) → Type ℓ - tracksSurjection a = ∀ y b → (b ⊩Y y) → ∃[ x ∈ X ] (e .map x ≡ y) × ((a ⨾ b) ⊩X x) - module _ - (surjection : isSurjection (e .map)) - (surjectionIsTracked : ∃[ a ∈ A ] tracksSurjection a) - (choice : Choice ℓ ℓ) - where - - kernelType : Type ℓ - kernelType = Σ[ x ∈ X ] Σ[ x' ∈ X ] (e .map x ≡ e .map x') - - kernelAssembly : Assembly kernelType - kernelAssembly .isSetX = isSetΣ (xs .isSetX) (λ x → isSetΣ (xs .isSetX) (λ x' → isProp→isSet (ys .isSetX _ _))) - kernelAssembly ._⊩_ r (x , x' , ex≡ex') = (xs ⊗ xs) ._⊩_ r (x , x') - kernelAssembly .⊩isPropValued r (x , x' , ex≡ex') = (xs ⊗ xs) .⊩isPropValued r (x , x') - kernelAssembly .⊩surjective (x , x' , ex≡ex') = (xs ⊗ xs) .⊩surjective (x , x') - - -- Kernel Pairs - k₁ : AssemblyMorphism kernelAssembly xs - k₁ .map (x , x' , ex≡ex') = x - k₁ .tracker = ∣ pr₁ , (λ (x , x' , ex≡ex') r r⊩xx' → r⊩xx' .fst) ∣₁ - - - k₂ : AssemblyMorphism kernelAssembly xs - k₂ .map (x , x' , ex≡ex') = x' - k₂ .tracker = ∣ pr₂ , (λ (x , x' , ex≡ex') r r⊩xx' → r⊩xx' .snd) ∣₁ - - open IsCoequalizer - eIsCoequalizer : IsCoequalizer {C = ASM} k₁ k₂ e - eIsCoequalizer .glues = AssemblyMorphism≡ _ _ (funExt λ (x , x' , ex≡ex') → ex≡ex') - eIsCoequalizer .univProp {W , ws} q k₁q≡k₂q = - uniqueExists - (λ where - .map y → {!choice X Y (e .map) surjection!} - .tracker → {!!}) {!!} {!!} {!!} diff --git a/tex/agda.sty b/tex/agda.sty deleted file mode 100644 index 58c28ec..0000000 --- a/tex/agda.sty +++ /dev/null @@ -1,722 +0,0 @@ -% ---------------------------------------------------------------------- -% Some useful commands when doing highlighting of Agda code in LaTeX. -% ---------------------------------------------------------------------- - -% !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! -% !!! NOTE: when you make changes to this file, bump the date. !!! -% !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! -\ProvidesPackage{agda} - [2021/07/14 version 2.6.3 Formatting LaTeX generated by Agda] - -\RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox, - calc, environ, xparse, xkeyval} - -% https://tex.stackexchange.com/questions/47576/combining-ifxetex-and-ifluatex-with-the-logical-or-operation -\newif\ifxetexorluatex -\ifxetex - \xetexorluatextrue -\else - \ifluatex - \xetexorluatextrue - \else - \xetexorluatexfalse - \fi -\fi - -% ---------------------------------------------------------------------- -% Options - -\DeclareOption{bw} {\newcommand{\AgdaColourScheme}{bw}} -\DeclareOption{conor}{\newcommand{\AgdaColourScheme}{conor}} - -\newif\if@AgdaEnableReferences\@AgdaEnableReferencesfalse -\DeclareOption{references}{ - \@AgdaEnableReferencestrue -} - -\newif\if@AgdaEnableLinks\@AgdaEnableLinksfalse -\DeclareOption{links}{ - \@AgdaEnableLinkstrue -} - -\ProcessOptions\relax - -% ---------------------------------------------------------------------- -% Font setup - -\tracinglostchars=2 % If the font is missing some symbol, then say - % so in the compilation output. - -% ---------------------------------------------------------------------- -% Colour schemes. - -\providecommand{\AgdaColourScheme}{standard} - -% ---------------------------------------------------------------------- -% References to code (needs additional post-processing of tex files to -% work, see wiki for details). - -\if@AgdaEnableReferences - \RequirePackage{catchfilebetweentags, xstring} - \newcommand{\AgdaRef}[2][]{% - \StrSubstitute{#2}{\_}{AgdaUnderscore}[\tmp]% - \ifthenelse{\isempty{#1}}% - {\ExecuteMetaData{AgdaTag-\tmp}}% - {\ExecuteMetaData{#1}{AgdaTag-\tmp}} - } -\fi - -\providecommand{\AgdaRef}[2][]{#2} - -% ---------------------------------------------------------------------- -% Links (only done if the option is passed and the user has loaded the -% hyperref package). - -\if@AgdaEnableLinks - \@ifpackageloaded{hyperref}{ - - % List that holds added targets. - \newcommand{\AgdaList}[0]{} - - \newtoggle{AgdaIsElem} - \newcounter{AgdaIndex} - \newcommand{\AgdaLookup}[3]{% - \togglefalse{AgdaIsElem}% - \setcounter{AgdaIndex}{0}% - \renewcommand*{\do}[1]{% - \ifstrequal{#1}{##1}% - {\toggletrue{AgdaIsElem}\listbreak}% - {\stepcounter{AgdaIndex}}}% - \dolistloop{\AgdaList}% - \iftoggle{AgdaIsElem}{#2}{#3}% - } - - \newcommand*{\AgdaTargetHelper}[1]{% - \AgdaLookup{#1}% - {\PackageError{agda}{``#1'' used as target more than once}% - {Overloaded identifiers and links do not% - work well, consider using unique% - \MessageBreak identifiers instead.}% - }% - {\listadd{\AgdaList}{#1}% - \hypertarget{Agda\theAgdaIndex}{}% - }% - } - - \newcommand{\AgdaTarget}[1]{\forcsvlist{\AgdaTargetHelper}{#1}} - - \newcommand{\AgdaLink}[1]{% - \AgdaLookup{#1}% - {\hyperlink{Agda\theAgdaIndex}{#1}}% - {#1}% - } - }{\PackageError{agda}{Load the hyperref package before the agda package}{}} -\fi - -\providecommand{\AgdaTarget}[1]{} -\providecommand{\AgdaLink}[1]{#1} - -% ---------------------------------------------------------------------- -% Font styles. - -\newcommand{\AgdaFontStyle}[1]{\textsf{#1}} -\ifthenelse{\equal{\AgdaColourScheme}{bw}}{ - \newcommand{\AgdaKeywordFontStyle}[1]{\underline{#1}} -}{ - \newcommand{\AgdaKeywordFontStyle}[1]{\textsf{#1}} -} -\newcommand{\AgdaStringFontStyle}[1]{\texttt{#1}} -\newcommand{\AgdaCommentFontStyle}[1]{\texttt{#1}} -\newcommand{\AgdaBoundFontStyle}[1]{\textit{#1}} - -% ---------------------------------------------------------------------- -% Colours. - -% ---------------------------------- -% The black and white colour scheme. -\ifthenelse{\equal{\AgdaColourScheme}{bw}}{ - - % Aspect colours. - \definecolor{AgdaComment} {HTML}{000000} - \definecolor{AgdaPragma} {HTML}{000000} - \definecolor{AgdaKeyword} {HTML}{000000} - \definecolor{AgdaString} {HTML}{000000} - \definecolor{AgdaNumber} {HTML}{000000} - \definecolor{AgdaSymbol} {HTML}{000000} - \definecolor{AgdaPrimitiveType}{HTML}{000000} - - % NameKind colours. - \definecolor{AgdaBound} {HTML}{000000} - \definecolor{AgdaGeneralizable} {HTML}{000000} - \definecolor{AgdaInductiveConstructor} {HTML}{000000} - \definecolor{AgdaCoinductiveConstructor}{HTML}{000000} - \definecolor{AgdaDatatype} {HTML}{000000} - \definecolor{AgdaField} {HTML}{000000} - \definecolor{AgdaFunction} {HTML}{000000} - \definecolor{AgdaMacro} {HTML}{000000} - \definecolor{AgdaModule} {HTML}{000000} - \definecolor{AgdaPostulate} {HTML}{000000} - \definecolor{AgdaPrimitive} {HTML}{000000} - \definecolor{AgdaRecord} {HTML}{000000} - \definecolor{AgdaArgument} {HTML}{000000} - - % Other aspect colours. - \definecolor{AgdaDottedPattern} {HTML}{000000} - \definecolor{AgdaUnsolvedMeta} {HTML}{D3D3D3} - \definecolor{AgdaUnsolvedConstraint}{HTML}{D3D3D3} - \definecolor{AgdaTerminationProblem}{HTML}{BEBEBE} - \definecolor{AgdaIncompletePattern} {HTML}{D3D3D3} - \definecolor{AgdaErrorWarning} {HTML}{BEBEBE} - \definecolor{AgdaError} {HTML}{696969} - - % Misc. - \definecolor{AgdaHole} {HTML}{BEBEBE} - -% ---------------------------------- -% Conor McBride's colour scheme. -}{ \ifthenelse{\equal{\AgdaColourScheme}{conor}}{ - - % Aspect colours. - \definecolor{AgdaComment} {HTML}{B22222} - \definecolor{AgdaPragma} {HTML}{000000} - \definecolor{AgdaKeyword} {HTML}{000000} - \definecolor{AgdaString} {HTML}{000000} - \definecolor{AgdaNumber} {HTML}{000000} - \definecolor{AgdaSymbol} {HTML}{000000} - \definecolor{AgdaPrimitiveType}{HTML}{0000CD} - - % NameKind colours. - \definecolor{AgdaBound} {HTML}{A020F0} - \definecolor{AgdaGeneralizable} {HTML}{A020F0} - \definecolor{AgdaInductiveConstructor} {HTML}{8B0000} - \definecolor{AgdaCoinductiveConstructor}{HTML}{8B0000} - \definecolor{AgdaDatatype} {HTML}{0000CD} - \definecolor{AgdaField} {HTML}{8B0000} - \definecolor{AgdaFunction} {HTML}{006400} - \definecolor{AgdaMacro} {HTML}{006400} - \definecolor{AgdaModule} {HTML}{006400} - \definecolor{AgdaPostulate} {HTML}{006400} - \definecolor{AgdaPrimitive} {HTML}{006400} - \definecolor{AgdaRecord} {HTML}{0000CD} - \definecolor{AgdaArgument} {HTML}{404040} - - % Other aspect colours. - \definecolor{AgdaDottedPattern} {HTML}{000000} - \definecolor{AgdaUnsolvedMeta} {HTML}{FFD700} - \definecolor{AgdaUnsolvedConstraint}{HTML}{FFD700} - \definecolor{AgdaTerminationProblem}{HTML}{FF0000} - \definecolor{AgdaIncompletePattern} {HTML}{A020F0} - \definecolor{AgdaErrorWarning} {HTML}{FF0000} - \definecolor{AgdaError} {HTML}{F4A460} - - % Misc. - \definecolor{AgdaHole} {HTML}{9DFF9D} - -% ---------------------------------- -% The standard colour scheme. -}{ - % Aspect colours. - \definecolor{AgdaComment} {HTML}{B22222} - \definecolor{AgdaPragma} {HTML}{000000} - \definecolor{AgdaKeyword} {HTML}{CD6600} - \definecolor{AgdaString} {HTML}{B22222} - \definecolor{AgdaNumber} {HTML}{A020F0} - \definecolor{AgdaSymbol} {HTML}{404040} - \definecolor{AgdaPrimitiveType}{HTML}{0000CD} - - % NameKind colours. - \definecolor{AgdaBound} {HTML}{000000} - \definecolor{AgdaGeneralizable} {HTML}{000000} - \definecolor{AgdaInductiveConstructor} {HTML}{008B00} - \definecolor{AgdaCoinductiveConstructor}{HTML}{8B7500} - \definecolor{AgdaDatatype} {HTML}{0000CD} - \definecolor{AgdaField} {HTML}{EE1289} - \definecolor{AgdaFunction} {HTML}{0000CD} - \definecolor{AgdaMacro} {HTML}{458B74} - \definecolor{AgdaModule} {HTML}{A020F0} - \definecolor{AgdaPostulate} {HTML}{0000CD} - \definecolor{AgdaPrimitive} {HTML}{0000CD} - \definecolor{AgdaRecord} {HTML}{0000CD} - \definecolor{AgdaArgument} {HTML}{404040} - - % Other aspect colours. - \definecolor{AgdaDottedPattern} {HTML}{000000} - \definecolor{AgdaUnsolvedMeta} {HTML}{FFFF00} - \definecolor{AgdaUnsolvedConstraint}{HTML}{FFFF00} - \definecolor{AgdaTerminationProblem}{HTML}{FFA07A} - \definecolor{AgdaIncompletePattern} {HTML}{F5DEB3} - \definecolor{AgdaErrorWarning} {HTML}{FFA07A} - \definecolor{AgdaError} {HTML}{FF0000} - - % Misc. - \definecolor{AgdaHole} {HTML}{9DFF9D} -}} - -% ---------------------------------------------------------------------- -% Commands. - -\newcommand{\AgdaNoSpaceMath}[1] - {\begingroup\thickmuskip=0mu\medmuskip=0mu#1\endgroup} - -% Aspect commands. -\newcommand{\AgdaComment} [1] - {\AgdaNoSpaceMath{\textcolor{AgdaComment}{\AgdaCommentFontStyle{#1}}}} -\newcommand{\AgdaPragma} [1] - {\AgdaNoSpaceMath{\textcolor{AgdaPragma}{\AgdaCommentFontStyle{#1}}}} -\newcommand{\AgdaKeyword} [1] - {\AgdaNoSpaceMath{\textcolor{AgdaKeyword}{\AgdaKeywordFontStyle{#1}}}} -\newcommand{\AgdaString} [1] - {\AgdaNoSpaceMath{\textcolor{AgdaString}{\AgdaStringFontStyle{#1}}}} -\newcommand{\AgdaNumber} [1] - {\AgdaNoSpaceMath{\textcolor{AgdaNumber}{\AgdaFontStyle{#1}}}} -\newcommand{\AgdaSymbol} [1] - {\AgdaNoSpaceMath{\textcolor{AgdaSymbol}{\AgdaFontStyle{#1}}}} -\newcommand{\AgdaPrimitiveType}[1] - {\AgdaNoSpaceMath{\textcolor{AgdaPrimitiveType}{\AgdaFontStyle{#1}}}} -%% Andreas, 2021-07-14, issue #5471 -%% To make italics correction \/ work, the font-style modifier -%% needs to be inside, in particular inside the \textcolor modifier, -%% as the \textcolor{} wrapping around something hides its content -%% to the logic that resolves \/ into a space or not. - -% Note that, in code generated by the LaTeX backend, \AgdaOperator is -% always applied to a NameKind command. -\newcommand{\AgdaOperator} [1]{#1} - -% NameKind commands. - -% The user can control the typesetting of (certain) individual tokens -% by redefining the following command. The first argument is the token -% and the second argument the thing to be typeset (sometimes just the -% token, sometimes \AgdaLink{}). Example: -% -% \usepackage{ifthen} -% -% % Insert extra space before some tokens. -% \DeclareRobustCommand{\AgdaFormat}[2]{% -% \ifthenelse{ -% \equal{#1}{≡⟨} \OR -% \equal{#1}{≡⟨⟩} \OR -% \equal{#1}{∎} -% }{\ }{}#2} -% -% Note the use of \DeclareRobustCommand. - -\newcommand{\AgdaFormat}[2]{#2} - -\newcommand{\AgdaBound}[1] - {\AgdaNoSpaceMath{\textcolor{AgdaBound}{\AgdaBoundFontStyle{\AgdaFormat{#1}{#1}}}}} -\newcommand{\AgdaGeneralizable}[1] - {\AgdaNoSpaceMath{\textcolor{AgdaGeneralizable}{\AgdaBoundFontStyle{\AgdaFormat{#1}{#1}}}}} -\newcommand{\AgdaInductiveConstructor}[1] - {\AgdaNoSpaceMath{\textcolor{AgdaInductiveConstructor}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} -\newcommand{\AgdaCoinductiveConstructor}[1] - {\AgdaNoSpaceMath{\textcolor{AgdaCoinductiveConstructor}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} -\newcommand{\AgdaDatatype}[1] - {\AgdaNoSpaceMath{\textcolor{AgdaDatatype}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} -\newcommand{\AgdaField}[1] - {\AgdaNoSpaceMath{\textcolor{AgdaField}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} -\newcommand{\AgdaFunction}[1] - {\AgdaNoSpaceMath{\textcolor{AgdaFunction}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} -\newcommand{\AgdaMacro}[1] - {\AgdaNoSpaceMath{\textcolor{AgdaMacro}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} -\newcommand{\AgdaModule}[1] - {\AgdaNoSpaceMath{\textcolor{AgdaModule}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} -\newcommand{\AgdaPostulate}[1] - {\AgdaNoSpaceMath{\textcolor{AgdaPostulate}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} -\newcommand{\AgdaPrimitive}[1] - {\AgdaNoSpaceMath{\textcolor{AgdaPrimitive}{\AgdaFontStyle{\AgdaFormat{#1}{#1}}}}} -\newcommand{\AgdaRecord}[1] - {\AgdaNoSpaceMath{\textcolor{AgdaRecord}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} -\newcommand{\AgdaArgument}[1] - {\AgdaNoSpaceMath{\textcolor{AgdaArgument}{\AgdaBoundFontStyle{\AgdaFormat{#1}{#1}}}}} - -% Other aspect commands. -\newcommand{\AgdaFixityOp} [1]{\AgdaNoSpaceMath{$#1$}} -\newcommand{\AgdaDottedPattern} [1]{\textcolor{AgdaDottedPattern}{#1}} -\newcommand{\AgdaUnsolvedMeta} [1] - {\AgdaFontStyle{\colorbox{AgdaUnsolvedMeta}{#1}}} -\newcommand{\AgdaUnsolvedConstraint}[1] - {\AgdaFontStyle{\colorbox{AgdaUnsolvedConstraint}{#1}}} -\newcommand{\AgdaTerminationProblem}[1] - {\AgdaFontStyle{\colorbox{AgdaTerminationProblem}{#1}}} -\newcommand{\AgdaIncompletePattern} [1]{\colorbox{AgdaIncompletePattern}{#1}} -\newcommand{\AgdaErrorWarning} [1]{\colorbox{AgdaErrorWarning}{#1}} -\newcommand{\AgdaError} [1] - {\textcolor{AgdaError}{\AgdaFontStyle{\underline{#1}}}} -\newcommand{\AgdaCatchallClause} [1]{#1} % feel free to change this - -% Used to hide code from LaTeX. -% -% Note that this macro has been deprecated in favour of giving the -% hide argument to the code environment. -\long\def\AgdaHide#1{\ignorespaces} - -% Misc. -\newcommand{\AgdaHole}[1]{\colorbox{AgdaHole}{#1}} - -% ---------------------------------------------------------------------- -% The code environment. - -\newcommand{\AgdaCodeStyle}{} -% \newcommand{\AgdaCodeStyle}{\tiny} - -\ifdefined\mathindent - {} -\else - \newdimen\mathindent\mathindent\leftmargini -\fi - -% Adds the given amount of vertical space and starts a new line. -% -% The implementation comes from lhs2TeX's polycode.fmt, written by -% Andres Löh. -\newcommand{\Agda@NewlineWithVerticalSpace}[1]{% - {\parskip=0pt\parindent=0pt\par\vskip #1\noindent}} - -% Should there be space around code? -\newboolean{Agda@SpaceAroundCode} - -% Use this command to avoid extra space around code blocks. -\newcommand{\AgdaNoSpaceAroundCode}{% - \setboolean{Agda@SpaceAroundCode}{false}} - -% Use this command to include extra space around code blocks. -\newcommand{\AgdaSpaceAroundCode}{% - \setboolean{Agda@SpaceAroundCode}{true}} - -% By default space is inserted around code blocks. -\AgdaSpaceAroundCode{} - -% Sometimes one might want to break up a code block into multiple -% pieces, but keep code in different blocks aligned with respect to -% each other. Then one can use the AgdaAlign environment. Example -% usage: -% -% \begin{AgdaAlign} -% \begin{code} -% code -% code (more code) -% \end{code} -% Explanation... -% \begin{code} -% aligned with "code" -% code (aligned with (more code)) -% \end{code} -% \end{AgdaAlign} -% -% Note that AgdaAlign environments should not be nested. -% -% Sometimes one might also want to hide code in the middle of a code -% block. This can be accomplished in the following way: -% -% \begin{AgdaAlign} -% \begin{code} -% visible -% \end{code} -% \begin{code}[hide] -% hidden -% \end{code} -% \begin{code} -% visible -% \end{code} -% \end{AgdaAlign} -% -% However, the result may be ugly: extra space is perhaps inserted -% around the code blocks. -% -% The AgdaSuppressSpace environment ensures that extra space is only -% inserted before the first code block, and after the last one (but -% not if \AgdaNoSpaceAroundCode{} is used). Example usage: -% -% \begin{AgdaAlign} -% \begin{code} -% code -% more code -% \end{code} -% Explanation... -% \begin{AgdaSuppressSpace} -% \begin{code} -% aligned with "code" -% aligned with "more code" -% \end{code} -% \begin{code}[hide] -% hidden code -% \end{code} -% \begin{code} -% also aligned with "more code" -% \end{code} -% \end{AgdaSuppressSpace} -% \end{AgdaAlign} -% -% Note that AgdaSuppressSpace environments should not be nested. -% -% There is also a combined environment, AgdaMultiCode, that combines -% the effects of AgdaAlign and AgdaSuppressSpace. - -% The number of the current/next code block (excluding hidden ones). -\newcounter{Agda@Current} -\setcounter{Agda@Current}{0} - -% The number of the previous code block (excluding hidden ones), used -% locally in \Agda@SuppressEnd. -\newcounter{Agda@Previous} - -% Is AgdaAlign active? -\newboolean{Agda@Align} -\setboolean{Agda@Align}{false} - -% The number of the first code block (if any) in a given AgdaAlign -% environment. -\newcounter{Agda@AlignStart} - -\newcommand{\Agda@AlignStart}{% - \ifthenelse{\boolean{Agda@Align}}{% - \PackageError{agda}{Nested AgdaAlign environments}{% - AgdaAlign and AgdaMultiCode environments must not be - nested.}}{% - \setboolean{Agda@Align}{true}% - \setcounter{Agda@AlignStart}{\value{Agda@Current}}}} - -\newcommand{\Agda@AlignEnd}{\setboolean{Agda@Align}{false}} - -\newenvironment{AgdaAlign}{% - \Agda@AlignStart{}}{% - \Agda@AlignEnd{}% - \ignorespacesafterend} - -% Is AgdaSuppressSpace active? -\newboolean{Agda@Suppress} -\setboolean{Agda@Suppress}{false} - -% The number of the first code block (if any) in a given -% AgdaSuppressSpace environment. -\newcounter{Agda@SuppressStart} - -% Does a "do not suppress space after" label exist for the current -% code block? (This boolean is used locally in the code environment's -% implementation.) -\newboolean{Agda@DoNotSuppressSpaceAfter} - -\newcommand{\Agda@SuppressStart}{% - \ifthenelse{\boolean{Agda@Suppress}}{% - \PackageError{agda}{Nested AgdaSuppressSpace environments}{% - AgdaSuppressSpace and AgdaMultiCode environments must not be - nested.}}{% - \setboolean{Agda@Suppress}{true}% - \setcounter{Agda@SuppressStart}{\value{Agda@Current}}}} - -% Marks the given code block as one that space should not be -% suppressed after (if AgdaSpaceAroundCode and AgdaSuppressSpace are -% both active). -\newcommand{\Agda@DoNotSuppressSpaceAfter}[1]{% - % The use of labels is intended to ensure that LaTeX will provide a - % warning if the document needs to be recompiled. - \label{Agda@DoNotSuppressSpaceAfter@#1}} - -\newcommand{\Agda@SuppressEnd}{% - \ifthenelse{\value{Agda@SuppressStart} = \value{Agda@Current}}{}{% - % Mark the previous code block in the .aux file. - \setcounter{Agda@Previous}{\theAgda@Current-1}% - \immediate\write\@auxout{% - \noexpand\Agda@DoNotSuppressSpaceAfter{\theAgda@Previous}}}% - \setboolean{Agda@Suppress}{false}} - -\newenvironment{AgdaSuppressSpace}{% - \Agda@SuppressStart{}}{% - \Agda@SuppressEnd{}% - \ignorespacesafterend} - -\newenvironment{AgdaMultiCode}{% - \Agda@AlignStart{}% - \Agda@SuppressStart{}}{% - \Agda@SuppressEnd{}% - \Agda@AlignEnd{}% - \ignorespacesafterend} - -% Vertical space used for empty lines. By default \abovedisplayskip. -\newlength{\AgdaEmptySkip} -\setlength{\AgdaEmptySkip}{\abovedisplayskip} - -% Extra space to be inserted for empty lines (the difference between -% \AgdaEmptySkip and \baselineskip). Used internally. -\newlength{\AgdaEmptyExtraSkip} - -% Counter used for code numbers. -\newcounter{AgdaCodeNumber} -% Formats a code number. -\newcommand{\AgdaFormatCodeNumber}[1]{(#1)} - -% A boolean used to handle the option number. -\newboolean{Agda@Number} -\setboolean{Agda@Number}{false} - -% A boolean used to handle the option inline*. (For some reason the -% approach used for hide and inline does not work for inline*.) -\newboolean{Agda@InlineStar} -\setboolean{Agda@InlineStar}{false} - -% Keys used by the code environment. -\define@boolkey[Agda]{code}{hide}[true]{} -\define@boolkey[Agda]{code}{inline}[true]{} -\define@boolkey[Agda]{code}{inline*}[true]{% - \setboolean{Agda@InlineStar}{true}} -\define@key[Agda]{code}{number}[]{% - \ifthenelse{\boolean{Agda@Number}}{}{% - \setboolean{Agda@Number}{true}% - % Increase the counter if this has not already been done. - \refstepcounter{AgdaCodeNumber}}% - % If the label is non-empty, set it. Note that it is possible to - % give several labels for a single code listing. - \ifthenelse{\equal{#1}{}}{}{\label{#1}}} - -% The code environment. -% -% Options: -% -% * hide: The code is hidden. Other options are ignored. -% -% * number: Give the code an equation number. -% -% * number=l: Give the code an equation number and the label l. It is -% possible to use this option several times with different labels. -% -% * inline/inline*: The code is inlined. In this case most of the -% discussion above does not apply, alignment is not respected, and so -% on. It is recommended to only use this option for a single line of -% code, and to not use two consecutive spaces in this piece of code. -% -% Note that this environment ignores spaces after its end. If a space -% (\AgdaSpace{}) should be inserted after the inline code, use -% inline*, otherwise use inline. -% -% When this option is used number is ignored. -% -% The implementation is based on plainhscode in lhs2TeX's -% polycode.fmt, written by Andres Löh. -\NewEnviron{code}[1][]{% - % Process the options. Complain about unknown options. - \setkeys[Agda]{code}[number]{#1}% - \ifAgda@code@hide% - % Hide the code. - \else% - \ifAgda@code@inline% - % Inline code. - % - % Make the polytable primitives emitted by the LaTeX backend - % do nothing. - \DeclareDocumentCommand{\>}{O{}O{}}{}% - \DeclareDocumentCommand{\<}{O{}}{}% - \AgdaCodeStyle\BODY% - \else% - \ifthenelse{\boolean{Agda@InlineStar}}{% - % Inline code with space at the end. - % - \DeclareDocumentCommand{\>}{O{}O{}}{}% - \DeclareDocumentCommand{\<}{O{}}{}% - \AgdaCodeStyle\BODY\AgdaSpace{}}{% - % - % Displayed code. - % - % Conditionally emit space before the code block. Unconditionally - % switch to a new line. - \ifthenelse{\boolean{Agda@SpaceAroundCode} \and% - \(\not \boolean{Agda@Suppress} \or% - \value{Agda@SuppressStart} = \value{Agda@Current}\)}{% - \Agda@NewlineWithVerticalSpace{\abovedisplayskip}}{% - \Agda@NewlineWithVerticalSpace{0pt}}% - % - % Check if numbers have been requested. If they have, then a side - % effect of this call is that Agda@Number is set to true, the code - % number counter is increased, and the label (if any) is set. - \setkeys[Agda]{code}[hide,inline,inline*]{#1}% - \ifthenelse{\boolean{Agda@Number}}{% - % Equation numbers have been requested. Use a minipage, so that - % there is room for the code number to the right, and the code - % number becomes centered vertically. - \begin{minipage}{% - \linewidth-% - \widthof{% - \AgdaSpace{}% - \AgdaFormatCodeNumber{\theAgdaCodeNumber}}}}{}% - % - % Indent the entire code block. - \advance\leftskip\mathindent% - % - % The code's style can be customised. - \AgdaCodeStyle% - % - % Used to control the height of empty lines. - \setlength{\AgdaEmptyExtraSkip}{\AgdaEmptySkip - \baselineskip}% - % - % The environment used to handle indentation (of individual lines) - % and alignment. - \begin{pboxed}% - % - % Conditionally preserve alignment between code blocks. - \ifthenelse{\boolean{Agda@Align}}{% - \ifthenelse{\value{Agda@AlignStart} = \value{Agda@Current}}{% - \savecolumns}{% - \restorecolumns}}{}% - % - % The code. - \BODY% - \end{pboxed}% - % - \ifthenelse{\boolean{Agda@Number}}{% - % Equation numbers have been requested. - \end{minipage}% - % Insert the code number to the right. - \hfill \AgdaFormatCodeNumber{\theAgdaCodeNumber}}{}% - % - % Does the label Agda@DoNotSuppressAfter@ exist? - \ifcsdef{r@Agda@DoNotSuppressSpaceAfter@\theAgda@Current}{% - \setboolean{Agda@DoNotSuppressSpaceAfter}{true}}{% - \setboolean{Agda@DoNotSuppressSpaceAfter}{false}}% - % - % Conditionally emit space after the code block. Unconditionally - % switch to a new line. - \ifthenelse{\boolean{Agda@SpaceAroundCode} \and% - \(\not \boolean{Agda@Suppress} \or% - \boolean{Agda@DoNotSuppressSpaceAfter}\)}{% - \Agda@NewlineWithVerticalSpace{\belowdisplayskip}}{% - \Agda@NewlineWithVerticalSpace{0pt}}% - % - % Step the code block counter, but only for non-hidden code. - \stepcounter{Agda@Current}}% - \fi% - \fi% - % Reset Agda@Number and Agda@InlineStar. - \setboolean{Agda@Number}{false}% - \setboolean{Agda@InlineStar}{false}} - -% Space inserted after tokens. -\newcommand{\AgdaSpace}{ } - -% Space inserted to indent something. -\newcommand{\AgdaIndentSpace}{\AgdaSpace{}$\;\;$} - -% Default column for polytable. -\defaultcolumn{@{}l@{\AgdaSpace{}}} - -% \AgdaIndent expects a non-negative integer as its only argument. -% This integer should be the distance, in code blocks, to the thing -% relative to which the text is indented. -% -% The default implementation only indents if the thing that the text -% is indented relative to exists in the same code block or is wrapped -% in the same AgdaAlign or AgdaMultiCode environment. -\newcommand{\AgdaIndent}[1]{% - \ifthenelse{#1 = 0 - \or - \( \boolean{Agda@Align} - \and - \cnttest{\value{Agda@Current} - #1}{>=}{ - \value{Agda@AlignStart}} - \)}{\AgdaIndentSpace{}}{}} - -% Underscores are typeset using \AgdaUnderscore{}. -\newcommand{\AgdaUnderscore}{\_} - -\endinput diff --git a/tex/index.tex b/tex/index.tex deleted file mode 100644 index 37a4eab..0000000 --- a/tex/index.tex +++ /dev/null @@ -1,9 +0,0 @@ -{-# OPTIONS --cubical #-} -module index where - -open import Realizability.Partiality -open import Realizability.PartialApplicativeStructure -open import Realizability.PartialCombinatoryAlgebra -open import Realizability.CombinatoryAlgebra -open import Realizability.ApplicativeStructure -open import Realizability.Assembly