fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Banish qualified import of Function - use \o for fun-comp!

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-04-11 11:10:33 +02:00
parent c90b064bb0
commit db5fb3603a
10 changed files with 29 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Cat/Categories/Cube.agda
View file

@ -7,7 +7,6 @@ open import Data.Bool hiding (T)
open import Data.Sum hiding ([_,_])
open import Data.Unit
open import Data.Empty
open import Function
open import Relation.Nullary
open import Relation.Nullary.Decidable

3
src/Cat/Categories/Fam.agda
View file

@ -2,7 +2,6 @@
module Cat.Categories.Fam where
open import Cat.Prelude
import Function
open import Cat.Category
@ -15,7 +14,7 @@ module _ (ℓa ℓb : Level) where
fst identity = λ x → x
snd identity = λ b → b
_<<<_ : {a b c : Object} → Arr b c → Arr a b → Arr a c
(g , g') <<< (f , f') = g Function.∘ f , g' Function.∘ f'
(g , g') <<< (f , f') = g ∘ f , g' ∘ f'
RawFam : RawCategory (lsuc (ℓa ⊔ ℓb)) (ℓa ⊔ ℓb)
RawFam = record

1
src/Cat/Categories/Rel.agda
View file

@ -2,7 +2,6 @@
module Cat.Categories.Rel where
open import Cat.Prelude hiding (Rel)
open import Function
open import Cat.Category

20
src/Cat/Categories/Sets.agda
View file

@ -4,8 +4,6 @@ module Cat.Categories.Sets where
open import Cat.Prelude as P
open import Function using (_∘_ ; _∘′_)
open import Cat.Category
open import Cat.Category.Functor
open import Cat.Category.Product
@ -25,14 +23,14 @@ module _ (ℓ : Level) where
SetsRaw : RawCategory (lsuc ℓ) ℓ
RawCategory.Object SetsRaw = hSet ℓ
RawCategory.Arrow SetsRaw (T , _) (U , _) = T → U
RawCategory.identity SetsRaw = Function.id
RawCategory._<<<_ SetsRaw = Function._∘′_
RawCategory.identity SetsRaw = idFun _
RawCategory._<<<_ SetsRaw = _∘′_
module _ where
private
open RawCategory SetsRaw hiding (_<<<_)
isIdentity : IsIdentity Function.id
isIdentity : IsIdentity (idFun _)
fst isIdentity = funExt λ _ → refl
snd isIdentity = funExt λ _ → refl
@ -70,17 +68,17 @@ module _ (ℓ : Level) where
where
module xxA = AreInverses xx
module yyA = AreInverses yy
ve-re : g ∘ f ≡ Function.id
ve-re : g ∘ f ≡ idFun _
ve-re = arrowsAreSets {A = hA} {B = hA} _ _ xxA.verso-recto yyA.verso-recto i
re-ve : f ∘ g ≡ Function.id
re-ve : f ∘ g ≡ idFun _
re-ve = arrowsAreSets {A = hB} {B = hB} _ _ xxA.recto-verso yyA.recto-verso i
1eq : x.inverse ≡ y.inverse
1eq = begin
x.inverse ≡⟨⟩
x.inverse ∘ Function.id ≡⟨ cong (λ φ → x.inverse ∘ φ) (sym yA.recto-verso) ⟩
x.inverse ∘ idFun _ ≡⟨ cong (λ φ → x.inverse ∘ φ) (sym yA.recto-verso) ⟩
x.inverse ∘ (f ∘ y.inverse) ≡⟨⟩
(x.inverse ∘ f) ∘ y.inverse ≡⟨ cong (λ φ → φ ∘ y.inverse) xA.verso-recto ⟩
Function.id ∘ y.inverse ≡⟨⟩
idFun _ ∘ y.inverse ≡⟨⟩
y.inverse ∎
2eq : (λ i → AreInverses f (1eq i)) [ x.areInverses ≡ y.areInverses ]
2eq = lemPropF p 1eq
@ -266,7 +264,7 @@ module _ {ℓ : Level} where
module _ (hX : Object) where
open Σ hX renaming (fst to X)
module _ (f : X → A ) (g : X → B) where
ump : fst Function.∘′ (f &&& g) ≡ f × snd Function.∘′ (f &&& g) ≡ g
ump : fst ∘′ (f &&& g) ≡ f × snd ∘′ (f &&& g) ≡ g
fst ump = refl
snd ump = refl
@ -280,7 +278,7 @@ module _ {ℓ : Level} where
= f &&& g , ump hX f g , λ eq → funExt (umpUniq eq)
where
open Σ hX renaming (fst to X) using ()
module _ {y : X → A × B} (eq : fst Function.∘′ y ≡ f × snd Function.∘′ y ≡ g) (x : X) where
module _ {y : X → A × B} (eq : fst ∘′ y ≡ f × snd ∘′ y ≡ g) (x : X) where
p1 : fst ((f &&& g) x) ≡ fst (y x)
p1 = begin
fst ((f &&& g) x) ≡⟨⟩

25
src/Cat/Category.agda
View file

@ -35,8 +35,6 @@ open Cat.Equivalence
renaming (_≅_ to _≈_)
hiding (preorder≅ ; Isomorphism)
import Function
------------------
-- * Categories --
------------------
@ -146,7 +144,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
postulate from[Contr] : Univalent[Contr] → Univalent
from[Andrea] : Univalent[Andrea] → Univalent
from[Andrea] = from[Contr] Function.∘ step
from[Andrea] = from[Contr] ∘ step
where
module _ (f : Univalent[Andrea]) (A : Object) where
aux : isContr (Σ[ B ∈ Object ] A ≡ B)
@ -510,7 +508,7 @@ module Opposite {ℓa ℓb : Level} where
module ℂ = Category ℂ
opRaw : RawCategory ℓa ℓb
RawCategory.Object opRaw = ℂ.Object
RawCategory.Arrow opRaw = Function.flip ℂ.Arrow
RawCategory.Arrow opRaw = flip ℂ.Arrow
RawCategory.identity opRaw = ℂ.identity
RawCategory._<<<_ opRaw = ℂ._>>>_
@ -529,9 +527,6 @@ module Opposite {ℓa ℓb : Level} where
open Σ k renaming (fst to η ; snd to inv-η)
open AreInverses inv-η
_⊙_ = Function._∘_
infixr 9 _⊙_
genericly : {ℓa ℓb ℓc : Level} {a : Set ℓa} {b : Set ℓb} {c : Set ℓc}
→ a × b × c → b × a × c
genericly (a , b , c) = (b , a , c)
@ -557,22 +552,22 @@ module Opposite {ℓa ℓb : Level} where
open Σ r-iso renaming (fst to r-l ; snd to r-r)
ζ : A ≅ B → A ≡ B
ζ = η ⊙ shuffle
ζ = η ∘ shuffle
-- inv : AreInverses (ℂ.idToIso A B) f
inv-ζ : AreInverses (idToIso A B) ζ
-- recto-verso : ℂ.idToIso A B <<< f ≡ idFun (A ℂ.≅ B)
inv-ζ = record
{ verso-recto = funExt (λ x → begin
(ζ ⊙ idToIso A B) x ≡⟨⟩
(η ⊙ shuffle ⊙ idToIso A B) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → η ⊙ shuffle ⊙ φ) (funExt lem)) ⟩
(η ⊙ shuffle ⊙ shuffle~ ⊙ ℂ.idToIso A B) x ≡⟨⟩
(η ⊙ ℂ.idToIso A B) x ≡⟨ (λ i → verso-recto i x) ⟩
(ζ ∘ idToIso A B) x ≡⟨⟩
(η ∘ shuffle ∘ idToIso A B) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → η ∘ shuffle ∘ φ) (funExt lem)) ⟩
(η ∘ shuffle ∘ shuffle~ ∘ ℂ.idToIso A B) x ≡⟨⟩
(η ∘ ℂ.idToIso A B) x ≡⟨ (λ i → verso-recto i x) ⟩
x ∎)
; recto-verso = funExt (λ x → begin
(idToIso A B ⊙ η ⊙ shuffle) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → φ ⊙ η ⊙ shuffle) (funExt lem)) ⟩
(shuffle~ ⊙ ℂ.idToIso A B ⊙ η ⊙ shuffle) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → shuffle~ ⊙ φ ⊙ shuffle) recto-verso) ⟩
(shuffle~ ⊙ shuffle) x ≡⟨⟩
(idToIso A B ∘ η ∘ shuffle) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → φ ∘ η ∘ shuffle) (funExt lem)) ⟩
(shuffle~ ∘ ℂ.idToIso A B ∘ η ∘ shuffle) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → shuffle~ ∘ φ ∘ shuffle) recto-verso) ⟩
(shuffle~ ∘ shuffle) x ≡⟨⟩
x ∎)
}

5
src/Cat/Category/Functor.agda
View file

@ -2,7 +2,6 @@
module Cat.Category.Functor where
open import Cat.Prelude
open import Function
open import Cubical
@ -165,8 +164,8 @@ module Functors where
module _ {ℓc ℓcc : Level} {ℂ : Category ℓc ℓcc} where
private
raw : RawFunctor ℂ ℂ
RawFunctor.omap raw = Function.id
RawFunctor.fmap raw = Function.id
RawFunctor.omap raw = idFun _
RawFunctor.fmap raw = idFun _
isFunctor : IsFunctor ℂ ℂ raw
IsFunctor.isIdentity isFunctor = refl

5
src/Cat/Category/Monad/Voevodsky.agda
View file

@ -5,7 +5,6 @@ This module provides construction 2.3 in [voe]
module Cat.Category.Monad.Voevodsky where
open import Cat.Prelude
open import Function
open import Cat.Category
open import Cat.Category.Functor as F
@ -132,10 +131,10 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
Kleisli→Monoidal : K.Monad → M.Monad
Kleisli→Monoidal = E.reverse
ve-re : Kleisli→Monoidal ∘ Monoidal→Kleisli ≡ Function.id
ve-re : Kleisli→Monoidal ∘ Monoidal→Kleisli ≡ idFun _
ve-re = E.verso-recto
re-ve : Monoidal→Kleisli ∘ Kleisli→Monoidal ≡ Function.id
re-ve : Monoidal→Kleisli ∘ Kleisli→Monoidal ≡ idFun _
re-ve = E.recto-verso
forth : §2-3.§1 omap pure → §2-3.§2 omap pure

5
src/Cat/Category/Product.agda
View file

@ -3,7 +3,6 @@ module Cat.Category.Product where
open import Cat.Prelude as P hiding (_×_ ; fst ; snd)
open import Cat.Equivalence hiding (_≅_)
-- module P = Cat.Prelude
open import Cat.Category
@ -203,15 +202,13 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
: ((X , xa , xb) ≡ (Y , ya , yb))
≈ (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb))
step0
= (λ p → cong fst p , cong-d (fst ⊙ snd) p , cong-d (snd ⊙ snd) p)
= (λ p → cong fst p , cong-d (fst ∘ snd) p , cong-d (snd ∘ snd) p)
-- , (λ x → λ i → fst x i , (fst (snd x) i) , (snd (snd x) i))
, (λ{ (p , q , r) → Σ≡ p λ i → q i , r i})
, record
{ verso-recto = funExt (λ{ p → refl})
; recto-verso = funExt (λ{ (p , q , r) → refl})
}
where
open import Function renaming (_∘_ to _⊙_)
-- Should follow from c being univalent
iso-id-inv : {p : X ≡ Y} → p ≡ ℂ.isoToId (ℂ.idToIso X Y p)

2
src/Cat/Equivalence.agda
View file

@ -151,8 +151,6 @@ module _ {ℓa ℓb ℓ : Level} (A : Set ℓa) (B : Set ℓb) where
(x ∘ f) ∘ y ≡⟨ cong (λ φ → φ ∘ y) inv-x.verso-recto ⟩
y ∎
open import Cat.Prelude
propInv : ∀ g → isProp (AreInverses f g)
propInv g t u i = record { verso-recto = a i ; recto-verso = b i }
where

5
src/Cat/Prelude.agda
View file

@ -9,7 +9,10 @@ open import Data.Product public
renaming (∃! to ∃!≈)
using (_×_ ; Σ-syntax ; swap)
-- TODO Import Data.Function under appropriate names.
open import Function using (_∘_ ; _∘′_ ; _$_ ; case_of_ ; flip) public
idFun : ∀ {a} (A : Set a) → A → A
idFun A a = a
open import Cubical public
-- FIXME rename `gradLemma` to `fromIsomorphism` - perhaps just use wrapper